defpred S1[ Function of (QC-Sub-WFF F1()),F2(), Nat] means for S being Element of QC-Sub-WFF F1() st len (@ (S `1)) <= $2 holds
( ( S is F1() -Sub_VERUM implies $1 . S = F3() ) & ( S is Sub_atomic implies $1 . S = F4(S) ) & ( S is Sub_negative implies $1 . S = F5(($1 . (Sub_the_argument_of S))) ) & ( S is Sub_conjunctive implies $1 . S = F6(($1 . (Sub_the_left_argument_of S)),($1 . (Sub_the_right_argument_of S))) ) & ( S is Sub_universal implies $1 . S = F7(F1(),S,($1 . (Sub_the_scope_of S))) ) );
defpred S2[ Element of F2(), Function of (QC-Sub-WFF F1()),F2(), Element of QC-Sub-WFF F1()] means ( ( $3 is F1() -Sub_VERUM implies $1 = F3() ) & ( $3 is Sub_atomic implies $1 = F4($3) ) & ( $3 is Sub_negative implies $1 = F5(($2 . (Sub_the_argument_of $3))) ) & ( $3 is Sub_conjunctive implies $1 = F6(($2 . (Sub_the_left_argument_of $3)),($2 . (Sub_the_right_argument_of $3))) ) & ( $3 is Sub_universal implies $1 = F7(F1(),$3,($2 . (Sub_the_scope_of $3))) ) );
defpred S3[ Nat] means ex F being Function of (QC-Sub-WFF F1()),F2() st S1[F,$1];
defpred S4[ object , object ] means ex S being Element of QC-Sub-WFF F1() st
( S = $1 & ( for g being Function of (QC-Sub-WFF F1()),F2() st S1[g, len (@ (S `1))] holds
$2 = g . S ) );
A1: for n being Nat st S3[n] holds
S3[n + 1]
proof
let n be Nat; :: thesis: ( S3[n] implies S3[n + 1] )
given F being Function of (QC-Sub-WFF F1()),F2() such that A2: S1[F,n] ; :: thesis: S3[n + 1]
defpred S5[ Element of QC-Sub-WFF F1(), Element of F2()] means ( ( len (@ ($1 `1)) <> n + 1 implies $2 = F . $1 ) & ( len (@ ($1 `1)) = n + 1 implies S2[$2,F,$1] ) );
A3: for S being Element of QC-Sub-WFF F1() ex y being Element of F2() st S5[S,y]
proof
let S be Element of QC-Sub-WFF F1(); :: thesis: ex y being Element of F2() st S5[S,y]
now :: thesis: ( ( len (@ (S `1)) <> n + 1 & ex y being Element of F2() st y = F . S ) or ( len (@ (S `1)) = n + 1 & S is F1() -Sub_VERUM & ex y being Element of F2() st S2[y,F,S] ) or ( len (@ (S `1)) = n + 1 & S is Sub_atomic & ex y being Element of F2() st S2[y,F,S] ) or ( len (@ (S `1)) = n + 1 & S is Sub_negative & ex y being Element of F2() st S2[y,F,S] ) or ( len (@ (S `1)) = n + 1 & S is Sub_conjunctive & ex y being Element of F2() st S2[y,F,S] ) or ( len (@ (S `1)) = n + 1 & S is Sub_universal & ex y being Element of F2() st S2[y,F,S] ) )
per cases ( len (@ (S `1)) <> n + 1 or ( len (@ (S `1)) = n + 1 & S is F1() -Sub_VERUM ) or ( len (@ (S `1)) = n + 1 & S is Sub_atomic ) or ( len (@ (S `1)) = n + 1 & S is Sub_negative ) or ( len (@ (S `1)) = n + 1 & S is Sub_conjunctive ) or ( len (@ (S `1)) = n + 1 & S is Sub_universal ) ) by Th12;
case len (@ (S `1)) <> n + 1 ; :: thesis: ex y being Element of F2() st y = F . S
take y = F . S; :: thesis: y = F . S
thus y = F . S ; :: thesis: verum
end;
case A4: ( len (@ (S `1)) = n + 1 & S is F1() -Sub_VERUM ) ; :: thesis: ex y being Element of F2() st S2[y,F,S]
take y = F3(); :: thesis: S2[y,F,S]
thus S2[y,F,S] by A4, Th27; :: thesis: verum
end;
case A5: ( len (@ (S `1)) = n + 1 & S is Sub_atomic ) ; :: thesis: ex y being Element of F2() st S2[y,F,S]
take y = F4(S); :: thesis: S2[y,F,S]
thus S2[y,F,S] by A5, Th27; :: thesis: verum
end;
case A6: ( len (@ (S `1)) = n + 1 & S is Sub_negative ) ; :: thesis: ex y being Element of F2() st S2[y,F,S]
take y = F5((F . (Sub_the_argument_of S))); :: thesis: S2[y,F,S]
thus S2[y,F,S] by A6, Th27; :: thesis: verum
end;
case A7: ( len (@ (S `1)) = n + 1 & S is Sub_conjunctive ) ; :: thesis: ex y being Element of F2() st S2[y,F,S]
take y = F6((F . (Sub_the_left_argument_of S)),(F . (Sub_the_right_argument_of S))); :: thesis: S2[y,F,S]
thus S2[y,F,S] by A7, Th27; :: thesis: verum
end;
case A8: ( len (@ (S `1)) = n + 1 & S is Sub_universal ) ; :: thesis: ex y being Element of F2() st S2[y,F,S]
take y = F7(F1(),S,(F . (Sub_the_scope_of S))); :: thesis: S2[y,F,S]
thus S2[y,F,S] by A8, Th27; :: thesis: verum
end;
end;
end;
hence ex y being Element of F2() st S5[S,y] ; :: thesis: verum
end;
consider G being Function of (QC-Sub-WFF F1()),F2() such that
A9: for S being Element of QC-Sub-WFF F1() holds S5[S,G . S] from FUNCT_2:sch 3(A3);
 take H = G; :: thesis: S1[H,n + 1]
