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 𝒫 𝒫 O | s x s O x s x 𝒫 s x ω Disj y x y x s
unelldsys.s φ S L
unelldsys.a φ A S
unelldsys.b φ B S
unelldsys.c φ A B =
Assertion unelldsys φ A B S

Proof

Step Hyp Ref Expression
1 isldsys.l L = s 𝒫 𝒫 O | s x s O x s x 𝒫 s x ω Disj y x y x s
2 unelldsys.s φ S L
3 unelldsys.a φ A S
4 unelldsys.b φ B S
5 unelldsys.c φ A B =
6 uneq1 A = A B = B
7 6 adantl φ A = A B = B
8 uncom B = B
9 un0 B = B
10 8 9 eqtr3i B = B
11 7 10 syl6eq φ A = A B = B
12 4 adantr φ A = B S
13 11 12 eqeltrd φ A = A B S
14 uniprg A S B S A B = A B
15 3 4 14 syl2anc φ A B = A B
16 15 adantr φ A A B = A B
17 prct A S B S A B ω
18 3 4 17 syl2anc φ A B ω
19 18 adantr φ A A B ω
20 5 adantr φ A A B =
21 3 adantr φ A A S
22 4 adantr φ A B S
23 n0 A z z A
24 23 biimpi A z z A
25 24 adantl φ A z z A
26 disjel A B = z A ¬ z B
27 5 26 sylan φ z A ¬ z B
28 nelne1 z A ¬ z B A B
29 28 adantll φ z A ¬ z B A B
30 27 29 mpdan φ z A A B
31 30 adantlr φ A z A A B
32 25 31 exlimddv φ A A B
33 id y = A y = A
34 id y = B y = B
35 33 34 disjprgw A S B S A B Disj y A B y A B =
36 21 22 32 35 syl3anc φ A Disj y A B y A B =
37 20 36 mpbird φ A Disj y A B y
38 breq1 z = A B z ω A B ω
39 disjeq1 z = A B Disj y z y Disj y A B y
40 38 39 anbi12d z = A B z ω Disj y z y A B ω Disj y A B y
41 unieq z = A B z = A B
42 41 eleq1d z = A B z S A B S
43 40 42 imbi12d z = A B z ω Disj y z y z S A B ω Disj y A B y A B S
44 biid s s
45 difeq2 x = z O x = O z
46 45 eleq1d x = z O x s O z s
47 46 cbvralvw x s O x s z s O z s
48 breq1 x = z x ω z ω
49 disjeq1 x = z Disj y x y Disj y z y
50 48 49 anbi12d x = z x ω Disj y x y z ω Disj y z y
51 unieq x = z x = z
52 51 eleq1d x = z x s z s
53 50 52 imbi12d x = z x ω Disj y x y x s z ω Disj y z y z s
54 53 cbvralvw x 𝒫 s x ω Disj y x y x s z 𝒫 s z ω Disj y z y z s
55 44 47 54 3anbi123i s x s O x s x 𝒫 s x ω Disj y x y x s s z s O z s z 𝒫 s z ω Disj y z y z s
56 55 rabbii s 𝒫 𝒫 O | s x s O x s x 𝒫 s x ω Disj y x y x s = s 𝒫 𝒫 O | s z s O z s z 𝒫 s z ω Disj y z y z s
57 1 56 eqtri L = s 𝒫 𝒫 O | s z s O z s z 𝒫 s z ω Disj y z y z s
58 57 isldsys S L S 𝒫 𝒫 O S z S O z S z 𝒫 S z ω Disj y z y z S
59 2 58 sylib φ S 𝒫 𝒫 O S z S O z S z 𝒫 S z ω Disj y z y z S
60 59 simprd φ S z S O z S z 𝒫 S z ω Disj y z y z S
61 60 simp3d φ z 𝒫 S z ω Disj y z y z S
62 prelpwi A S B S A B 𝒫 S
63 3 4 62 syl2anc φ A B 𝒫 S
64 43 61 63 rspcdva φ A B ω Disj y A B y A B S
65 64 adantr φ A A B ω Disj y A B y A B S
66 19 37 65 mp2and φ A A B S
67 16 66 eqeltrrd φ A A B S
68 13 67 pm2.61dane φ A B S