let p be Element of HP-WFF ; :: thesis: for v being SetValuation0 holds
( fixpoints (Perm ((v tohilbperm),p)) <> {} iff SetVal0 (v,p) <> {} )
let v be SetValuation0; :: thesis: ( fixpoints (Perm ((v tohilbperm),p)) <> {} iff SetVal0 (v,p) <> {} )
set V = v tohilbval ;
set P = v tohilbperm ;
set fP = Perm (v tohilbperm);
set fv = SetVal0 v;
set fV = SetVal (v tohilbval);
set I = id 1;
defpred S2[ set ] means ( (SetVal0 v) . $1 = {} iff fixpoints ((Perm (v tohilbperm)) . $1) = {} );
A1: S2[ VERUM ]
proof
fixpoints ((Perm (v tohilbperm)) . VERUM) = fixpoints (id 1) by HILBERT3:def 5
.= 1 ;
hence S2[ VERUM ] by Def2; :: thesis: verum
end;
A2: for n being Element of NAT holds S2[ prop n]
proof
let n be Element of NAT ; :: thesis: S2[ prop n]
set l = prop n;
set x = (SetVal0 v) . n;
set X = (SetVal (v tohilbval)) . n;
B0: ( (Perm (v tohilbperm)) . (prop n) = (v tohilbperm) . n & (SetVal0 v) . (prop n) = v . n ) by Def2, HILBERT3:def 5;
thus ( (SetVal0 v) . (prop n) = {} implies fixpoints ((Perm (v tohilbperm)) . (prop n)) = {} ) :: thesis: ( fixpoints ((Perm (v tohilbperm)) . (prop n)) = {} implies (SetVal0 v) . (prop n) = {} )
proof
assume (SetVal0 v) . (prop n) = {} ; :: thesis: fixpoints ((Perm (v tohilbperm)) . (prop n)) = {}
then (v tohilbperm) . n = (0,1) --> (1,0) by B0, Lm34, Lm17;
hence fixpoints ((Perm (v tohilbperm)) . (prop n)) = {} by B0; :: thesis: verum
end;
assume B1: fixpoints ((Perm (v tohilbperm)) . (prop n)) = {} ; :: thesis: (SetVal0 v) . (prop n) = {}
assume (SetVal0 v) . (prop n) <> {} ; :: thesis: contradiction
then ( v . n <> {} & (v tohilbperm) . n = (v . n) tohilb ) by Def2, Lm34;
then (v tohilbperm) . n = id 1 by Lm18;
hence contradiction by CARD_1:49, B1, B0; :: thesis: verum
end;
A3: for r, s being Element of HP-WFF st S2[r] & S2[s] holds
( S2[r '&' s] & S2[r => s] )
proof
let r, s be Element of HP-WFF ; :: thesis: ( S2[r] & S2[s] implies ( S2[r '&' s] & S2[r => s] ) )
set a = r '&' s;
set i = r => s;
set F = SetVal ((v tohilbval),r);
set H = SetVal ((v tohilbval),s);
set f = Perm ((v tohilbperm),r);
set h = Perm ((v tohilbperm),s);
reconsider h = Perm ((v tohilbperm),s) as non empty V67() Permutation of (SetVal ((v tohilbval),s)) ;
reconsider ff = (Perm ((v tohilbperm),r)) " as non empty V67() Permutation of (SetVal ((v tohilbval),r)) ;
set S = SomePoints ff;
set O = OtherPoints ff;
reconsider S = SomePoints ff, O = OtherPoints ff as Subset of (field ff) ;
set f1 = ff | S;
set f2 = ff | O;
assume B0: ( S2[r] & S2[s] ) ; :: thesis: ( S2[r '&' s] & S2[r => s] )
reconsider Sr = SetVal0 (v,r), Ss = SetVal0 (v,s) as set ;
SetVal0 (v,(r '&' s)) = [:Sr,Ss:] by Def2;
then ( SetVal0 (v,(r '&' s)) = {} iff [:(fixpoints (Perm ((v tohilbperm),r))),(fixpoints (Perm ((v tohilbperm),s))):] = {} ) by B0;
then ( SetVal0 (v,(r '&' s)) = {} iff fixpoints [:(Perm ((v tohilbperm),r)),(Perm ((v tohilbperm),s)):] = {} ) by FOMODEL0:76;
then ( SetVal0 (v,(r '&' s)) = {} iff fixpoints (Perm ((v tohilbperm),(r '&' s))) = {} ) by HILBERT3:35;
hence ( (SetVal0 v) . (r '&' s) = {} iff fixpoints ((Perm (v tohilbperm)) . (r '&' s)) = {} ) ; :: thesis: S2[r => s]
thus ( (SetVal0 v) . (r => s) = {} implies fixpoints ((Perm (v tohilbperm)) . (r => s)) = {} ) :: thesis: ( fixpoints ((Perm (v tohilbperm)) . (r => s)) = {} implies (SetVal0 v) . (r => s) = {} )
proof
assume (SetVal0 v) . (r => s) = {} ; :: thesis: fixpoints ((Perm (v tohilbperm)) . (r => s)) = {}
then {} = Funcs (((SetVal0 v) . r),((SetVal0 v) . s)) by Def2;
then ( Perm ((v tohilbperm),r) is with_fixpoint & h is without_fixpoints ) by B0;
then Perm ((v tohilbperm),(r => s)) is without_fixpoints by Lm3;
hence fixpoints ((Perm (v tohilbperm)) . (r => s)) = {} ; :: thesis: verum
end;
assume B2: fixpoints ((Perm (v tohilbperm)) . (r => s)) = {} ; :: thesis: (SetVal0 v) . (r => s) = {}
assume B3: (SetVal0 v) . (r => s) <> {} ; :: thesis: contradiction
per cases ( (SetVal0 v) . s <> {} or (SetVal0 v) . s = {} ) ;
suppose CCCC20: (SetVal0 v) . s = {} ; :: thesis: contradiction
then ( Funcs (((SetVal0 v) . r),((SetVal0 v) . s)) <> {} & (SetVal0 v) . s = {} ) by B3, Def2;
then CC20: ( (SetVal0 v) . s = {} & (SetVal0 v) . r = {} & (fixpoints ff) \+\ (fixpoints (Perm ((v tohilbperm),r))) = {} ) ;
C00: ( dom ff = SetVal ((v tohilbval),r) & dom h = SetVal ((v tohilbval),s) & rng h c= SetVal ((v tohilbval),s) & rng ff c= SetVal ((v tohilbval),r) ) by PARTFUN1:def 2;
C01: ( field ff = (SetVal ((v tohilbval),r)) null (rng ff) & field h = (SetVal ((v tohilbval),s)) null (rng h) ) by PARTFUN1:def 2;
C0: ( dom ff = SetVal ((v tohilbval),r) & dom h = SetVal ((v tohilbval),s) & rng h c= SetVal ((v tohilbval),s) & rng ff c= SetVal ((v tohilbval),r) & field ff = SetVal ((v tohilbval),r) & field h = SetVal ((v tohilbval),s) & dom (ff | S) = S & dom (ff | O) = O & ff .: O = S & ff .: S = O & rng (ff | S) = ff .: S & rng (ff | O) = ff .: O ) by C00, C01, Lm30;
then C2: ( (rng (ff | S)) /\ (rng (ff | O)) = {} & rng (ff | S) = dom (ff | O) & rng (ff | O) = dom (ff | S) ) ;
reconsider S = S, O = O as Subset of (dom ff) by PARTFUN1:def 2, C01;
( (rng h) \ (dom h) = {} & (field h) \ (fixpoints h) <> {} ) by CCCC20, B0;
then reconsider SH = SomePoints h, OH = OtherPoints h as non empty Subset of (dom h) by PARTFUN1:def 2, C01, Lm26;
set b1 = the Element of SH;
set b2 = h . the Element of SH;
( h . the Element of SH in h .: SH & h .: SH c= OH ) by Lm23, FUNCT_1:108;
then ( h . the Element of SH in OH & not h . the Element of SH in OH /\ SH ) ;
then C21: the Element of SH <> h . the Element of SH by XBOOLE_0:def 4;
reconsider b1 = the Element of SH as Element of dom h ;
set b2 = h . b1;
set ha = (b1,(h . b1)) --> ((h . b1),b1);
set hb = h \ ((b1,(h . b1)) --> ((h . b1),b1));
set g1 = [:(rng (ff | S)),{(h . b1)}:];
set g2 = [:(rng (ff | O)),{b1}:];
set g = [:(rng (ff | S)),{(h . b1)}:] \/ [:(rng (ff | O)),{b1}:];
set h1 = b1 .--> (h . b1);
set h2 = (h . b1) .--> b1;
( h . (h . b1) = b1 & h . b1 in dom h ) by C00;
then reconsider h1 = b1 .--> (h . b1), h2 = (h . b1) .--> b1 as Relation-like Function-like Subset of h by FUNCT_4:85;
( h1 \/ h2 c= h & h1 +*1 h2 c= h1 \/ h2 ) ;
then reconsider hha = (b1,(h . b1)) --> ((h . b1),b1) as Relation-like Function-like Subset of h by XBOOLE_1:1;
h = (h /\ ((b1,(h . b1)) --> ((h . b1),b1))) \/ (h \ ((b1,(h . b1)) --> ((h . b1),b1))) ;
then C14: (((ff | S) \/ (ff | O)) * ([:(rng (ff | S)),{(h . b1)}:] \/ [:(rng (ff | O)),{b1}:])) * h = ((((ff | S) \/ (ff | O)) * ([:(rng (ff | S)),{(h . b1)}:] \/ [:(rng (ff | O)),{b1}:])) * (hha null h)) \/ ((((ff | S) \/ (ff | O)) * ([:(rng (ff | S)),{(h . b1)}:] \/ [:(rng (ff | O)),{b1}:])) * (h \ ((b1,(h . b1)) --> ((h . b1),b1)))) by RELAT_1:32;
CC13: ( dom ((b1,(h . b1)) --> ((h . b1),b1)) = {b1,(h . b1)} & dom (h \ hha) = (dom h) \ (dom ((b1,(h . b1)) --> ((h . b1),b1))) ) by FOMODEL0:78, FUNCT_4:62;
( rng [:(rng (ff | S)),{(h . b1)}:] c= {(h . b1)} & {(h . b1)} \ {b1,(h . b1)} = {} ) ;
then ( rng [:(rng (ff | S)),{(h . b1)}:] c= {(h . b1)} & {(h . b1)} c= {b1,(h . b1)} ) by FOMODEL0:29;
then reconsider rg1 = rng [:(rng (ff | S)),{(h . b1)}:] as Subset of {b1,(h . b1)} by XBOOLE_1:1;
( rng [:(rng (ff | O)),{b1}:] c= {b1} & {b1} \ {b1,(h . b1)} = {} ) ;
then ( rng [:(rng (ff | O)),{b1}:] c= {b1} & {b1} c= {b1,(h . b1)} ) by FOMODEL0:29;
then reconsider rg2 = rng [:(rng (ff | O)),{b1}:] as Subset of {b1,(h . b1)} by XBOOLE_1:1;
( (rg1 \/ rg2) \+\ (rng ([:(rng (ff | S)),{(h . b1)}:] \/ [:(rng (ff | O)),{b1}:])) = {} & (rg1 \/ rg2) \ {b1,(h . b1)} = {} ) ;
then reconsider rg = rng ([:(rng (ff | S)),{(h . b1)}:] \/ [:(rng (ff | O)),{b1}:]) as Subset of {b1,(h . b1)} by FOMODEL0:29;
rng (((ff | S) \/ (ff | O)) >*> ([:(rng (ff | S)),{(h . b1)}:] \/ [:(rng (ff | O)),{b1}:])) c= rg by RELAT_1:26;
then reconsider R = rng (((ff | S) \/ (ff | O)) >*> ([:(rng (ff | S)),{(h . b1)}:] \/ [:(rng (ff | O)),{b1}:])) as Subset of {b1,(h . b1)} by XBOOLE_1:1;
(dom (h \ ((b1,(h . b1)) --> ((h . b1),b1)))) /\ R = {} by CC13;
then (((ff | S) \/ (ff | O)) >*> ([:(rng (ff | S)),{(h . b1)}:] \/ [:(rng (ff | O)),{b1}:])) >*> (h \ ((b1,(h . b1)) --> ((h . b1),b1))) = {} by XBOOLE_0:def 7, RELAT_1:44;
then C15: [:(rng (ff | S)),{(h . b1)}:] \/ [:(rng (ff | O)),{b1}:] c= (((ff | S) \/ (ff | O)) >*> ([:(rng (ff | S)),{(h . b1)}:] \/ [:(rng (ff | O)),{b1}:])) >*> h by C14, C2, FOMODEL0:77, C21;
CC3: S /\ O = {} ;
CC8: ( (dom [:(rng (ff | S)),{(h . b1)}:]) \ (dom [:(rng (ff | O)),{b1}:]) = dom [:(rng (ff | S)),{(h . b1)}:] & (dom (ff | S)) \ (dom (ff | O)) = dom (ff | S) ) by C0, CC3, XBOOLE_0:def 7, XBOOLE_1:83;
reconsider rff = rng ff as Subset of (SetVal ((v tohilbval),r)) ;
C10: SetVal ((v tohilbval),r) = ((field ff) \ S) \/ ((field ff) /\ S) by C01
.= ((field ff) \ S) \/ ((dom ff) /\ S) by C01, PARTFUN1:def 2
.= (O null (dom ff)) \/ S by CC20, B0 ;
( ((ff | S) \/ (ff | O)) \ ff = {} & ((dom (ff | S)) \/ (dom (ff | O))) \+\ (dom ((ff | S) \/ (ff | O))) = {} ) ;
then ( (ff | S) \/ (ff | O) c= ff & dom ((ff | S) \/ (ff | O)) = SetVal ((v tohilbval),r) ) by C10, FOMODEL0:29;
then (ff | S) \/ (ff | O) = ff by C00, FOMODEL0:68;
then C12: [:(rng (ff | S)),{(h . b1)}:] +* [:(rng (ff | O)),{b1}:] c= (h * ([:(rng (ff | S)),{(h . b1)}:] +* [:(rng (ff | O)),{b1}:])) * ff by CC8, C15, RELAT_1:36;
((dom [:(rng (ff | S)),{(h . b1)}:]) \/ (dom [:(rng (ff | O)),{b1}:])) \+\ (dom ([:(rng (ff | S)),{(h . b1)}:] \/ [:(rng (ff | O)),{b1}:])) = {} ;
then C11: dom ([:(rng (ff | S)),{(h . b1)}:] +* [:(rng (ff | O)),{b1}:]) = SetVal ((v tohilbval),r) by C0, C10, CC8, FOMODEL0:29;
dom ((h * ([:(rng (ff | S)),{(h . b1)}:] +* [:(rng (ff | O)),{b1}:])) * ff) c= dom ([:(rng (ff | S)),{(h . b1)}:] +* [:(rng (ff | O)),{b1}:]) by C11;
then C17: [:(rng (ff | S)),{(h . b1)}:] +* [:(rng (ff | O)),{b1}:] = (h * ([:(rng (ff | S)),{(h . b1)}:] +* [:(rng (ff | O)),{b1}:])) * ff by C12, FOMODEL0:68;
reconsider bb1 = b1, bb2 = h . b1 as Element of SetVal ((v tohilbval),s) ;
reconsider B = {bb1,bb2} as non empty Subset of (SetVal ((v tohilbval),s)) ;
rg c= {b1,(h . b1)} ;
then reconsider gg = [:(rng (ff | S)),{(h . b1)}:] +* [:(rng (ff | O)),{b1}:] as Element of Funcs ((SetVal ((v tohilbval),r)),B) by CC8, C11, FUNCT_2:def 2;
gg is SetVal ((v tohilbval),s) -valued ;
then {gg} \ (Funcs ((SetVal ((v tohilbval),r)),(SetVal ((v tohilbval),s)))) = {} ;
then reconsider gg = gg as Element of Funcs ((SetVal ((v tohilbval),r)),(SetVal ((v tohilbval),s))) by FOMODEL0:29;
( (Perm ((v tohilbperm),(r => s))) . gg = gg & gg <> {} ) by C17, HILBERT3:37;
then ( (Perm ((v tohilbperm),(r => s))) . gg = gg & gg in dom (Perm ((v tohilbperm),(r => s))) ) by FUNCT_1:def 2;
then gg is_a_fixpoint_of Perm ((v tohilbperm),(r => s)) by ABIAN:def 3;
hence contradiction by B2, FOMODEL0:69; :: thesis: verum
end;
end;
end;
for r being Element of HP-WFF holds S2[r] from HILBERT2:sch 2(A1, A2, A3);
 hence ( fixpoints (Perm ((v tohilbperm),p)) <> {} iff SetVal0 (v,p) <> {} ) ; :: thesis: verum