let A be set ; :: thesis: for a being Element of DISJOINT_PAIRS A
for u being Element of (NormForm A) ex v being Element of (NormForm A) st
( v in SUB u & (@ v) ^ {a} = {} & ( for b being Element of DISJOINT_PAIRS A st b in (diff u) . v holds
b \/ a in DISJOINT_PAIRS A ) )
let a be Element of DISJOINT_PAIRS A; :: thesis: for u being Element of (NormForm A) ex v being Element of (NormForm A) st
( v in SUB u & (@ v) ^ {a} = {} & ( for b being Element of DISJOINT_PAIRS A st b in (diff u) . v holds
b \/ a in DISJOINT_PAIRS A ) )
let u be Element of (NormForm A); :: thesis: ex v being Element of (NormForm A) st
( v in SUB u & (@ v) ^ {a} = {} & ( for b being Element of DISJOINT_PAIRS A st b in (diff u) . v holds
b \/ a in DISJOINT_PAIRS A ) )
defpred S1[ set ] means verum;
deffunc H3( set ) -> set = $1;
defpred S2[ Element of DISJOINT_PAIRS A] means not $1 \/ a in DISJOINT_PAIRS A;
set M = { H3(s) where s is Element of DISJOINT_PAIRS A : ( H3(s) in u & S2[s] ) } ;
deffunc H4( Element of DISJOINT_PAIRS A) -> Element of [:(Fin A),(Fin A):] = $1 \/ a;
defpred S3[ set ] means $1 in u;
defpred S4[ Element of DISJOINT_PAIRS A] means ( S3[$1] & S2[$1] );
A1: { H4(t) where t is Element of DISJOINT_PAIRS A : ( t in { s where s is Element of DISJOINT_PAIRS A : S4[s] } & S1[t] ) } = { H4(s) where s is Element of DISJOINT_PAIRS A : ( S4[s] & S1[s] ) } from FRAENKEL:sch 14();
 defpred S5[ set , set ] means $1 in { H3(s) where s is Element of DISJOINT_PAIRS A : ( H3(s) in u & S2[s] ) } ;
defpred S6[ set , set ] means ( $1 in { H3(s) where s is Element of DISJOINT_PAIRS A : ( H3(s) in u & S2[s] ) } & $2 in {a} );
A2: { H4(s1) where s1 is Element of DISJOINT_PAIRS A : ( S4[s1] & S1[s1] ) } = { H4(s2) where s2 is Element of DISJOINT_PAIRS A : S4[s2] }
proof
thus { H4(s1) where s1 is Element of DISJOINT_PAIRS A : ( S4[s1] & S1[s1] ) } c= { H4(s2) where s2 is Element of DISJOINT_PAIRS A : S4[s2] } :: according to XBOOLE_0:def 10 :: thesis: { H4(s2) where s2 is Element of DISJOINT_PAIRS A : S4[s2] } c= { H4(s1) where s1 is Element of DISJOINT_PAIRS A : ( S4[s1] & S1[s1] ) }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { H4(s1) where s1 is Element of DISJOINT_PAIRS A : ( S4[s1] & S1[s1] ) } or x in { H4(s2) where s2 is Element of DISJOINT_PAIRS A : S4[s2] } )
assume x in { H4(s1) where s1 is Element of DISJOINT_PAIRS A : ( S4[s1] & S1[s1] ) } ; :: thesis: x in { H4(s2) where s2 is Element of DISJOINT_PAIRS A : S4[s2] }
then ex s1 being Element of DISJOINT_PAIRS A st
( x = H4(s1) & S4[s1] & S1[s1] ) ;
hence x in { H4(s2) where s2 is Element of DISJOINT_PAIRS A : S4[s2] } ; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { H4(s2) where s2 is Element of DISJOINT_PAIRS A : S4[s2] } or x in { H4(s1) where s1 is Element of DISJOINT_PAIRS A : ( S4[s1] & S1[s1] ) } )
assume x in { H4(s1) where s1 is Element of DISJOINT_PAIRS A : S4[s1] } ; :: thesis: x in { H4(s1) where s1 is Element of DISJOINT_PAIRS A : ( S4[s1] & S1[s1] ) }
then ex s1 being Element of DISJOINT_PAIRS A st
( x = H4(s1) & S4[s1] ) ;
hence x in { H4(s1) where s1 is Element of DISJOINT_PAIRS A : ( S4[s1] & S1[s1] ) } ; :: thesis: verum
end;
A3: { H3(s) where s is Element of DISJOINT_PAIRS A : ( H3(s) in u & S2[s] ) } c= u from FRAENKEL:sch 17();
 then reconsider v = { H3(s) where s is Element of DISJOINT_PAIRS A : ( H3(s) in u & S2[s] ) } as Element of (NormForm A) by Th5;
