# 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}=\left\{{s}\in 𝒫𝒫{O}|\left(\varnothing \in {s}\wedge \forall {x}\in {s}\phantom{\rule{.4em}{0ex}}{O}\setminus {x}\in {s}\wedge \forall {x}\in 𝒫{s}\phantom{\rule{.4em}{0ex}}\left(\left({x}\preccurlyeq \mathrm{\omega }\wedge \underset{{y}\in {x}}{Disj}{y}\right)\to \bigcup {x}\in {s}\right)\right)\right\}$
unelldsys.s ${⊢}{\phi }\to {S}\in {L}$
unelldsys.a ${⊢}{\phi }\to {A}\in {S}$
unelldsys.b ${⊢}{\phi }\to {B}\in {S}$
unelldsys.c ${⊢}{\phi }\to {A}\cap {B}=\varnothing$
Assertion unelldsys ${⊢}{\phi }\to {A}\cup {B}\in {S}$

### Proof

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