let A be set ; for K, L being Element of Normal_forms_on A st K = {} & L = {} holds
K =>> L = {[{},{}]}
let K, L be Element of Normal_forms_on A; ( K = {} & L = {} implies K =>> L = {[{},{}]} )
assume that
A1:
K = {}
and
L = {}
; K =>> L = {[{},{}]}
A2:
{} = {}. A
;
A3:
K = {}. (DISJOINT_PAIRS A)
by A1;
A4:
now for f being Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) holds FinPairUnion (K,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A))))) = [{},{}]let f be
Element of
Funcs (
(DISJOINT_PAIRS A),
[:(Fin A),(Fin A):]);
FinPairUnion (K,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A))))) = [{},{}]thus FinPairUnion (
K,
((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A))))) =
the_unity_wrt (FinPairUnion A)
by A3, NORMFORM:18, SETWISEO:31
.=
[{},{}]
by A2, NORMFORM:19
;
verum end;
A5:
{ (FinPairUnion (K,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))))) where f is Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : f .: K c= L } = {[{},{}]}
proof
thus
{ (FinPairUnion (K,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))))) where f is Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : f .: K c= L } c= {[{},{}]}
XBOOLE_0:def 10 {[{},{}]} c= { (FinPairUnion (K,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))))) where f is Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : f .: K c= L } proof
let x be
object ;
TARSKI:def 3 ( not x in { (FinPairUnion (K,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))))) where f is Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : f .: K c= L } or x in {[{},{}]} )
assume
x in { (FinPairUnion (K,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))))) where f is Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : f .: K c= L }
;
x in {[{},{}]}
then
ex
f being
Element of
Funcs (
(DISJOINT_PAIRS A),
[:(Fin A),(Fin A):]) st
(
x = FinPairUnion (
K,
((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A))))) &
f .: K c= L )
;
then
x = [{},{}]
by A4;
hence
x in {[{},{}]}
by TARSKI:def 1;
verum
end;
thus
{[{},{}]} c= { (FinPairUnion (K,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))))) where f is Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : f .: K c= L }
verumproof
set f9 = the
Element of
Funcs (
(DISJOINT_PAIRS A),
[:(Fin A),(Fin A):]);
let x be
object ;
TARSKI:def 3 ( not x in {[{},{}]} or x in { (FinPairUnion (K,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))))) where f is Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : f .: K c= L } )
assume
x in {[{},{}]}
;
x in { (FinPairUnion (K,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))))) where f is Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : f .: K c= L }
then
x = [{},{}]
by TARSKI:def 1;
then A6:
x = FinPairUnion (
K,
((pair_diff A) .: ( the Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]),(incl (DISJOINT_PAIRS A)))))
by A4;
the
Element of
Funcs (
(DISJOINT_PAIRS A),
[:(Fin A),(Fin A):])
.: K c= L
by A1;
hence
x in { (FinPairUnion (K,((pair_diff A) .: (f,(incl (DISJOINT_PAIRS A)))))) where f is Element of Funcs ((DISJOINT_PAIRS A),[:(Fin A),(Fin A):]) : f .: K c= L }
by A6;
verum
end;
end;
[{},{}] is Element of DISJOINT_PAIRS A
by Th12;
hence
K =>> L = {[{},{}]}
by A5, ZFMISC_1:46; verum