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 = {[{},{}]} )
assume A1: K = {} ; :: thesis: - K = {[{},{}]}
A2: { [ { (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 object ; :: 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 `2 = { (g . t2) where t2 is Element of DISJOINT_PAIRS A : ( g . t2 in t2 `1 & t2 in K ) } by A3;
A5: now :: thesis: not x `2 <> {}
set y = the Element of x `2 ;
assume x `2 <> {} ; :: thesis: contradiction
then the Element of x `2 in x `2 ;
then ex t1 being Element of DISJOINT_PAIRS A st
( the Element of x `2 = g . t1 & g . t1 in t1 `1 & t1 in K ) by A4;
hence contradiction by A1; :: thesis: verum
end;
A6: x `1 = { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in K ) } by A3;
now :: thesis: not x `1 <> {}
set y = the Element of x `1 ;
assume x `1 <> {} ; :: thesis: contradiction
then the Element of x `1 in x `1 ;
then ex t1 being Element of DISJOINT_PAIRS A st
( the Element of x `1 = g . t1 & g . t1 in t1 `2 & t1 in K ) by A6;
hence contradiction by A1; :: thesis: verum
end;
then x = [{},{}] by A3, A5;
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
set g = the Element of Funcs ((DISJOINT_PAIRS A),[A]);
let x be object ; :: 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 A7: x = [{},{}] by TARSKI:def 1;
A8: now :: thesis: not { ( the Element of Funcs ((DISJOINT_PAIRS A),[A]) . t1) where t1 is Element of DISJOINT_PAIRS A : ( the Element of Funcs ((DISJOINT_PAIRS A),[A]) . t1 in t1 `2 & t1 in K ) } <> {}
set y = the Element of { ( the Element of Funcs ((DISJOINT_PAIRS A),[A]) . t1) where t1 is Element of DISJOINT_PAIRS A : ( the Element of Funcs ((DISJOINT_PAIRS A),[A]) . t1 in t1 `2 & t1 in K ) } ;
assume { ( the Element of Funcs ((DISJOINT_PAIRS A),[A]) . t1) where t1 is Element of DISJOINT_PAIRS A : ( the Element of Funcs ((DISJOINT_PAIRS A),[A]) . t1 in t1 `2 & t1 in K ) } <> {} ; :: thesis: contradiction
then the Element of { ( the Element of Funcs ((DISJOINT_PAIRS A),[A]) . t1) where t1 is Element of DISJOINT_PAIRS A : ( the Element of Funcs ((DISJOINT_PAIRS A),[A]) . t1 in t1 `2 & t1 in K ) } in { ( the Element of Funcs ((DISJOINT_PAIRS A),[A]) . t1) where t1 is Element of DISJOINT_PAIRS A : ( the Element of Funcs ((DISJOINT_PAIRS A),[A]) . t1 in t1 `2 & t1 in K ) } ;
then ex t1 being Element of DISJOINT_PAIRS A st
( the Element of { ( the Element of Funcs ((DISJOINT_PAIRS A),[A]) . t1) where t1 is Element of DISJOINT_PAIRS A : ( the Element of Funcs ((DISJOINT_PAIRS A),[A]) . t1 in t1 `2 & t1 in K ) } = the Element of Funcs ((DISJOINT_PAIRS A),[A]) . t1 & the Element of Funcs ((DISJOINT_PAIRS A),[A]) . t1 in t1 `2 & t1 in K ) ;
hence contradiction by A1; :: thesis: verum
end;
A9: now :: thesis: not { ( the Element of Funcs ((DISJOINT_PAIRS A),[A]) . t2) where t2 is Element of DISJOINT_PAIRS A : ( the Element of Funcs ((DISJOINT_PAIRS A),[A]) . t2 in t2 `1 & t2 in K ) } <> {}
set y = the Element of { ( the Element of Funcs ((DISJOINT_PAIRS A),[A]) . t2) where t2 is Element of DISJOINT_PAIRS A : ( the Element of Funcs ((DISJOINT_PAIRS A),[A]) . t2 in t2 `1 & t2 in K ) } ;
assume { ( the Element of Funcs ((DISJOINT_PAIRS A),[A]) . t2) where t2 is Element of DISJOINT_PAIRS A : ( the Element of Funcs ((DISJOINT_PAIRS A),[A]) . t2 in t2 `1 & t2 in K ) } <> {} ; :: thesis: contradiction
then the Element of { ( the Element of Funcs ((DISJOINT_PAIRS A),[A]) . t2) where t2 is Element of DISJOINT_PAIRS A : ( the Element of Funcs ((DISJOINT_PAIRS A),[A]) . t2 in t2 `1 & t2 in K ) } in { ( the Element of Funcs ((DISJOINT_PAIRS A),[A]) . t2) where t2 is Element of DISJOINT_PAIRS A : ( the Element of Funcs ((DISJOINT_PAIRS A),[A]) . t2 in t2 `1 & t2 in K ) } ;
then ex t1 being Element of DISJOINT_PAIRS A st
( the Element of { ( the Element of Funcs ((DISJOINT_PAIRS A),[A]) . t2) where t2 is Element of DISJOINT_PAIRS A : ( the Element of Funcs ((DISJOINT_PAIRS A),[A]) . t2 in t2 `1 & t2 in K ) } = the Element of Funcs ((DISJOINT_PAIRS A),[A]) . t1 & the Element of Funcs ((DISJOINT_PAIRS A),[A]) . t1 in t1 `1 & t1 in K ) ;
hence contradiction by A1; :: thesis: verum
end;
for s being Element of DISJOINT_PAIRS A st s in K holds
the Element of Funcs ((DISJOINT_PAIRS A),[A]) . s in (s `1) \/ (s `2) by A1;
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 A7, A8, A9; :: thesis: verum
end;
end;
[{},{}] is Element of DISJOINT_PAIRS A by Th12;
hence - K = {[{},{}]} by A2, ZFMISC_1:46; :: thesis: verum