let A be set ; :: thesis: for K being Element of Normal_forms_on A st K = {} holds
- K = {[{} ,{} ]}
let K be Element of Normal_forms_on A; :: thesis: ( K = {} implies - K = {[{} ,{} ]} )
A1: [{} ,{} ] is Element of DISJOINT_PAIRS A by Th17;
assume A2: K = {} ; :: thesis: - K = {[{} ,{} ]}
{ [{ (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in K ) } ,{ (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in K ) } ] where g is Element of Funcs (DISJOINT_PAIRS A),[A] : for s being Element of DISJOINT_PAIRS A st s in K holds
g . s in (s `1 ) \/ (s `2 ) } = {[{} ,{} ]}

proof

thus { [{ (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in K ) } ,{ (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in K ) } ] where g is Element of Funcs (DISJOINT_PAIRS A),[A] : for s being Element of DISJOINT_PAIRS A st s in K holds
g . s in (s `1 ) \/ (s `2 ) } c= {[{} ,{} ]} :: according to XBOOLE_0:def 10 :: thesis: {[{} ,{} ]} c= { [{ (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in K ) } ,{ (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in K ) } ] where g is Element of Funcs (DISJOINT_PAIRS A),[A] : for s being Element of DISJOINT_PAIRS A st s in K holds
g . s in (s `1 ) \/ (s `2 ) }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { [{ (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in K ) } ,{ (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in K ) } ] where g is Element of Funcs (DISJOINT_PAIRS A),[A] : for s being Element of DISJOINT_PAIRS A st s in K holds
g . s in (s `1 ) \/ (s `2 ) } or x in {[{} ,{} ]} )
assume x in { [{ (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in K ) } ,{ (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in K ) } ] where g is Element of Funcs (DISJOINT_PAIRS A),[A] : for s being Element of DISJOINT_PAIRS A st s in K holds
g . s in (s `1 ) \/ (s `2 ) } ; :: thesis: x in {[{} ,{} ]}
then consider g being Element of Funcs (DISJOINT_PAIRS A),[A] such that
A3: x = [{ (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in K ) } ,{ (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in K ) } ] and
for s being Element of DISJOINT_PAIRS A st s in K holds
g . s in (s `1 ) \/ (s `2 ) ;
A4: ( x `1 = { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in K ) } & x `2 = { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in K ) } ) by A3, MCART_1:7;

A5: now

consider y being Element of x `1 ;
assume x `1 <> {} ; :: thesis: contradiction
then y in x `1 ;
then ex t1 being Element of DISJOINT_PAIRS A st
( y = g . t1 & g . t1 in t1 `2 & t1 in K ) by A4;
hence contradiction by A2; :: thesis: verum

end;

now

consider y being Element of x `2 ;
assume x `2 <> {} ; :: thesis: contradiction
then y in x `2 ;
then ex t1 being Element of DISJOINT_PAIRS A st
( y = g . t1 & g . t1 in t1 `1 & t1 in K ) by A4;
hence contradiction by A2; :: thesis: verum

end;

then x = [{} ,{} ] by A3, A5, MCART_1:8;
hence x in {[{} ,{} ]} by TARSKI:def 1; :: thesis: verum

end;

thus {[{} ,{} ]} c= { [{ (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in K ) } ,{ (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in K ) } ] where g is Element of Funcs (DISJOINT_PAIRS A),[A] : for s being Element of DISJOINT_PAIRS A st s in K holds
g . s in (s `1 ) \/ (s `2 ) } :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {[{} ,{} ]} or x in { [{ (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in K ) } ,{ (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in K ) } ] where g is Element of Funcs (DISJOINT_PAIRS A),[A] : for s being Element of DISJOINT_PAIRS A st s in K holds
g . s in (s `1 ) \/ (s `2 ) } )
assume x in {[{} ,{} ]} ; :: thesis: x in { [{ (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in K ) } ,{ (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in K ) } ] where g is Element of Funcs (DISJOINT_PAIRS A),[A] : for s being Element of DISJOINT_PAIRS A st s in K holds
g . s in (s `1 ) \/ (s `2 ) }
then A6: x = [{} ,{} ] by TARSKI:def 1;
consider g being Element of Funcs (DISJOINT_PAIRS A),[A];

A7: now

consider y being Element of { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in K ) } ;
assume { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in K ) } <> {} ; :: thesis: contradiction
then y in { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in K ) } ;
then ex t1 being Element of DISJOINT_PAIRS A st
( y = g . t1 & g . t1 in t1 `2 & t1 in K ) ;
hence contradiction by A2; :: thesis: verum

end;

A8: now

consider y being Element of { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in K ) } ;
assume { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in K ) } <> {} ; :: thesis: contradiction
then y in { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in K ) } ;
then ex t1 being Element of DISJOINT_PAIRS A st
( y = g . t1 & g . t1 in t1 `1 & t1 in K ) ;
hence contradiction by A2; :: thesis: verum

end;

for s being Element of DISJOINT_PAIRS A st s in K holds
g . s in (s `1 ) \/ (s `2 ) by A2;
hence x in { [{ (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in K ) } ,{ (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in K ) } ] where g is Element of Funcs (DISJOINT_PAIRS A),[A] : for s being Element of DISJOINT_PAIRS A st s in K holds
g . s in (s `1 ) \/ (s `2 ) } by A6, A7, A8; :: thesis: verum

end;

end;

hence - K = {[{} ,{} ]} by A1, ZFMISC_1:52; :: thesis: verum