let A be set ; for K being Element of Normal_forms_on A st K = {} holds
- K = {[{},{}]}
let K be Element of Normal_forms_on A; ( K = {} implies - K = {[{},{}]} )
assume A1:
K = {}
; - 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= {[{},{}]}
XBOOLE_0:def 10 {[{},{}]} 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 ;
TARSKI:def 3 ( 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) }
;
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;
A6:
x `1 = { (g . t1) where t1 is Element of DISJOINT_PAIRS A : ( g . t1 in t1 `2 & t1 in K ) }
by A3;
then
x = [{},{}]
by A3, A5;
hence
x in {[{},{}]}
by TARSKI:def 1;
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) }
verumproof
set g = the
Element of
Funcs (
(DISJOINT_PAIRS A),
[A]);
let x be
object ;
TARSKI:def 3 ( 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 {[{},{}]}
;
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 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 ) } <> {}
;
contradictionthen
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;
verum end;
A9:
now 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 ) } <> {}
;
contradictionthen
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;
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;
verum
end;
end;
[{},{}] is Element of DISJOINT_PAIRS A
by Th12;
hence
- K = {[{},{}]}
by A2, ZFMISC_1:46; verum