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 biimpi 
 |-  ( A =/= (/) -> E. z z e. A )
25 24 adantl 
 |-  ( ( ph /\ A =/= (/) ) -> E. z z e. A )
26 disjel 
 |-  ( ( ( A i^i B ) = (/) /\ z e. A ) -> -. z e. B )
27 5 26 sylan 
 |-  ( ( ph /\ z e. A ) -> -. z e. B )
28 nelne1 
 |-  ( ( z e. A /\ -. z e. B ) -> A =/= B )
29 28 adantll 
 |-  ( ( ( ph /\ z e. A ) /\ -. z e. B ) -> A =/= B )
30 27 29 mpdan 
 |-  ( ( ph /\ z e. A ) -> A =/= B )
31 30 adantlr 
 |-  ( ( ( ph /\ A =/= (/) ) /\ z e. A ) -> A =/= B )
32 25 31 exlimddv 
 |-  ( ( ph /\ A =/= (/) ) -> A =/= B )
33 id 
 |-  ( y = A -> y = A )
34 id 
 |-  ( y = B -> y = B )
35 33 34 disjprgw 
 |-  ( ( A e. S /\ B e. S /\ A =/= B ) -> ( Disj_ y e. { A , B } y <-> ( A i^i B ) = (/) ) )
36 21 22 32 35 syl3anc 
 |-  ( ( ph /\ A =/= (/) ) -> ( Disj_ y e. { A , B } y <-> ( A i^i B ) = (/) ) )
37 20 36 mpbird 
 |-  ( ( ph /\ A =/= (/) ) -> Disj_ y e. { A , B } y )
38 breq1 
 |-  ( z = { A , B } -> ( z ~<_ _om <-> { A , B } ~<_ _om ) )
39 disjeq1 
 |-  ( z = { A , B } -> ( Disj_ y e. z y <-> Disj_ y e. { A , B } y ) )
40 38 39 anbi12d 
 |-  ( z = { A , B } -> ( ( z ~<_ _om /\ Disj_ y e. z y ) <-> ( { A , B } ~<_ _om /\ Disj_ y e. { A , B } y ) ) )
41 unieq 
 |-  ( z = { A , B } -> U. z = U. { A , B } )
42 41 eleq1d 
 |-  ( z = { A , B } -> ( U. z e. S <-> U. { A , B } e. S ) )
43 40 42 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 ) ) )
44 biid 
 |-  ( (/) e. s <-> (/) e. s )
45 difeq2 
 |-  ( x = z -> ( O \ x ) = ( O \ z ) )
46 45 eleq1d 
 |-  ( x = z -> ( ( O \ x ) e. s <-> ( O \ z ) e. s ) )
47 46 cbvralvw 
 |-  ( A. x e. s ( O \ x ) e. s <-> A. z e. s ( O \ z ) e. s )
48 breq1 
 |-  ( x = z -> ( x ~<_ _om <-> z ~<_ _om ) )
49 disjeq1 
 |-  ( x = z -> ( Disj_ y e. x y <-> Disj_ y e. z y ) )
50 48 49 anbi12d 
 |-  ( x = z -> ( ( x ~<_ _om /\ Disj_ y e. x y ) <-> ( z ~<_ _om /\ Disj_ y e. z y ) ) )
51 unieq 
 |-  ( x = z -> U. x = U. z )
52 51 eleq1d 
 |-  ( x = z -> ( U. x e. s <-> U. z e. s ) )
53 50 52 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 ) ) )
54 53 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 ) )
55 44 47 54 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 ) ) )
56 55 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 ) ) }
57 1 56 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 ) ) }
58 57 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 ) ) ) )
59 2 58 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 ) ) ) )
60 59 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 ) ) )
61 60 simp3d 
 |-  ( ph -> A. z e. ~P S ( ( z ~<_ _om /\ Disj_ y e. z y ) -> U. z e. S ) )
62 prelpwi 
 |-  ( ( A e. S /\ B e. S ) -> { A , B } e. ~P S )
63 3 4 62 syl2anc 
 |-  ( ph -> { A , B } e. ~P S )
64 43 61 63 rspcdva 
 |-  ( ph -> ( ( { A , B } ~<_ _om /\ Disj_ y e. { A , B } y ) -> U. { A , B } e. S ) )
65 64 adantr 
 |-  ( ( ph /\ A =/= (/) ) -> ( ( { A , B } ~<_ _om /\ Disj_ y e. { A , B } y ) -> U. { A , B } e. S ) )
66 19 37 65 mp2and 
 |-  ( ( ph /\ A =/= (/) ) -> U. { A , B } e. S )
67 16 66 eqeltrrd 
 |-  ( ( ph /\ A =/= (/) ) -> ( A u. B ) e. S )
68 13 67 pm2.61dane 
 |-  ( ph -> ( A u. B ) e. S )