let X be set ; :: thesis: for Y being finite Subset-Family of X holds union (Components Y) = X

let Y be finite Subset-Family of X; :: thesis: union (Components Y) = X

X c= union (Components Y)

let Y be finite Subset-Family of X; :: thesis: union (Components Y) = X

X c= union (Components Y)

proof

hence
union (Components Y) = X
; :: thesis: verum
deffunc H_{1}( set ) -> Element of BOOLEAN = FALSE ;

deffunc H_{2}( set ) -> Element of BOOLEAN = TRUE ;

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in X or z in union (Components Y) )

consider p being FinSequence of bool X such that

len p = card Y and

rng p = Y and

A1: Components Y = { (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p } by Def2;

defpred S_{1}[ set ] means z in p . $1;

A2: for i being Nat st i in Seg (len p) holds

( ( S_{1}[i] implies H_{2}(i) in BOOLEAN ) & ( not S_{1}[i] implies H_{1}(i) in BOOLEAN ) )
;

consider q being FinSequence of BOOLEAN such that

A3: len q = len p and

A4: for i being Nat st i in Seg (len p) holds

( ( S_{1}[i] implies q . i = H_{2}(i) ) & ( not S_{1}[i] implies q . i = H_{1}(i) ) )
from YELLOW15:sch 1(A2);

assume A5: z in X ; :: thesis: z in union (Components Y)

Intersect (rng (MergeSequence (p,q))) in Components Y by A1, A3;

hence z in union (Components Y) by A12, TARSKI:def 4; :: thesis: verum

end;deffunc H

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in X or z in union (Components Y) )

consider p being FinSequence of bool X such that

len p = card Y and

rng p = Y and

A1: Components Y = { (Intersect (rng (MergeSequence (p,q)))) where q is FinSequence of BOOLEAN : len q = len p } by Def2;

defpred S

A2: for i being Nat st i in Seg (len p) holds

( ( S

consider q being FinSequence of BOOLEAN such that

A3: len q = len p and

A4: for i being Nat st i in Seg (len p) holds

( ( S

assume A5: z in X ; :: thesis: z in union (Components Y)

now :: thesis: for Z being set st Z in rng (MergeSequence (p,q)) holds

z in Z

then A12:
z in Intersect (rng (MergeSequence (p,q)))
by A5, SETFAM_1:43;z in Z

let Z be set ; :: thesis: ( Z in rng (MergeSequence (p,q)) implies z in Z )

assume Z in rng (MergeSequence (p,q)) ; :: thesis: z in Z

then consider i being Nat such that

A6: i in dom (MergeSequence (p,q)) and

A7: (MergeSequence (p,q)) . i = Z by FINSEQ_2:10;

A8: dom (MergeSequence (p,q)) = dom p by Th1;

then A9: dom (MergeSequence (p,q)) = Seg (len p) by FINSEQ_1:def 3;

end;assume Z in rng (MergeSequence (p,q)) ; :: thesis: z in Z

then consider i being Nat such that

A6: i in dom (MergeSequence (p,q)) and

A7: (MergeSequence (p,q)) . i = Z by FINSEQ_2:10;

A8: dom (MergeSequence (p,q)) = dom p by Th1;

then A9: dom (MergeSequence (p,q)) = Seg (len p) by FINSEQ_1:def 3;

now :: thesis: z in Zend;

hence
z in Z
; :: thesis: verumIntersect (rng (MergeSequence (p,q))) in Components Y by A1, A3;

hence z in union (Components Y) by A12, TARSKI:def 4; :: thesis: verum