take v ; :: thesis: ( v in SUB u & (@ v) ^ {a} = {} & ( for b being Element of DISJOINT_PAIRS A st b in (diff u) . v holds
b \/ a in DISJOINT_PAIRS A ) )
thus v in SUB u by A3; :: thesis: ( (@ v) ^ {a} = {} & ( for b being Element of DISJOINT_PAIRS A st b in (diff u) . v holds
b \/ a in DISJOINT_PAIRS A ) )
defpred S7[ set , set ] means ( $2 = a & $1 in { H3(s) where s is Element of DISJOINT_PAIRS A : ( H3(s) in u & S2[s] ) } );
deffunc H5( Element of DISJOINT_PAIRS A, Element of DISJOINT_PAIRS A) -> Element of [:(Fin A),(Fin A):] = $1 \/ $2;
A4: { H4(t) where t is Element of DISJOINT_PAIRS A : ( t in { s where s is Element of DISJOINT_PAIRS A : S4[s] } & S1[t] ) } = { H4(t1) where t1 is Element of DISJOINT_PAIRS A : t1 in { s1 where s1 is Element of DISJOINT_PAIRS A : S4[s1] } }
proof
thus { H4(t) where t is Element of DISJOINT_PAIRS A : ( t in { s where s is Element of DISJOINT_PAIRS A : S4[s] } & S1[t] ) } c= { H4(t1) where t1 is Element of DISJOINT_PAIRS A : t1 in { s1 where s1 is Element of DISJOINT_PAIRS A : S4[s1] } } :: according to XBOOLE_0:def 10 :: thesis: { H4(t1) where t1 is Element of DISJOINT_PAIRS A : t1 in { s1 where s1 is Element of DISJOINT_PAIRS A : S4[s1] } } c= { H4(t) where t is Element of DISJOINT_PAIRS A : ( t in { s where s is Element of DISJOINT_PAIRS A : S4[s] } & S1[t] ) }
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { H4(t) where t is Element of DISJOINT_PAIRS A : ( t in { s where s is Element of DISJOINT_PAIRS A : S4[s] } & S1[t] ) } or x in { H4(t1) where t1 is Element of DISJOINT_PAIRS A : t1 in { s1 where s1 is Element of DISJOINT_PAIRS A : S4[s1] } } )
assume x in { H4(t) where t is Element of DISJOINT_PAIRS A : ( t in { s where s is Element of DISJOINT_PAIRS A : S4[s] } & S1[t] ) } ; :: thesis: x in { H4(t1) where t1 is Element of DISJOINT_PAIRS A : t1 in { s1 where s1 is Element of DISJOINT_PAIRS A : S4[s1] } }
then ex t being Element of DISJOINT_PAIRS A st
( x = H4(t) & t in { s where s is Element of DISJOINT_PAIRS A : S4[s] } & S1[t] ) ;
hence x in { H4(t1) where t1 is Element of DISJOINT_PAIRS A : t1 in { s1 where s1 is Element of DISJOINT_PAIRS A : S4[s1] } } ; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { H4(t1) where t1 is Element of DISJOINT_PAIRS A : t1 in { s1 where s1 is Element of DISJOINT_PAIRS A : S4[s1] } } or x in { H4(t) where t is Element of DISJOINT_PAIRS A : ( t in { s where s is Element of DISJOINT_PAIRS A : S4[s] } & S1[t] ) } )
assume x in { H4(t) where t is Element of DISJOINT_PAIRS A : t in { s where s is Element of DISJOINT_PAIRS A : S4[s] } } ; :: thesis: x in { H4(t) where t is Element of DISJOINT_PAIRS A : ( t in { s where s is Element of DISJOINT_PAIRS A : S4[s] } & S1[t] ) }
then ex t being Element of DISJOINT_PAIRS A st
( x = H4(t) & t in { s where s is Element of DISJOINT_PAIRS A : S4[s] } ) ;
hence x in { H4(t) where t is Element of DISJOINT_PAIRS A : ( t in { s where s is Element of DISJOINT_PAIRS A : S4[s] } & S1[t] ) } ; :: thesis: verum
end;
A5: { H5(s,t) where s, t is Element of DISJOINT_PAIRS A : ( t = a & S5[s,t] ) } = { H5(s9,a) where s9 is Element of DISJOINT_PAIRS A : S5[s9,a] } from FRAENKEL:sch 20();
 A6: for s, t being Element of DISJOINT_PAIRS A holds
( S6[s,t] iff S7[s,t] ) by TARSKI:def 1;
A7: { H5(s,t) where s, t is Element of DISJOINT_PAIRS A : S6[s,t] } = { H5(s9,t9) where s9, t9 is Element of DISJOINT_PAIRS A : S7[s9,t9] } from FRAENKEL:sch 4(A6);
 { H4(s) where s is Element of DISJOINT_PAIRS A : ( S3[s] & not H4(s) in DISJOINT_PAIRS A ) } misses DISJOINT_PAIRS A from FRAENKEL:sch 18();
 hence (@ v) ^ {a} = {} by A1, A4, A2, A7, A5; :: thesis: for b being Element of DISJOINT_PAIRS A st b in (diff u) . v holds
b \/ a in DISJOINT_PAIRS A
let b be Element of DISJOINT_PAIRS A; :: thesis: ( b in (diff u) . v implies b \/ a in DISJOINT_PAIRS A )
assume b in (diff u) . v ; :: thesis: b \/ a in DISJOINT_PAIRS A
then A8: b in u \ v by Def11;
then not b in { H3(s) where s is Element of DISJOINT_PAIRS A : ( H3(s) in u & S2[s] ) } by XBOOLE_0:def 5;
hence b \/ a in DISJOINT_PAIRS A by A8; :: thesis: verum