Metamath Proof Explorer

Theorem unelldsys

Description: Lambda-systems are closed under disjoint set unions. (Contributed by Thierry Arnoux, 21-Jun-2020)

Ref Expression
Hypotheses isldsys.l 
|- L = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. s ) ) }
unelldsys.s 
|- ( ph -> S e. L )
unelldsys.a 
|- ( ph -> A e. S )
unelldsys.b 
|- ( ph -> B e. S )
unelldsys.c 
|- ( ph -> ( A i^i B ) = (/) )
Assertion unelldsys 
|- ( ph -> ( A u. B ) e. S )

Proof

Step Hyp Ref Expression
1 isldsys.l 
 |-  L = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. s ) ) }
2 unelldsys.s 
 |-  ( ph -> S e. L )
3 unelldsys.a 
 |-  ( ph -> A e. S )
4 unelldsys.b 
 |-  ( ph -> B e. S )
5 unelldsys.c 
 |-  ( ph -> ( A i^i B ) = (/) )
6 uneq1 
 |-  ( A = (/) -> ( A u. B ) = ( (/) u. B ) )
7 6 adantl 
 |-  ( ( ph /\ A = (/) ) -> ( A u. B ) = ( (/) u. B ) )
8 uncom 
 |-  ( B u. (/) ) = ( (/) u. B )
9 un0 
 |-  ( B u. (/) ) = B
10 8 9 eqtr3i 
 |-  ( (/) u. B ) = B
11 7 10 eqtrdi 
 |-  ( ( ph /\ A = (/) ) -> ( A u. B ) = B )
12 4 adantr 
 |-  ( ( ph /\ A = (/) ) -> B e. S )
13 11 12 eqeltrd 
 |-  ( ( ph /\ A = (/) ) -> ( A u. B ) e. S )
14 uniprg 
 |-  ( ( A e. S /\ B e. S ) -> U. { A , B } = ( A u. B ) )
15 3 4 14 syl2anc 
 |-  ( ph -> U. { A , B } = ( A u. B ) )
16 15 adantr 
 |-  ( ( ph /\ A =/= (/) ) -> U. { A , B } = ( A u. B ) )
17 prct 
 |-  ( ( A e. S /\ B e. S ) -> { A , B } ~<_ _om )
18 3 4 17 syl2anc 
 |-  ( ph -> { A , B } ~<_ _om )
19 18 adantr 
 |-  ( ( ph /\ A =/= (/) ) -> { A , B } ~<_ _om )
20 5 adantr 
 |-  ( ( ph /\ A =/= (/) ) -> ( A i^i B ) = (/) )
21 3 adantr 
 |-  ( ( ph /\ A =/= (/) ) -> A e. S )
22 4 adantr 
 |-  ( ( ph /\ A =/= (/) ) -> B e. S )
23 n0 
 |-  ( A =/= (/) <-> E. z z e. A )
24 23 bilani 
 |-  ( ( ph /\ A =/= (/) ) -> E. z z e. A )
25 disjel 
 |-  ( ( ( A i^i B ) = (/) /\ z e. A ) -> -. z e. B )
26 5 25 sylan 
 |-  ( ( ph /\ z e. A ) -> -. z e. B )
27 nelne1 
 |-  ( ( z e. A /\ -. z e. B ) -> A =/= B )
28 27 adantll 
 |-  ( ( ( ph /\ z e. A ) /\ -. z e. B ) -> A =/= B )
29 26 28 mpdan 
 |-  ( ( ph /\ z e. A ) -> A =/= B )
30 29 adantlr 
 |-  ( ( ( ph /\ A =/= (/) ) /\ z e. A ) -> A =/= B )
31 24 30 exlimddv 
 |-  ( ( ph /\ A =/= (/) ) -> A =/= B )
32 id 
 |-  ( y = A -> y = A )
33 id 
 |-  ( y = B -> y = B )
34 32 33 disjprg 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> ( Disj_ y e. { A , B } y <-> ( A i^i B ) = (/) ) )
35 21 22 31 34 syl3anc 
 |-  ( ( ph /\ A =/= (/) ) -> ( Disj_ y e. { A , B } y <-> ( A i^i B ) = (/) ) )
36 20 35 mpbird 
 |-  ( ( ph /\ A =/= (/) ) -> Disj_ y e. { A , B } y )
37 breq1 
 |-  ( z = { A , B } -> ( z ~<_ _om <-> { A , B } ~<_ _om ) )
38 disjeq1 
 |-  ( z = { A , B } -> ( Disj_ y e. z y <-> Disj_ y e. { A , B } y ) )
39 37 38 anbi12d 
 |-  ( z = { A , B } -> ( ( z ~<_ _om /\ Disj_ y e. z y ) <-> ( { A , B } ~<_ _om /\ Disj_ y e. { A , B } y ) ) )
