defpred S1[ Function of MP-WFF,F1(), Nat] means for A being MP-wff st card (dom A) <= $2 holds
( ( A = VERUM implies $1 . A = F2() ) & ( for p being MP-variable st A = @ p holds
$1 . A = F3(p) ) & ( for B being MP-wff st A = 'not' B holds
$1 . A = F4(($1 . B)) ) & ( for B being MP-wff st A = (#) B holds
$1 . A = F5(($1 . B)) ) & ( for B, C being MP-wff st A = B '&' C holds
$1 . A = F6(($1 . B),($1 . C)) ) );
defpred S2[ Element of F1(), Function of MP-WFF,F1(), Element of MP-WFF ] means ( ( $3 = VERUM implies $1 = F2() ) & ( for p being MP-variable st $3 = @ p holds
$1 = F3(p) ) & ( for A being MP-wff st $3 = 'not' A holds
$1 = F4(($2 . A)) ) & ( for A being MP-wff st $3 = (#) A holds
$1 = F5(($2 . A)) ) & ( for A, B being MP-wff st $3 = A '&' B holds
$1 = F6(($2 . A),($2 . B)) ) );
defpred S3[ Nat] means ex F being Function of MP-WFF,F1() st S1[F,$1];
defpred S4[ object , object ] means ex A being Element of MP-WFF st
( A = $1 & ( for g being Function of MP-WFF,F1() st S1[g, card (dom A)] holds
$2 = g . A ) );
A1: for k being Nat st S3[k] holds
S3[k + 1]
proof
let k be Nat; :: thesis: ( S3[k] implies S3[k + 1] )
given F being Function of MP-WFF,F1() such that A2: S1[F,k] ; :: thesis: S3[k + 1]
defpred S5[ Element of MP-WFF , Element of F1()] means ( ( card (dom $1) <> k + 1 implies $2 = F . $1 ) & ( card (dom $1) = k + 1 implies S2[$2,F,$1] ) );
A3: for x being Element of MP-WFF ex y being Element of F1() st S5[x,y]
proof
let A be Element of MP-WFF ; :: thesis: ex y being Element of F1() st S5[A,y]
now :: thesis: ( ( card (dom A) <> k + 1 & ex y being Element of F1() st verum ) or ( card (dom A) = k + 1 & A = VERUM & ex y being Element of F1() st S2[y,F,A] ) or ( card (dom A) = k + 1 & ex p being MP-variable st A = @ p & ex y being Element of F1() st S2[y,F,A] ) or ( card (dom A) = k + 1 & ex B being MP-wff st A = 'not' B & ex y being Element of F1() st S2[y,F,A] ) or ( card (dom A) = k + 1 & ex B being MP-wff st A = (#) B & ex y being Element of F1() st S2[y,F,A] ) or ( card (dom A) = k + 1 & ex B, C being MP-wff st A = B '&' C & ex y being Element of F1() st S2[y,F,A] ) )
per cases ( card (dom A) <> k + 1 or ( card (dom A) = k + 1 & A = VERUM ) or ( card (dom A) = k + 1 & ex p being MP-variable st A = @ p ) or ( card (dom A) = k + 1 & ex B being MP-wff st A = 'not' B ) or ( card (dom A) = k + 1 & ex B being MP-wff st A = (#) B ) or ( card (dom A) = k + 1 & ex B, C being MP-wff st A = B '&' C ) ) by Th37;
case card (dom A) <> k + 1 ; :: thesis: ex y being Element of F1() st verum
take y = F . A; :: thesis: verum
end;
case A4: ( card (dom A) = k + 1 & A = VERUM ) ; :: thesis: ex y being Element of F1() st S2[y,F,A]
take y = F2(); :: thesis: S2[y,F,A]
thus S2[y,F,A] by A4, Lm4, Lm6; :: thesis: verum
end;
case ( card (dom A) = k + 1 & ex p being MP-variable st A = @ p ) ; :: thesis: ex y being Element of F1() st S2[y,F,A]
then consider p being MP-variable such that
A5: A = @ p ;
take y = F3(p); :: thesis: S2[y,F,A]
thus S2[y,F,A] by A5, Lm6, Th27, Th38; :: thesis: verum
end;
case ( card (dom A) = k + 1 & ex B being MP-wff st A = 'not' B ) ; :: thesis: ex y being Element of F1() st S2[y,F,A]
then consider B being MP-wff such that
A6: A = 'not' B ;
take y = F4((F . B)); :: thesis: S2[y,F,A]
thus S2[y,F,A] by A6, Lm4, Th28, Th38, Th39; :: thesis: verum
end;
case ( card (dom A) = k + 1 & ex B being MP-wff st A = (#) B ) ; :: thesis: ex y being Element of F1() st S2[y,F,A]
then consider B being MP-wff such that
A7: A = (#) B ;
take y = F5((F . B)); :: thesis: S2[y,F,A]
thus S2[y,F,A] by A7, Lm4, Th29, Th38, Th39, Th40; :: thesis: verum
end;
case ( card (dom A) = k + 1 & ex B, C being MP-wff st A = B '&' C ) ; :: thesis: ex y being Element of F1() st S2[y,F,A]
then consider B, C being MP-wff such that
A8: A = B '&' C ;
take y = F6((F . B),(F . C)); :: thesis: S2[y,F,A]
now :: thesis: for B1, C1 being MP-wff st A = B1 '&' C1 holds
y = F6((F . B1),(F . C1))
let B1, C1 be MP-wff; :: thesis: ( A = B1 '&' C1 implies y = F6((F . B1),(F . C1)) )
assume A9: A = B1 '&' C1 ; :: thesis: y = F6((F . B1),(F . C1))
then B = B1 by A8, Th30;
hence y = F6((F . B1),(F . C1)) by A8, A9, Th30; :: thesis: verum
end;
hence S2[y,F,A] by A8, Lm4, Th38, Th39, Th40; :: thesis: verum
end;
end;
end;
hence ex y being Element of F1() st S5[A,y] ; :: thesis: verum
end;
consider G being Function of MP-WFF,F1() such that
A10: for p being Element of MP-WFF holds S5[p,G . p] from FUNCT_2:sch 3(A3);
 take H = G; :: thesis: S1[H,k + 1]
thus S1[H,k + 1] :: thesis: verum
proof
let A be Element of MP-WFF ; :: thesis: ( card (dom A) <= k + 1 implies ( ( A = VERUM implies H . A = F2() ) & ( for p being MP-variable st A = @ p holds
H . A = F3(p) ) & ( for B being MP-wff st A = 'not' B holds
H . A = F4((H . B)) ) & ( for B being MP-wff st A = (#) B holds
H . A = F5((H . B)) ) & ( for B, C being MP-wff st A = B '&' C holds
H . A = F6((H . B),(H . C)) ) ) )
set p = card (dom A);
assume A11: card (dom A) <= k + 1 ; :: thesis: ( ( A = VERUM implies H . A = F2() ) & ( for p being MP-variable st A = @ p holds
H . A = F3(p) ) & ( for B being MP-wff st A = 'not' B holds
H . A = F4((H . B)) ) & ( for B being MP-wff st A = (#) B holds
H . A = F5((H . B)) ) & ( for B, C being MP-wff st A = B '&' C holds
H . A = F6((H . B),(H . C)) ) )
thus ( A = VERUM implies H . A = F2() ) :: thesis: ( ( for p being MP-variable st A = @ p holds
H . A = F3(p) ) & ( for B being MP-wff st A = 'not' B holds
H . A = F4((H . B)) ) & ( for B being MP-wff st A = (#) B holds
H . A = F5((H . B)) ) & ( for B, C being MP-wff st A = B '&' C holds
H . A = F6((H . B),(H . C)) ) )
proof
per cases ( card (dom A) <> k + 1 or card (dom A) = k + 1 ) ;
suppose card (dom A) <> k + 1 ; :: thesis: ( A = VERUM implies H . A = F2() )
then ( card (dom A) <= k & H . A = F . A ) by A10, A11, NAT_1:8;
hence ( A = VERUM implies H . A = F2() ) by A2; :: thesis: verum
end;
suppose card (dom A) = k + 1 ; :: thesis: ( A = VERUM implies H . A = F2() )
hence ( A = VERUM implies H . A = F2() ) by A10; :: thesis: verum
end;
end;
end;
thus for p being MP-variable st A = @ p holds
H . A = F3(p) :: thesis: ( ( for B being MP-wff st A = 'not' B holds
H . A = F4((H . B)) ) & ( for B being MP-wff st A = (#) B holds
H . A = F5((H . B)) ) & ( for B, C being MP-wff st A = B '&' C holds
H . A = F6((H . B),(H . C)) ) )
proof
let q be MP-variable; :: thesis: ( A = @ q implies H . A = F3(q) )
assume A12: A = @ q ; :: thesis: H . A = F3(q)
per cases ( card (dom A) <> k + 1 or card (dom A) = k + 1 ) ;
suppose card (dom A) <> k + 1 ; :: thesis: H . A = F3(q)
then ( card (dom A) <= k & H . A = F . A ) by A10, A11, NAT_1:8;
hence H . A = F3(q) by A2, A12; :: thesis: verum
end;
suppose card (dom A) = k + 1 ; :: thesis: H . A = F3(q)
hence H . A = F3(q) by A10, A12; :: thesis: verum
end;
end;
end;
thus for B being MP-wff st A = 'not' B holds
H . A = F4((H . B)) :: thesis: ( ( for B being MP-wff st A = (#) B holds
H . A = F5((H . B)) ) & ( for B, C being MP-wff st A = B '&' C holds
H . A = F6((H . B),(H . C)) ) )
proof
let B be MP-wff; :: thesis: ( A = 'not' B implies H . A = F4((H . B)) )
assume A13: A = 'not' B ; :: thesis: H . A = F4((H . B))
then card (dom B) <> k + 1 by A11, Th33;
then A14: H . B = F . B by A10;
per cases ( card (dom A) <> k + 1 or card (dom A) = k + 1 ) ;
suppose card (dom A) <> k + 1 ; :: thesis: H . A = F4((H . B))
then ( card (dom A) <= k & H . A = F . A ) by A10, A11, NAT_1:8;
hence H . A = F4((H . B)) by A2, A13, A14; :: thesis: verum
end;
suppose card (dom A) = k + 1 ; :: thesis: H . A = F4((H . B))
hence H . A = F4((H . B)) by A10, A13, A14; :: thesis: verum
end;
end;
end;
thus for B being MP-wff st A = (#) B holds
H . A = F5((H . B)) :: thesis: for B, C being MP-wff st A = B '&' C holds
H . A = F6((H . B),(H . C))
proof
let B be MP-wff; :: thesis: ( A = (#) B implies H . A = F5((H . B)) )
assume A15: A = (#) B ; :: thesis: H . A = F5((H . B))
then card (dom B) <> k + 1 by A11, Th34;
then A16: H . B = F . B by A10;
per cases ( card (dom A) <> k + 1 or card (dom A) = k + 1 ) ;
suppose card (dom A) <> k + 1 ; :: thesis: H . A = F5((H . B))
then ( card (dom A) <= k & H . A = F . A ) by A10, A11, NAT_1:8;
hence H . A = F5((H . B)) by A2, A15, A16; :: thesis: verum
end;
suppose card (dom A) = k + 1 ; :: thesis: H . A = F5((H . B))
hence H . A = F5((H . B)) by A10, A15, A16; :: thesis: verum
end;
end;
end;
thus for B, C being MP-wff st A = B '&' C holds
H . A = F6((H . B),(H . C)) :: thesis: verum
proof
let B, C be MP-wff; :: thesis: ( A = B '&' C implies H . A = F6((H . B),(H . C)) )
assume A17: A = B '&' C ; :: thesis: H . A = F6((H . B),(H . C))
then card (dom B) <> k + 1 by A11, Th35;
then A18: H . B = F . B by A10;
card (dom C) <> k + 1 by A11, A17, Th35;
then A19: H . C = F . C by A10;
per cases ( card (dom A) <> k + 1 or card (dom A) = k + 1 ) ;
suppose card (dom A) <> k + 1 ; :: thesis: H . A = F6((H . B),(H . C))
then ( card (dom A) <= k & H . A = F . A ) by A10, A11, NAT_1:8;
hence H . A = F6((H . B),(H . C)) by A2, A17, A18, A19; :: thesis: verum
end;
suppose card (dom A) = k + 1 ; :: thesis: H . A = F6((H . B),(H . C))
hence H . A = F6((H . B),(H . C)) by A10, A17, A18, A19; :: thesis: verum
end;
end;
end;
end;
end;
A20: S3[ 0 ]
proof
set F = the Function of MP-WFF,F1();
take the Function of MP-WFF,F1() ; :: thesis: S1[ the Function of MP-WFF,F1(), 0 ]
let A be MP-wff; :: thesis: ( card (dom A) <= 0 implies ( ( A = VERUM implies the Function of MP-WFF,F1() . A = F2() ) & ( for p being MP-variable st A = @ p holds
the Function of MP-WFF,F1() . A = F3(p) ) & ( for B being MP-wff st A = 'not' B holds
the Function of MP-WFF,F1() . A = F4(( the Function of MP-WFF,F1() . B)) ) & ( for B being MP-wff st A = (#) B holds
the Function of MP-WFF,F1() . A = F5(( the Function of MP-WFF,F1() . B)) ) & ( for B, C being MP-wff st A = B '&' C holds
the Function of MP-WFF,F1() . A = F6(( the Function of MP-WFF,F1() . B),( the Function of MP-WFF,F1() . C)) ) ) )
assume card (dom A) <= 0 ; :: thesis: ( ( A = VERUM implies the Function of MP-WFF,F1() . A = F2() ) & ( for p being MP-variable st A = @ p holds
the Function of MP-WFF,F1() . A = F3(p) ) & ( for B being MP-wff st A = 'not' B holds
the Function of MP-WFF,F1() . A = F4(( the Function of MP-WFF,F1() . B)) ) & ( for B being MP-wff st A = (#) B holds
the Function of MP-WFF,F1() . A = F5(( the Function of MP-WFF,F1() . B)) ) & ( for B, C being MP-wff st A = B '&' C holds
the Function of MP-WFF,F1() . A = F6(( the Function of MP-WFF,F1() . B),( the Function of MP-WFF,F1() . C)) ) )
hence ( ( A = VERUM implies the Function of MP-WFF,F1() . A = F2() ) & ( for p being MP-variable st A = @ p holds
the Function of MP-WFF,F1() . A = F3(p) ) & ( for B being MP-wff st A = 'not' B holds
the Function of MP-WFF,F1() . A = F4(( the Function of MP-WFF,F1() . B)) ) & ( for B being MP-wff st A = (#) B holds
the Function of MP-WFF,F1() . A = F5(( the Function of MP-WFF,F1() . B)) ) & ( for B, C being MP-wff st A = B '&' C holds
the Function of MP-WFF,F1() . A = F6(( the Function of MP-WFF,F1() . B),( the Function of MP-WFF,F1() . C)) ) ) by NAT_1:2; :: thesis: verum
end;
A21: for n being Nat holds S3[n] from NAT_1:sch 2(A20, A1);
 A22: for x being object st x in MP-WFF holds
ex y being object st S4[x,y]
proof
let x be object ; :: thesis: ( x in MP-WFF implies ex y being object st S4[x,y] )
assume x in MP-WFF ; :: thesis: ex y being object st S4[x,y]
then reconsider x9 = x as Element of MP-WFF ;
consider F being Function of MP-WFF,F1() such that
A23: S1[F, card (dom x9)] by A21;
take F . x ; :: thesis: S4[x,F . x]
take x9 ; :: thesis: ( x9 = x & ( for g being Function of MP-WFF,F1() st S1[g, card (dom x9)] holds
F . x = g . x9 ) )
thus x = x9 ; :: thesis: for g being Function of MP-WFF,F1() st S1[g, card (dom x9)] holds
F . x = g . x9
let G be Function of MP-WFF,F1(); :: thesis: ( S1[G, card (dom x9)] implies F . x = G . x9 )
defpred S5[ Element of MP-WFF ] means ( card (dom $1) <= card (dom x9) implies F . $1 = G . $1 );
assume A24: S1[G, card (dom x9)] ; :: thesis: F . x = G . x9
A25: for p being MP-variable holds S5[ @ p]
proof
let p be MP-variable; :: thesis: S5[ @ p]
assume A26: card (dom (@ p)) <= card (dom x9) ; :: thesis: F . (@ p) = G . (@ p)
hence F . (@ p) = F3(p) by A23
.= G . (@ p) by A24, A26 ;
:: thesis: verum
end;
A27: for A, B being Element of MP-WFF st S5[A] & S5[B] holds
S5[A '&' B]
proof
let A, B be MP-wff; :: thesis: ( S5[A] & S5[B] implies S5[A '&' B] )
assume that
A28: ( S5[A] & S5[B] ) and
A29: card (dom (A '&' B)) <= card (dom x9) ; :: thesis: F . (A '&' B) = G . (A '&' B)
( card (dom A) < card (dom (A '&' B)) & card (dom B) < card (dom (A '&' B)) ) by Th35;
hence F . (A '&' B) = F6((G . A),(G . B)) by A23, A28, A29, XXREAL_0:2
.= G . (A '&' B) by A24, A29 ;
:: thesis: verum
end;
A30: for A being Element of MP-WFF st S5[A] holds
S5[ (#) A]
proof
let A be MP-wff; :: thesis: ( S5[A] implies S5[ (#) A] )
assume A31: S5[A] ; :: thesis: S5[ (#) A]
assume A32: card (dom ((#) A)) <= card (dom x9) ; :: thesis: F . ((#) A) = G . ((#) A)
card (dom A) < card (dom ((#) A)) by Th34;
hence F . ((#) A) = F5((G . A)) by A23, A31, A32, XXREAL_0:2
.= G . ((#) A) by A24, A32 ;
:: thesis: verum
end;
A33: for A being Element of MP-WFF st S5[A] holds
S5[ 'not' A]
proof
let A be MP-wff; :: thesis: ( S5[A] implies S5[ 'not' A] )
assume A34: S5[A] ; :: thesis: S5[ 'not' A]
assume A35: card (dom ('not' A)) <= card (dom x9) ; :: thesis: F . ('not' A) = G . ('not' A)
card (dom A) < card (dom ('not' A)) by Th33;
hence F . ('not' A) = F4((G . A)) by A23, A34, A35, XXREAL_0:2
.= G . ('not' A) by A24, A35 ;
:: thesis: verum
end;
A36: S5[ VERUM ]
proof
assume A37: card (dom VERUM) <= card (dom x9) ; :: thesis: F . VERUM = G . VERUM
hence F . VERUM = F2() by A23
.= G . VERUM by A24, A37 ;
:: thesis: verum
end;
for p being Element of MP-WFF holds S5[p] from MODAL_1:sch 1(A36, A25, A33, A30, A27);
 hence F . x = G . x9 ; :: thesis: verum
end;
consider F being Function such that
A38: dom F = MP-WFF and
A39: for x being object st x in MP-WFF holds
S4[x,F . x] from CLASSES1:sch 1(A22);
 rng F c= F1()
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng F or y in F1() )
assume y in rng F ; :: thesis: y in F1()
then consider x being object such that
A40: ( x in MP-WFF & y = F . x ) by A38, FUNCT_1:def 3;
consider p being Element of MP-WFF such that
p = x and
A41: for g being Function of MP-WFF,F1() st S1[g, card (dom p)] holds
y = g . p by A39, A40;
consider G being Function of MP-WFF,F1() such that
A42: S1[G, card (dom p)] by A21;
y = G . p by A41, A42;
hence y in F1() ; :: thesis: verum
end;
then reconsider F = F as Function of MP-WFF,F1() by A38, FUNCT_2:def 1, RELSET_1:4;
consider A being MP-wff such that
A43: A = VERUM and
A44: for g being Function of MP-WFF,F1() st S1[g, card (dom A)] holds
F . VERUM = g . A by A39;
take F ; :: thesis: ( F . VERUM = F2() & ( for p being MP-variable holds F . (@ p) = F3(p) ) & ( for A being Element of MP-WFF holds F . ('not' A) = F4((F . A)) ) & ( for A being Element of MP-WFF holds F . ((#) A) = F5((F . A)) ) & ( for A, B being Element of MP-WFF holds F . (A '&' B) = F6((F . A),(F . B)) ) )
consider G being Function of MP-WFF,F1() such that
A45: S1[G, card (dom A)] by A21;
F . VERUM = G . VERUM by A43, A44, A45;
hence F . VERUM = F2() by A43, A45; :: thesis: ( ( for p being MP-variable holds F . (@ p) = F3(p) ) & ( for A being Element of MP-WFF holds F . ('not' A) = F4((F . A)) ) & ( for A being Element of MP-WFF holds F . ((#) A) = F5((F . A)) ) & ( for A, B being Element of MP-WFF holds F . (A '&' B) = F6((F . A),(F . B)) ) )
thus for p being MP-variable holds F . (@ p) = F3(p) :: thesis: ( ( for A being Element of MP-WFF holds F . ('not' A) = F4((F . A)) ) & ( for A being Element of MP-WFF holds F . ((#) A) = F5((F . A)) ) & ( for A, B being Element of MP-WFF holds F . (A '&' B) = F6((F . A),(F . B)) ) )
proof
let p be MP-variable; :: thesis: F . (@ p) = F3(p)
consider A being MP-wff such that
A46: A = @ p and
A47: for g being Function of MP-WFF,F1() st S1[g, card (dom A)] holds
F . (@ p) = g . A by A39;
consider G being Function of MP-WFF,F1() such that
A48: S1[G, card (dom A)] by A21;
F . (@ p) = G . (@ p) by A46, A47, A48;
hence F . (@ p) = F3(p) by A46, A48; :: thesis: verum
end;
thus for A being Element of MP-WFF holds F . ('not' A) = F4((F . A)) :: thesis: ( ( for A being Element of MP-WFF holds F . ((#) A) = F5((F . A)) ) & ( for A, B being Element of MP-WFF holds F . (A '&' B) = F6((F . A),(F . B)) ) )
proof
let A be Element of MP-WFF ; :: thesis: F . ('not' A) = F4((F . A))
consider A1 being MP-wff such that
A49: A1 = 'not' A and
A50: for g being Function of MP-WFF,F1() st S1[g, card (dom A1)] holds
F . ('not' A) = g . A1 by A39;
consider G being Function of MP-WFF,F1() such that
A51: S1[G, card (dom A1)] by A21;
A52: for k being Nat st k < card (dom ('not' A)) holds
S1[G,k]
proof
let k be Nat; :: thesis: ( k < card (dom ('not' A)) implies S1[G,k] )
assume A53: k < card (dom ('not' A)) ; :: thesis: S1[G,k]
let a be Element of MP-WFF ; :: thesis: ( card (dom a) <= k implies ( ( a = VERUM implies G . a = F2() ) & ( for p being MP-variable st a = @ p holds
G . a = F3(p) ) & ( for B being MP-wff st a = 'not' B holds
G . a = F4((G . B)) ) & ( for B being MP-wff st a = (#) B holds
G . a = F5((G . B)) ) & ( for B, C being MP-wff st a = B '&' C holds
G . a = F6((G . B),(G . C)) ) ) )
assume card (dom a) <= k ; :: thesis: ( ( a = VERUM implies G . a = F2() ) & ( for p being MP-variable st a = @ p holds
G . a = F3(p) ) & ( for B being MP-wff st a = 'not' B holds
G . a = F4((G . B)) ) & ( for B being MP-wff st a = (#) B holds
G . a = F5((G . B)) ) & ( for B, C being MP-wff st a = B '&' C holds
G . a = F6((G . B),(G . C)) ) )
then card (dom a) <= card (dom ('not' A)) by A53, XXREAL_0:2;
hence ( ( a = VERUM implies G . a = F2() ) & ( for p being MP-variable st a = @ p holds
G . a = F3(p) ) & ( for B being MP-wff st a = 'not' B holds
G . a = F4((G . B)) ) & ( for B being MP-wff st a = (#) B holds
G . a = F5((G . B)) ) & ( for B, C being MP-wff st a = B '&' C holds
G . a = F6((G . B),(G . C)) ) ) by A49, A51; :: thesis: verum
end;
A54: ex B being MP-wff st
( B = A & ( for g being Function of MP-WFF,F1() st S1[g, card (dom B)] holds
F . A = g . B ) ) by A39;
set k = card (dom A);
card (dom A) < card (dom ('not' A)) by Th33;
then S1[G, card (dom A)] by A52;
then A55: F . A = G . A by A54;
F . ('not' A) = G . ('not' A) by A49, A50, A51;
hence F . ('not' A) = F4((F . A)) by A49, A51, A55; :: thesis: verum
end;
thus for A being Element of MP-WFF holds F . ((#) A) = F5((F . A)) :: thesis: for A, B being Element of MP-WFF holds F . (A '&' B) = F6((F . A),(F . B))
proof
let A be Element of MP-WFF ; :: thesis: F . ((#) A) = F5((F . A))
consider A1 being MP-wff such that
A56: A1 = (#) A and
A57: for g being Function of MP-WFF,F1() st S1[g, card (dom A1)] holds
F . ((#) A) = g . A1 by A39;
consider G being Function of MP-WFF,F1() such that
A58: S1[G, card (dom A1)] by A21;
A59: for k being Nat st k < card (dom ((#) A)) holds
S1[G,k]
proof
let k be Nat; :: thesis: ( k < card (dom ((#) A)) implies S1[G,k] )
assume A60: k < card (dom ((#) A)) ; :: thesis: S1[G,k]
let a be Element of MP-WFF ; :: thesis: ( card (dom a) <= k implies ( ( a = VERUM implies G . a = F2() ) & ( for p being MP-variable st a = @ p holds
G . a = F3(p) ) & ( for B being MP-wff st a = 'not' B holds
G . a = F4((G . B)) ) & ( for B being MP-wff st a = (#) B holds
G . a = F5((G . B)) ) & ( for B, C being MP-wff st a = B '&' C holds
G . a = F6((G . B),(G . C)) ) ) )
assume card (dom a) <= k ; :: thesis: ( ( a = VERUM implies G . a = F2() ) & ( for p being MP-variable st a = @ p holds
G . a = F3(p) ) & ( for B being MP-wff st a = 'not' B holds
G . a = F4((G . B)) ) & ( for B being MP-wff st a = (#) B holds
G . a = F5((G . B)) ) & ( for B, C being MP-wff st a = B '&' C holds
G . a = F6((G . B),(G . C)) ) )
then card (dom a) <= card (dom ((#) A)) by A60, XXREAL_0:2;
hence ( ( a = VERUM implies G . a = F2() ) & ( for p being MP-variable st a = @ p holds
G . a = F3(p) ) & ( for B being MP-wff st a = 'not' B holds
G . a = F4((G . B)) ) & ( for B being MP-wff st a = (#) B holds
G . a = F5((G . B)) ) & ( for B, C being MP-wff st a = B '&' C holds
G . a = F6((G . B),(G . C)) ) ) by A56, A58; :: thesis: verum
end;
A61: ex B being MP-wff st
( B = A & ( for g being Function of MP-WFF,F1() st S1[g, card (dom B)] holds
F . A = g . B ) ) by A39;
set k = card (dom A);
card (dom A) < card (dom ((#) A)) by Th34;
then S1[G, card (dom A)] by A59;
then A62: F . A = G . A by A61;
F . ((#) A) = G . ((#) A) by A56, A57, A58;
hence F . ((#) A) = F5((F . A)) by A56, A58, A62; :: thesis: verum
end;
thus for A, B being Element of MP-WFF holds F . (A '&' B) = F6((F . A),(F . B)) :: thesis: verum
proof
let A, B be Element of MP-WFF ; :: thesis: F . (A '&' B) = F6((F . A),(F . B))
set k1 = card (dom A);
set k2 = card (dom B);
consider A1 being MP-wff such that
A63: A1 = A '&' B and
A64: for g being Function of MP-WFF,F1() st S1[g, card (dom A1)] holds
F . (A '&' B) = g . A1 by A39;
consider G being Function of MP-WFF,F1() such that
A65: S1[G, card (dom A1)] by A21;
A66: for k being Nat st k < card (dom (A '&' B)) holds
S1[G,k]
proof
let k be Nat; :: thesis: ( k < card (dom (A '&' B)) implies S1[G,k] )
assume A67: k < card (dom (A '&' B)) ; :: thesis: S1[G,k]
let a be Element of MP-WFF ; :: thesis: ( card (dom a) <= k implies ( ( a = VERUM implies G . a = F2() ) & ( for p being MP-variable st a = @ p holds
G . a = F3(p) ) & ( for B being MP-wff st a = 'not' B holds
G . a = F4((G . B)) ) & ( for B being MP-wff st a = (#) B holds
G . a = F5((G . B)) ) & ( for B, C being MP-wff st a = B '&' C holds
G . a = F6((G . B),(G . C)) ) ) )
assume card (dom a) <= k ; :: thesis: ( ( a = VERUM implies G . a = F2() ) & ( for p being MP-variable st a = @ p holds
G . a = F3(p) ) & ( for B being MP-wff st a = 'not' B holds
G . a = F4((G . B)) ) & ( for B being MP-wff st a = (#) B holds
G . a = F5((G . B)) ) & ( for B, C being MP-wff st a = B '&' C holds
G . a = F6((G . B),(G . C)) ) )
then card (dom a) <= card (dom (A '&' B)) by A67, XXREAL_0:2;
hence ( ( a = VERUM implies G . a = F2() ) & ( for p being MP-variable st a = @ p holds
G . a = F3(p) ) & ( for B being MP-wff st a = 'not' B holds
G . a = F4((G . B)) ) & ( for B being MP-wff st a = (#) B holds
G . a = F5((G . B)) ) & ( for B, C being MP-wff st a = B '&' C holds
G . a = F6((G . B),(G . C)) ) ) by A63, A65; :: thesis: verum
end;
A68: ex B1 being MP-wff st
( B1 = A & ( for g being Function of MP-WFF,F1() st S1[g, card (dom B1)] holds
F . A = g . B1 ) ) by A39;
card (dom A) < card (dom (A '&' B)) by Th35;
then S1[G, card (dom A)] by A66;
then A69: F . A = G . A by A68;
A70: ex C being MP-wff st
( C = B & ( for g being Function of MP-WFF,F1() st S1[g, card (dom C)] holds
F . B = g . C ) ) by A39;
card (dom B) < card (dom (A '&' B)) by Th35;
then S1[G, card (dom B)] by A66;
then A71: F . B = G . B by A70;
F . (A '&' B) = G . (A '&' B) by A63, A64, A65;
hence F . (A '&' B) = F6((F . A),(F . B)) by A63, A65, A69, A71; :: thesis: verum
end;