thus S1[H,n + 1] :: thesis: verum
proof
let S be Element of QC-Sub-WFF F1(); :: thesis: ( len (@ (S `1)) <= n + 1 implies ( ( S is F1() -Sub_VERUM implies H . S = F3() ) & ( S is Sub_atomic implies H . S = F4(S) ) & ( S is Sub_negative implies H . S = F5((H . (Sub_the_argument_of S))) ) & ( S is Sub_conjunctive implies H . S = F6((H . (Sub_the_left_argument_of S)),(H . (Sub_the_right_argument_of S))) ) & ( S is Sub_universal implies H . S = F7(F1(),S,(H . (Sub_the_scope_of S))) ) ) )
assume A10: len (@ (S `1)) <= n + 1 ; :: thesis: ( ( S is F1() -Sub_VERUM implies H . S = F3() ) & ( S is Sub_atomic implies H . S = F4(S) ) & ( S is Sub_negative implies H . S = F5((H . (Sub_the_argument_of S))) ) & ( S is Sub_conjunctive implies H . S = F6((H . (Sub_the_left_argument_of S)),(H . (Sub_the_right_argument_of S))) ) & ( S is Sub_universal implies H . S = F7(F1(),S,(H . (Sub_the_scope_of S))) ) )
thus ( S is F1() -Sub_VERUM implies H . S = F3() ) :: thesis: ( ( S is Sub_atomic implies H . S = F4(S) ) & ( S is Sub_negative implies H . S = F5((H . (Sub_the_argument_of S))) ) & ( S is Sub_conjunctive implies H . S = F6((H . (Sub_the_left_argument_of S)),(H . (Sub_the_right_argument_of S))) ) & ( S is Sub_universal implies H . S = F7(F1(),S,(H . (Sub_the_scope_of S))) ) )
proof
now :: thesis: ( S is F1() -Sub_VERUM implies H . S = F3() )
per cases ( len (@ (S `1)) <> n + 1 or len (@ (S `1)) = n + 1 ) ;
suppose len (@ (S `1)) <> n + 1 ; :: thesis: ( S is F1() -Sub_VERUM implies H . S = F3() )
then ( len (@ (S `1)) <= n & H . S = F . S ) by A9, A10, NAT_1:8;
hence ( S is F1() -Sub_VERUM implies H . S = F3() ) by A2; :: thesis: verum
end;
suppose len (@ (S `1)) = n + 1 ; :: thesis: ( S is F1() -Sub_VERUM implies H . S = F3() )
hence ( S is F1() -Sub_VERUM implies H . S = F3() ) by A9; :: thesis: verum
end;
end;
end;
hence ( S is F1() -Sub_VERUM implies H . S = F3() ) ; :: thesis: verum
end;
thus ( S is Sub_atomic implies H . S = F4(S) ) :: thesis: ( ( S is Sub_negative implies H . S = F5((H . (Sub_the_argument_of S))) ) & ( S is Sub_conjunctive implies H . S = F6((H . (Sub_the_left_argument_of S)),(H . (Sub_the_right_argument_of S))) ) & ( S is Sub_universal implies H . S = F7(F1(),S,(H . (Sub_the_scope_of S))) ) )
proof
now :: thesis: ( S is Sub_atomic implies H . S = F4(S) )
per cases ( len (@ (S `1)) <> n + 1 or len (@ (S `1)) = n + 1 ) ;
suppose len (@ (S `1)) <> n + 1 ; :: thesis: ( S is Sub_atomic implies H . S = F4(S) )
then ( len (@ (S `1)) <= n & H . S = F . S ) by A9, A10, NAT_1:8;
hence ( S is Sub_atomic implies H . S = F4(S) ) by A2; :: thesis: verum
end;
suppose len (@ (S `1)) = n + 1 ; :: thesis: ( S is Sub_atomic implies H . S = F4(S) )
hence ( S is Sub_atomic implies H . S = F4(S) ) by A9; :: thesis: verum
end;
end;
end;
hence ( S is Sub_atomic implies H . S = F4(S) ) ; :: thesis: verum
end;
thus ( S is Sub_negative implies H . S = F5((H . (Sub_the_argument_of S))) ) :: thesis: ( ( S is Sub_conjunctive implies H . S = F6((H . (Sub_the_left_argument_of S)),(H . (Sub_the_right_argument_of S))) ) & ( S is Sub_universal implies H . S = F7(F1(),S,(H . (Sub_the_scope_of S))) ) )
proof
assume A11: S is Sub_negative ; :: thesis: H . S = F5((H . (Sub_the_argument_of S)))
then len (@ ((Sub_the_argument_of S) `1)) <> n + 1 by A10, Th22;
then A12: H . (Sub_the_argument_of S) = F . (Sub_the_argument_of S) by A9;
now :: thesis: H . S = F5((H . (Sub_the_argument_of S)))
per cases ( len (@ (S `1)) <> n + 1 or len (@ (S `1)) = n + 1 ) ;
suppose len (@ (S `1)) <> n + 1 ; :: thesis: H . S = F5((H . (Sub_the_argument_of S)))
then ( len (@ (S `1)) <= n & H . S = F . S ) by A9, A10, NAT_1:8;
hence H . S = F5((H . (Sub_the_argument_of S))) by A2, A11, A12; :: thesis: verum
end;
suppose len (@ (S `1)) = n + 1 ; :: thesis: H . S = F5((H . (Sub_the_argument_of S)))
hence H . S = F5((H . (Sub_the_argument_of S))) by A9, A11, A12; :: thesis: verum
end;
end;
end;
hence H . S = F5((H . (Sub_the_argument_of S))) ; :: thesis: verum
end;
thus ( S is Sub_conjunctive implies H . S = F6((H . (Sub_the_left_argument_of S)),(H . (Sub_the_right_argument_of S))) ) :: thesis: ( S is Sub_universal implies H . S = F7(F1(),S,(H . (Sub_the_scope_of S))) )
proof
assume A13: S is Sub_conjunctive ; :: thesis: H . S = F6((H . (Sub_the_left_argument_of S)),(H . (Sub_the_right_argument_of S)))
then len (@ ((Sub_the_right_argument_of S) `1)) <> n + 1 by A10, Th23;
then A14: H . (Sub_the_right_argument_of S) = F . (Sub_the_right_argument_of S) by A9;
len (@ ((Sub_the_left_argument_of S) `1)) <> n + 1 by A10, A13, Th23;
then A15: H . (Sub_the_left_argument_of S) = F . (Sub_the_left_argument_of S) by A9;
now :: thesis: H . S = F6((H . (Sub_the_left_argument_of S)),(H . (Sub_the_right_argument_of S)))
per cases ( len (@ (S `1)) <> n + 1 or len (@ (S `1)) = n + 1 ) ;
suppose len (@ (S `1)) <> n + 1 ; :: thesis: H . S = F6((H . (Sub_the_left_argument_of S)),(H . (Sub_the_right_argument_of S)))
then ( len (@ (S `1)) <= n & H . S = F . S ) by A9, A10, NAT_1:8;
hence H . S = F6((H . (Sub_the_left_argument_of S)),(H . (Sub_the_right_argument_of S))) by A2, A13, A15, A14; :: thesis: verum
end;
end;
end;
hence H . S = F6((H . (Sub_the_left_argument_of S)),(H . (Sub_the_right_argument_of S))) ; :: thesis: verum
end;
thus ( S is Sub_universal implies H . S = F7(F1(),S,(H . (Sub_the_scope_of S))) ) :: thesis: verum
proof
assume A16: S is Sub_universal ; :: thesis: H . S = F7(F1(),S,(H . (Sub_the_scope_of S)))
then len (@ ((Sub_the_scope_of S) `1)) <> n + 1 by A10, Th24;
then A17: H . (Sub_the_scope_of S) = F . (Sub_the_scope_of S) by A9;
now :: thesis: H . S = F7(F1(),S,(H . (Sub_the_scope_of S)))
per cases ( len (@ (S `1)) <> n + 1 or len (@ (S `1)) = n + 1 ) ;
suppose len (@ (S `1)) <> n + 1 ; :: thesis: H . S = F7(F1(),S,(H . (Sub_the_scope_of S)))
then ( len (@ (S `1)) <= n & H . S = F . S ) by A9, A10, NAT_1:8;
hence H . S = F7(F1(),S,(H . (Sub_the_scope_of S))) by A2, A16, A17; :: thesis: verum
end;
suppose len (@ (S `1)) = n + 1 ; :: thesis: H . S = F7(F1(),S,(H . (Sub_the_scope_of S)))
hence H . S = F7(F1(),S,(H . (Sub_the_scope_of S))) by A9, A16, A17; :: thesis: verum
end;
end;
end;
hence H . S = F7(F1(),S,(H . (Sub_the_scope_of S))) ; :: thesis: verum
end;
end;
end;
A18: S3[ 0 ]
proof
set F = the Function of (QC-Sub-WFF F1()),F2();
take the Function of (QC-Sub-WFF F1()),F2() ; :: thesis: S1[ the Function of (QC-Sub-WFF F1()),F2(), 0 ]
let S be Element of QC-Sub-WFF F1(); :: thesis: ( len (@ (S `1)) <= 0 implies ( ( S is F1() -Sub_VERUM implies the Function of (QC-Sub-WFF F1()),F2() . S = F3() ) & ( S is Sub_atomic implies the Function of (QC-Sub-WFF F1()),F2() . S = F4(S) ) & ( S is Sub_negative implies the Function of (QC-Sub-WFF F1()),F2() . S = F5(( the Function of (QC-Sub-WFF F1()),F2() . (Sub_the_argument_of S))) ) & ( S is Sub_conjunctive implies the Function of (QC-Sub-WFF F1()),F2() . S = F6(( the Function of (QC-Sub-WFF F1()),F2() . (Sub_the_left_argument_of S)),( the Function of (QC-Sub-WFF F1()),F2() . (Sub_the_right_argument_of S))) ) & ( S is Sub_universal implies the Function of (QC-Sub-WFF F1()),F2() . S = F7(F1(),S,( the Function of (QC-Sub-WFF F1()),F2() . (Sub_the_scope_of S))) ) ) )
assume len (@ (S `1)) <= 0 ; :: thesis: ( ( S is F1() -Sub_VERUM implies the Function of (QC-Sub-WFF F1()),F2() . S = F3() ) & ( S is Sub_atomic implies the Function of (QC-Sub-WFF F1()),F2() . S = F4(S) ) & ( S is Sub_negative implies the Function of (QC-Sub-WFF F1()),F2() . S = F5(( the Function of (QC-Sub-WFF F1()),F2() . (Sub_the_argument_of S))) ) & ( S is Sub_conjunctive implies the Function of (QC-Sub-WFF F1()),F2() . S = F6(( the Function of (QC-Sub-WFF F1()),F2() . (Sub_the_left_argument_of S)),( the Function of (QC-Sub-WFF F1()),F2() . (Sub_the_right_argument_of S))) ) & ( S is Sub_universal implies the Function of (QC-Sub-WFF F1()),F2() . S = F7(F1(),S,( the Function of (QC-Sub-WFF F1()),F2() . (Sub_the_scope_of S))) ) )
hence ( ( S is F1() -Sub_VERUM implies the Function of (QC-Sub-WFF F1()),F2() . S = F3() ) & ( S is Sub_atomic implies the Function of (QC-Sub-WFF F1()),F2() . S = F4(S) ) & ( S is Sub_negative implies the Function of (QC-Sub-WFF F1()),F2() . S = F5(( the Function of (QC-Sub-WFF F1()),F2() . (Sub_the_argument_of S))) ) & ( S is Sub_conjunctive implies the Function of (QC-Sub-WFF F1()),F2() . S = F6(( the Function of (QC-Sub-WFF F1()),F2() . (Sub_the_left_argument_of S)),( the Function of (QC-Sub-WFF F1()),F2() . (Sub_the_right_argument_of S))) ) & ( S is Sub_universal implies the Function of (QC-Sub-WFF F1()),F2() . S = F7(F1(),S,( the Function of (QC-Sub-WFF F1()),F2() . (Sub_the_scope_of S))) ) ) by QC_LANG1:10; :: thesis: verum
end;
A19: for n being Nat holds S3[n] from NAT_1:sch 2(A18, A1);
 A20: for x being object st x in QC-Sub-WFF F1() holds
ex y being object st S4[x,y]
proof
let x be object ; :: thesis: ( x in QC-Sub-WFF F1() implies ex y being object st S4[x,y] )
assume x in QC-Sub-WFF F1() ; :: thesis: ex y being object st S4[x,y]
then reconsider x9 = x as Element of QC-Sub-WFF F1() ;
consider F being Function of (QC-Sub-WFF F1()),F2() such that
A21: S1[F, len (@ (x9 `1))] by A19;
take F . x ; :: thesis: S4[x,F . x]
take x9 ; :: thesis: ( x9 = x & ( for g being Function of (QC-Sub-WFF F1()),F2() st S1[g, len (@ (x9 `1))] holds
F . x = g . x9 ) )
thus x9 = x ; :: thesis: for g being Function of (QC-Sub-WFF F1()),F2() st S1[g, len (@ (x9 `1))] holds
F . x = g . x9
let G be Function of (QC-Sub-WFF F1()),F2(); :: thesis: ( S1[G, len (@ (x9 `1))] implies F . x = G . x9 )
assume A22: S1[G, len (@ (x9 `1))] ; :: thesis: F . x = G . x9
defpred S5[ Element of QC-Sub-WFF F1()] means ( len (@ ($1 `1)) <= len (@ (x9 `1)) implies F . $1 = G . $1 );
A23: now :: thesis: for S being Element of QC-Sub-WFF F1() holds
( ( S is Sub_atomic implies S5[S] ) & ( S is F1() -Sub_VERUM implies S5[S] ) & ( S is Sub_negative & S5[ Sub_the_argument_of S] implies S5[S] ) & ( S is Sub_conjunctive & S5[ Sub_the_left_argument_of S] & S5[ Sub_the_right_argument_of S] implies S5[S] ) & ( S is Sub_universal & S5[ Sub_the_scope_of S] implies S5[S] ) )
let S be Element of QC-Sub-WFF F1(); :: thesis: ( ( S is Sub_atomic implies S5[S] ) & ( S is F1() -Sub_VERUM implies S5[S] ) & ( S is Sub_negative & S5[ Sub_the_argument_of S] implies S5[S] ) & ( S is Sub_conjunctive & S5[ Sub_the_left_argument_of S] & S5[ Sub_the_right_argument_of S] implies S5[S] ) & ( S is Sub_universal & S5[ Sub_the_scope_of S] implies S5[S] ) )
thus ( S is Sub_atomic implies S5[S] ) :: thesis: ( ( S is F1() -Sub_VERUM implies S5[S] ) & ( S is Sub_negative & S5[ Sub_the_argument_of S] implies S5[S] ) & ( S is Sub_conjunctive & S5[ Sub_the_left_argument_of S] & S5[ Sub_the_right_argument_of S] implies S5[S] ) & ( S is Sub_universal & S5[ Sub_the_scope_of S] implies S5[S] ) )
proof
assume A24: ( S is Sub_atomic & len (@ (S `1)) <= len (@ (x9 `1)) ) ; :: thesis: F . S = G . S
hence F . S = F4(S) by A21
.= G . S by A22, A24 ;
:: thesis: verum
end;
thus ( S is F1() -Sub_VERUM implies S5[S] ) :: thesis: ( ( S is Sub_negative & S5[ Sub_the_argument_of S] implies S5[S] ) & ( S is Sub_conjunctive & S5[ Sub_the_left_argument_of S] & S5[ Sub_the_right_argument_of S] implies S5[S] ) & ( S is Sub_universal & S5[ Sub_the_scope_of S] implies S5[S] ) )
proof
assume A25: ( S is F1() -Sub_VERUM & len (@ (S `1)) <= len (@ (x9 `1)) ) ; :: thesis: F . S = G . S
hence F . S = F3() by A21
.= G . S by A22, A25 ;
:: thesis: verum
end;
thus ( S is Sub_negative & S5[ Sub_the_argument_of S] implies S5[S] ) :: thesis: ( ( S is Sub_conjunctive & S5[ Sub_the_left_argument_of S] & S5[ Sub_the_right_argument_of S] implies S5[S] ) & ( S is Sub_universal & S5[ Sub_the_scope_of S] implies S5[S] ) )
proof
assume that
A26: S is Sub_negative and
A27: S5[ Sub_the_argument_of S] and
A28: len (@ (S `1)) <= len (@ (x9 `1)) ; :: thesis: F . S = G . S
len (@ ((Sub_the_argument_of S) `1)) < len (@ (S `1)) by A26, Th22;
hence F . S = F5((G . (Sub_the_argument_of S))) by A21, A26, A27, A28, XXREAL_0:2
.= G . S by A22, A26, A28 ;
:: thesis: verum
end;
thus ( S is Sub_conjunctive & S5[ Sub_the_left_argument_of S] & S5[ Sub_the_right_argument_of S] implies S5[S] ) :: thesis: ( S is Sub_universal & S5[ Sub_the_scope_of S] implies S5[S] )thus ( S is Sub_universal & S5[ Sub_the_scope_of S] implies S5[S] ) :: thesis: verum
proof
assume that
A32: S is Sub_universal and
A33: S5[ Sub_the_scope_of S] and
A34: len (@ (S `1)) <= len (@ (x9 `1)) ; :: thesis: F . S = G . S
len (@ ((Sub_the_scope_of S) `1)) < len (@ (S `1)) by A32, Th24;
hence F . S = F7(F1(),S,(G . (Sub_the_scope_of S))) by A21, A32, A33, A34, XXREAL_0:2
.= G . S by A22, A32, A34 ;
:: thesis: verum
end;
end;
for S being Element of QC-Sub-WFF F1() holds S5[S] from SUBSTUT1:sch 2(A23);
 hence F . x = G . x9 ; :: thesis: verum
end;
consider F being Function such that
A35: dom F = QC-Sub-WFF F1() and
A36: for x being object st x in QC-Sub-WFF F1() holds
S4[x,F . x] from CLASSES1:sch 1(A20);
 rng F c= F2()
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng F or y in F2() )
assume y in rng F ; :: thesis: y in F2()
then consider x being object such that
A37: ( x in QC-Sub-WFF F1() & y = F . x ) by A35, FUNCT_1:def 3;
consider S being Element of QC-Sub-WFF F1() such that
S = x and
A38: for g being Function of (QC-Sub-WFF F1()),F2() st S1[g, len (@ (S `1))] holds
y = g . S by A36, A37;
consider G being Function of (QC-Sub-WFF F1()),F2() such that
A39: S1[G, len (@ (S `1))] by A19;
y = G . S by A38, A39;
hence y in F2() ; :: thesis: verum
end;
then reconsider F = F as Function of (QC-Sub-WFF F1()),F2() by A35, FUNCT_2:def 1, RELSET_1:4;
take F ; :: thesis: for S being Element of QC-Sub-WFF F1()
for d1, d2 being Element of F2() holds
( ( S is F1() -Sub_VERUM implies F . S = F3() ) & ( S is Sub_atomic implies F . S = F4(S) ) & ( S is Sub_negative & d1 = F . (Sub_the_argument_of S) implies F . S = F5(d1) ) & ( S is Sub_conjunctive & d1 = F . (Sub_the_left_argument_of S) & d2 = F . (Sub_the_right_argument_of S) implies F . S = F6(d1,d2) ) & ( S is Sub_universal & d1 = F . (Sub_the_scope_of S) implies F . S = F7(F1(),S,d1) ) )
let S be Element of QC-Sub-WFF F1(); :: thesis: for d1, d2 being Element of F2() holds
( ( S is F1() -Sub_VERUM implies F . S = F3() ) & ( S is Sub_atomic implies F . S = F4(S) ) & ( S is Sub_negative & d1 = F . (Sub_the_argument_of S) implies F . S = F5(d1) ) & ( S is Sub_conjunctive & d1 = F . (Sub_the_left_argument_of S) & d2 = F . (Sub_the_right_argument_of S) implies F . S = F6(d1,d2) ) & ( S is Sub_universal & d1 = F . (Sub_the_scope_of S) implies F . S = F7(F1(),S,d1) ) )
consider S1 being Element of QC-Sub-WFF F1() such that
A40: S1 = S and
A41: for g being Function of (QC-Sub-WFF F1()),F2() st S1[g, len (@ (S1 `1))] holds
F . S = g . S1 by A36;
let d1, d2 be Element of F2(); :: thesis: ( ( S is F1() -Sub_VERUM implies F . S = F3() ) & ( S is Sub_atomic implies F . S = F4(S) ) & ( S is Sub_negative & d1 = F . (Sub_the_argument_of S) implies F . S = F5(d1) ) & ( S is Sub_conjunctive & d1 = F . (Sub_the_left_argument_of S) & d2 = F . (Sub_the_right_argument_of S) implies F . S = F6(d1,d2) ) & ( S is Sub_universal & d1 = F . (Sub_the_scope_of S) implies F . S = F7(F1(),S,d1) ) )
consider G being Function of (QC-Sub-WFF F1()),F2() such that
A42: S1[G, len (@ (S1 `1))] by A19;
set S9 = Sub_the_scope_of S;
A43: ex S1 being Element of QC-Sub-WFF F1() st
( S1 = Sub_the_scope_of S & ( for g being Function of (QC-Sub-WFF F1()),F2() st S1[g, len (@ (S1 `1))] holds
F . (Sub_the_scope_of S) = g . S1 ) ) by A36;
A44: F . S = G . S by A40, A41, A42;
hence ( S is F1() -Sub_VERUM implies F . S = F3() ) by A40, A42; :: thesis: ( ( S is Sub_atomic implies F . S = F4(S) ) & ( S is Sub_negative & d1 = F . (Sub_the_argument_of S) implies F . S = F5(d1) ) & ( S is Sub_conjunctive & d1 = F . (Sub_the_left_argument_of S) & d2 = F . (Sub_the_right_argument_of S) implies F . S = F6(d1,d2) ) & ( S is Sub_universal & d1 = F . (Sub_the_scope_of S) implies F . S = F7(F1(),S,d1) ) )
thus ( S is Sub_atomic implies F . S = F4(S) ) by A40, A42, A44; :: thesis: ( ( S is Sub_negative & d1 = F . (Sub_the_argument_of S) implies F . S = F5(d1) ) & ( S is Sub_conjunctive & d1 = F . (Sub_the_left_argument_of S) & d2 = F . (Sub_the_right_argument_of S) implies F . S = F6(d1,d2) ) & ( S is Sub_universal & d1 = F . (Sub_the_scope_of S) implies F . S = F7(F1(),S,d1) ) )
A45: for k being Nat st k < len (@ (S `1)) holds
S1[G,k]
proof
let k be Nat; :: thesis: ( k < len (@ (S `1)) implies S1[G,k] )
assume A46: k < len (@ (S `1)) ; :: thesis: S1[G,k]
let S9 be Element of QC-Sub-WFF F1(); :: thesis: ( len (@ (S9 `1)) <= k implies ( ( S9 is F1() -Sub_VERUM implies G . S9 = F3() ) & ( S9 is Sub_atomic implies G . S9 = F4(S9) ) & ( S9 is Sub_negative implies G . S9 = F5((G . (Sub_the_argument_of S9))) ) & ( S9 is Sub_conjunctive implies G . S9 = F6((G . (Sub_the_left_argument_of S9)),(G . (Sub_the_right_argument_of S9))) ) & ( S9 is Sub_universal implies G . S9 = F7(F1(),S9,(G . (Sub_the_scope_of S9))) ) ) )
assume len (@ (S9 `1)) <= k ; :: thesis: ( ( S9 is F1() -Sub_VERUM implies G . S9 = F3() ) & ( S9 is Sub_atomic implies G . S9 = F4(S9) ) & ( S9 is Sub_negative implies G . S9 = F5((G . (Sub_the_argument_of S9))) ) & ( S9 is Sub_conjunctive implies G . S9 = F6((G . (Sub_the_left_argument_of S9)),(G . (Sub_the_right_argument_of S9))) ) & ( S9 is Sub_universal implies G . S9 = F7(F1(),S9,(G . (Sub_the_scope_of S9))) ) )
then len (@ (S9 `1)) <= len (@ (S `1)) by A46, XXREAL_0:2;
hence ( ( S9 is F1() -Sub_VERUM implies G . S9 = F3() ) & ( S9 is Sub_atomic implies G . S9 = F4(S9) ) & ( S9 is Sub_negative implies G . S9 = F5((G . (Sub_the_argument_of S9))) ) & ( S9 is Sub_conjunctive implies G . S9 = F6((G . (Sub_the_left_argument_of S9)),(G . (Sub_the_right_argument_of S9))) ) & ( S9 is Sub_universal implies G . S9 = F7(F1(),S9,(G . (Sub_the_scope_of S9))) ) ) by A40, A42; :: thesis: verum
end;
thus ( S is Sub_negative & d1 = F . (Sub_the_argument_of S) implies F . S = F5(d1) ) :: thesis: ( ( S is Sub_conjunctive & d1 = F . (Sub_the_left_argument_of S) & d2 = F . (Sub_the_right_argument_of S) implies F . S = F6(d1,d2) ) & ( S is Sub_universal & d1 = F . (Sub_the_scope_of S) implies F . S = F7(F1(),S,d1) ) )
proof
set S9 = Sub_the_argument_of S;
set k = len (@ ((Sub_the_argument_of S) `1));
A47: ex S1 being Element of QC-Sub-WFF F1() st
( S1 = Sub_the_argument_of S & ( for g being Function of (QC-Sub-WFF F1()),F2() st S1[g, len (@ (S1 `1))] holds
F . (Sub_the_argument_of S) = g . S1 ) ) by A36;
assume A48: S is Sub_negative ; :: thesis: ( not d1 = F . (Sub_the_argument_of S) or F . S = F5(d1) )
then len (@ ((Sub_the_argument_of S) `1)) < len (@ (S `1)) by Th22;
then S1[G, len (@ ((Sub_the_argument_of S) `1))] by A45;
then F . (Sub_the_argument_of S) = G . (Sub_the_argument_of S) by A47;
hence ( not d1 = F . (Sub_the_argument_of S) or F . S = F5(d1) ) by A40, A42, A44, A48; :: thesis: verum
end;
thus ( S is Sub_conjunctive & d1 = F . (Sub_the_left_argument_of S) & d2 = F . (Sub_the_right_argument_of S) implies F . S = F6(d1,d2) ) :: thesis: ( S is Sub_universal & d1 = F . (Sub_the_scope_of S) implies F . S = F7(F1(),S,d1) )
proof
set S99 = Sub_the_right_argument_of S;
set S9 = Sub_the_left_argument_of S;
set k9 = len (@ ((Sub_the_left_argument_of S) `1));
set k99 = len (@ ((Sub_the_right_argument_of S) `1));
A49: ex S2 being Element of QC-Sub-WFF F1() st
( S2 = Sub_the_right_argument_of S & ( for g being Function of (QC-Sub-WFF F1()),F2() st S1[g, len (@ (S2 `1))] holds
F . (Sub_the_right_argument_of S) = g . S2 ) ) by A36;
assume A50: S is Sub_conjunctive ; :: thesis: ( not d1 = F . (Sub_the_left_argument_of S) or not d2 = F . (Sub_the_right_argument_of S) or F . S = F6(d1,d2) )
then len (@ ((Sub_the_left_argument_of S) `1)) < len (@ (S `1)) by Th23;
then A51: S1[G, len (@ ((Sub_the_left_argument_of S) `1))] by A45;
len (@ ((Sub_the_right_argument_of S) `1)) < len (@ (S `1)) by A50, Th23;
then S1[G, len (@ ((Sub_the_right_argument_of S) `1))] by A45;
then A52: F . (Sub_the_right_argument_of S) = G . (Sub_the_right_argument_of S) by A49;
ex S1 being Element of QC-Sub-WFF F1() st
( S1 = Sub_the_left_argument_of S & ( for g being Function of (QC-Sub-WFF F1()),F2() st S1[g, len (@ (S1 `1))] holds
F . (Sub_the_left_argument_of S) = g . S1 ) ) by A36;
then F . (Sub_the_left_argument_of S) = G . (Sub_the_left_argument_of S) by A51;
hence ( not d1 = F . (Sub_the_left_argument_of S) or not d2 = F . (Sub_the_right_argument_of S) or F . S = F6(d1,d2) ) by A40, A42, A44, A50, A52; :: thesis: verum
end;
set k = len (@ ((Sub_the_scope_of S) `1));
assume A53: S is Sub_universal ; :: thesis: ( not d1 = F . (Sub_the_scope_of S) or F . S = F7(F1(),S,d1) )
then len (@ ((Sub_the_scope_of S) `1)) < len (@ (S `1)) by Th24;
then S1[G, len (@ ((Sub_the_scope_of S) `1))] by A45;
then F . (Sub_the_scope_of S) = G . (Sub_the_scope_of S) by A43;
hence ( not d1 = F . (Sub_the_scope_of S) or F . S = F7(F1(),S,d1) ) by A40, A42, A44, A53; :: thesis: verum