40 unieq 
 |-  ( z = { A , B } -> U. z = U. { A , B } )
41 40 eleq1d 
 |-  ( z = { A , B } -> ( U. z e. S <-> U. { A , B } e. S ) )
42 39 41 imbi12d 
 |-  ( z = { A , B } -> ( ( ( z ~<_ _om /\ Disj_ y e. z y ) -> U. z e. S ) <-> ( ( { A , B } ~<_ _om /\ Disj_ y e. { A , B } y ) -> U. { A , B } e. S ) ) )
43 biid 
 |-  ( (/) e. s <-> (/) e. s )
44 difeq2 
 |-  ( x = z -> ( O \ x ) = ( O \ z ) )
45 44 eleq1d 
 |-  ( x = z -> ( ( O \ x ) e. s <-> ( O \ z ) e. s ) )
46 45 cbvralvw 
 |-  ( A. x e. s ( O \ x ) e. s <-> A. z e. s ( O \ z ) e. s )
47 breq1 
 |-  ( x = z -> ( x ~<_ _om <-> z ~<_ _om ) )
48 disjeq1 
 |-  ( x = z -> ( Disj_ y e. x y <-> Disj_ y e. z y ) )
49 47 48 anbi12d 
 |-  ( x = z -> ( ( x ~<_ _om /\ Disj_ y e. x y ) <-> ( z ~<_ _om /\ Disj_ y e. z y ) ) )
50 unieq 
 |-  ( x = z -> U. x = U. z )
51 50 eleq1d 
 |-  ( x = z -> ( U. x e. s <-> U. z e. s ) )
52 49 51 imbi12d 
 |-  ( x = z -> ( ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. s ) <-> ( ( z ~<_ _om /\ Disj_ y e. z y ) -> U. z e. s ) ) )
53 52 cbvralvw 
 |-  ( A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. s ) <-> A. z e. ~P s ( ( z ~<_ _om /\ Disj_ y e. z y ) -> U. z e. s ) )
54 43 46 53 3anbi123i 
 |-  ( ( (/) e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. s ) ) <-> ( (/) e. s /\ A. z e. s ( O \ z ) e. s /\ A. z e. ~P s ( ( z ~<_ _om /\ Disj_ y e. z y ) -> U. z e. s ) ) )
55 54 rabbii 
 |-  { s e. ~P ~P O | ( (/) e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> U. x e. s ) ) } = { s e. ~P ~P O | ( (/) e. s /\ A. z e. s ( O \ z ) e. s /\ A. z e. ~P s ( ( z ~<_ _om /\ Disj_ y e. z y ) -> U. z e. s ) ) }
56 1 55 eqtri 
 |-  L = { s e. ~P ~P O | ( (/) e. s /\ A. z e. s ( O \ z ) e. s /\ A. z e. ~P s ( ( z ~<_ _om /\ Disj_ y e. z y ) -> U. z e. s ) ) }
57 56 isldsys 
 |-  ( S e. L <-> ( S e. ~P ~P O /\ ( (/) e. S /\ A. z e. S ( O \ z ) e. S /\ A. z e. ~P S ( ( z ~<_ _om /\ Disj_ y e. z y ) -> U. z e. S ) ) ) )
58 2 57 sylib 
 |-  ( ph -> ( S e. ~P ~P O /\ ( (/) e. S /\ A. z e. S ( O \ z ) e. S /\ A. z e. ~P S ( ( z ~<_ _om /\ Disj_ y e. z y ) -> U. z e. S ) ) ) )
59 58 simprd 
 |-  ( ph -> ( (/) e. S /\ A. z e. S ( O \ z ) e. S /\ A. z e. ~P S ( ( z ~<_ _om /\ Disj_ y e. z y ) -> U. z e. S ) ) )
60 59 simp3d 
 |-  ( ph -> A. z e. ~P S ( ( z ~<_ _om /\ Disj_ y e. z y ) -> U. z e. S ) )
61 prelpwi 
 |-  ( ( A e. S /\ B e. S ) -> { A , B } e. ~P S )
62 3 4 61 syl2anc 
 |-  ( ph -> { A , B } e. ~P S )
63 42 60 62 rspcdva 
 |-  ( ph -> ( ( { A , B } ~<_ _om /\ Disj_ y e. { A , B } y ) -> U. { A , B } e. S ) )
64 63 adantr 
 |-  ( ( ph /\ A =/= (/) ) -> ( ( { A , B } ~<_ _om /\ Disj_ y e. { A , B } y ) -> U. { A , B } e. S ) )
65 19 36 64 mp2and 
 |-  ( ( ph /\ A =/= (/) ) -> U. { A , B } e. S )
66 16 65 eqeltrrd 
 |-  ( ( ph /\ A =/= (/) ) -> ( A u. B ) e. S )
67 13 66 pm2.61dane 
 |-  ( ph -> ( A u. B ) e. S )