let A be QC-alphabet ; :: thesis: for x being bound_QC-variable of A
for p being Element of QC-WFF A holds Fixed (p . x) = Fixed p
let x be bound_QC-variable of A; :: thesis: for p being Element of QC-WFF A holds Fixed (p . x) = Fixed p
let p be Element of QC-WFF A; :: thesis: Fixed (p . x) = Fixed p
defpred S1[ Element of QC-WFF A] means Fixed ($1 . x) = Fixed $1;
A1: for p being Element of QC-WFF A st S1[p] holds
S1[ 'not' p]
proof
let p be Element of QC-WFF A; :: thesis: ( S1[p] implies S1[ 'not' p] )
assume A2: Fixed (p . x) = Fixed p ; :: thesis: S1[ 'not' p]
thus Fixed (('not' p) . x) = Fixed ('not' (p . x)) by Th19
.= Fixed p by A2, QC_LANG3:65
.= Fixed ('not' p) by QC_LANG3:65 ; :: thesis: verum
end;
A3: for p, q being Element of QC-WFF A st S1[p] & S1[q] holds
S1[p '&' q]
proof
let p, q be Element of QC-WFF A; :: thesis: ( S1[p] & S1[q] implies S1[p '&' q] )
assume A4: ( Fixed (p . x) = Fixed p & Fixed (q . x) = Fixed q ) ; :: thesis: S1[p '&' q]
thus Fixed ((p '&' q) . x) = Fixed ((p . x) '&' (q . x)) by Th21
.= (Fixed p) \/ (Fixed q) by A4, QC_LANG3:67
.= Fixed (p '&' q) by QC_LANG3:67 ; :: thesis: verum
end;
A5: for k being Nat
for P being QC-pred_symbol of k,A
for l being QC-variable_list of k,A holds S1[P ! l]
proof
let k be Nat; :: thesis: for P being QC-pred_symbol of k,A
for l being QC-variable_list of k,A holds S1[P ! l]
let P be QC-pred_symbol of k,A; :: thesis: for l being QC-variable_list of k,A holds S1[P ! l]
let l be QC-variable_list of k,A; :: thesis: S1[P ! l]
set F1 = { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in fixed_QC-variables A ) } ;
set ll = Subst (l,((A a. 0) .--> x));
set F2 = { ((Subst (l,((A a. 0) .--> x))) . i) where i is Nat : ( 1 <= i & i <= len (Subst (l,((A a. 0) .--> x))) & (Subst (l,((A a. 0) .--> x))) . i in fixed_QC-variables A ) } ;
A6: len l = len (Subst (l,((A a. 0) .--> x))) by Def1;
now :: thesis: for y being object holds
( ( y in { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in fixed_QC-variables A ) } implies y in { ((Subst (l,((A a. 0) .--> x))) . i) where i is Nat : ( 1 <= i & i <= len (Subst (l,((A a. 0) .--> x))) & (Subst (l,((A a. 0) .--> x))) . i in fixed_QC-variables A ) } ) & ( y in { ((Subst (l,((A a. 0) .--> x))) . i) where i is Nat : ( 1 <= i & i <= len (Subst (l,((A a. 0) .--> x))) & (Subst (l,((A a. 0) .--> x))) . i in fixed_QC-variables A ) } implies y in { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in fixed_QC-variables A ) } ) )
let y be object ; :: thesis: ( ( y in { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in fixed_QC-variables A ) } implies y in { ((Subst (l,((A a. 0) .--> x))) . i) where i is Nat : ( 1 <= i & i <= len (Subst (l,((A a. 0) .--> x))) & (Subst (l,((A a. 0) .--> x))) . i in fixed_QC-variables A ) } ) & ( y in { ((Subst (l,((A a. 0) .--> x))) . i) where i is Nat : ( 1 <= i & i <= len (Subst (l,((A a. 0) .--> x))) & (Subst (l,((A a. 0) .--> x))) . i in fixed_QC-variables A ) } implies y in { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in fixed_QC-variables A ) } ) )
thus ( y in { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in fixed_QC-variables A ) } implies y in { ((Subst (l,((A a. 0) .--> x))) . i) where i is Nat : ( 1 <= i & i <= len (Subst (l,((A a. 0) .--> x))) & (Subst (l,((A a. 0) .--> x))) . i in fixed_QC-variables A ) } ) :: thesis: ( y in { ((Subst (l,((A a. 0) .--> x))) . i) where i is Nat : ( 1 <= i & i <= len (Subst (l,((A a. 0) .--> x))) & (Subst (l,((A a. 0) .--> x))) . i in fixed_QC-variables A ) } implies y in { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in fixed_QC-variables A ) } )
proof
assume y in { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in fixed_QC-variables A ) } ; :: thesis: y in { ((Subst (l,((A a. 0) .--> x))) . i) where i is Nat : ( 1 <= i & i <= len (Subst (l,((A a. 0) .--> x))) & (Subst (l,((A a. 0) .--> x))) . i in fixed_QC-variables A ) }
then consider i being Nat such that
A7: y = l . i and
A8: ( 1 <= i & i <= len l ) and
A9: l . i in fixed_QC-variables A ;
l . i <> A a. 0 by A9, QC_LANG3:32;
then (Subst (l,((A a. 0) .--> x))) . i = l . i by A8, Th3;
hence y in { ((Subst (l,((A a. 0) .--> x))) . i) where i is Nat : ( 1 <= i & i <= len (Subst (l,((A a. 0) .--> x))) & (Subst (l,((A a. 0) .--> x))) . i in fixed_QC-variables A ) } by A6, A7, A8, A9; :: thesis: verum
end;
assume y in { ((Subst (l,((A a. 0) .--> x))) . i) where i is Nat : ( 1 <= i & i <= len (Subst (l,((A a. 0) .--> x))) & (Subst (l,((A a. 0) .--> x))) . i in fixed_QC-variables A ) } ; :: thesis: y in { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in fixed_QC-variables A ) }
then consider i being Nat such that
A10: y = (Subst (l,((A a. 0) .--> x))) . i and
A11: ( 1 <= i & i <= len (Subst (l,((A a. 0) .--> x))) ) and
A12: (Subst (l,((A a. 0) .--> x))) . i in fixed_QC-variables A ;
now :: thesis: not l . i = A a. 0
assume l . i = A a. 0 ; :: thesis: contradiction
then (Subst (l,((A a. 0) .--> x))) . i = x by A6, A11, Th3;
hence contradiction by A12, Lm1; :: thesis: verum
end;
then (Subst (l,((A a. 0) .--> x))) . i = l . i by A6, A11, Th3;
hence y in { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in fixed_QC-variables A ) } by A6, A10, A11, A12; :: thesis: verum
end;
then A13: { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in fixed_QC-variables A ) } = { ((Subst (l,((A a. 0) .--> x))) . i) where i is Nat : ( 1 <= i & i <= len (Subst (l,((A a. 0) .--> x))) & (Subst (l,((A a. 0) .--> x))) . i in fixed_QC-variables A ) } by TARSKI:2;
( Fixed (P ! l) = { (l . i) where i is Nat : ( 1 <= i & i <= len l & l . i in fixed_QC-variables A ) } & Fixed (P ! (Subst (l,((A a. 0) .--> x)))) = { ((Subst (l,((A a. 0) .--> x))) . i) where i is Nat : ( 1 <= i & i <= len (Subst (l,((A a. 0) .--> x))) & (Subst (l,((A a. 0) .--> x))) . i in fixed_QC-variables A ) } ) by QC_LANG3:64;
hence S1[P ! l] by A13, Th17; :: thesis: verum
end;
A14: for y being bound_QC-variable of A
for p being Element of QC-WFF A st S1[p] holds
S1[ All (y,p)]
proof
let y be bound_QC-variable of A; :: thesis: for p being Element of QC-WFF A st S1[p] holds
S1[ All (y,p)]
let p be Element of QC-WFF A; :: thesis: ( S1[p] implies S1[ All (y,p)] )
assume A15: Fixed (p . x) = Fixed p ; :: thesis: S1[ All (y,p)]
now :: thesis: ( x <> y implies Fixed ((All (y,p)) . x) = Fixed (All (y,p)) )
assume x <> y ; :: thesis: Fixed ((All (y,p)) . x) = Fixed (All (y,p))
hence Fixed ((All (y,p)) . x) = Fixed (All (y,(p . x))) by Th25
.= Fixed p by A15, QC_LANG3:68
.= Fixed (All (y,p)) by QC_LANG3:68 ;
:: thesis: verum
end;
hence S1[ All (y,p)] by Th24; :: thesis: verum
end;
A16: S1[ VERUM A] by Th15;
for p being Element of QC-WFF A holds S1[p] from QC_LANG1:sch 1(A5, A16, A1, A3, A14);
 hence Fixed (p . x) = Fixed p ; :: thesis: verum