Theorem unelldsys

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

	Ref	Expression
Hypotheses	isldsys.l	⊢ 𝐿 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑠 ) ) }
	unelldsys.s	⊢ ( 𝜑 → 𝑆 ∈ 𝐿 )
	unelldsys.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
	unelldsys.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑆 )
	unelldsys.c	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∅ )
Assertion	unelldsys	⊢ ( 𝜑 → ( 𝐴 ∪ 𝐵 ) ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		isldsys.l	⊢ 𝐿 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑠 ) ) }
2		unelldsys.s	⊢ ( 𝜑 → 𝑆 ∈ 𝐿 )
3		unelldsys.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
4		unelldsys.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑆 )
5		unelldsys.c	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) = ∅ )
6		uneq1	⊢ ( 𝐴 = ∅ → ( 𝐴 ∪ 𝐵 ) = ( ∅ ∪ 𝐵 ) )
7	6	adantl	⊢ ( ( 𝜑 ∧ 𝐴 = ∅ ) → ( 𝐴 ∪ 𝐵 ) = ( ∅ ∪ 𝐵 ) )
8		uncom	⊢ ( 𝐵 ∪ ∅ ) = ( ∅ ∪ 𝐵 )
9		un0	⊢ ( 𝐵 ∪ ∅ ) = 𝐵
10	8 9	eqtr3i	⊢ ( ∅ ∪ 𝐵 ) = 𝐵
11	7 10	eqtrdi	⊢ ( ( 𝜑 ∧ 𝐴 = ∅ ) → ( 𝐴 ∪ 𝐵 ) = 𝐵 )
12	4	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = ∅ ) → 𝐵 ∈ 𝑆 )
13	11 12	eqeltrd	⊢ ( ( 𝜑 ∧ 𝐴 = ∅ ) → ( 𝐴 ∪ 𝐵 ) ∈ 𝑆 )
14		uniprg	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → ∪ { 𝐴 , 𝐵 } = ( 𝐴 ∪ 𝐵 ) )
15	3 4 14	syl2anc	⊢ ( 𝜑 → ∪ { 𝐴 , 𝐵 } = ( 𝐴 ∪ 𝐵 ) )
16	15	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) → ∪ { 𝐴 , 𝐵 } = ( 𝐴 ∪ 𝐵 ) )
17		prct	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → { 𝐴 , 𝐵 } ≼ ω )
18	3 4 17	syl2anc	⊢ ( 𝜑 → { 𝐴 , 𝐵 } ≼ ω )
19	18	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) → { 𝐴 , 𝐵 } ≼ ω )
20	5	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) → ( 𝐴 ∩ 𝐵 ) = ∅ )
21	3	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) → 𝐴 ∈ 𝑆 )
22	4	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) → 𝐵 ∈ 𝑆 )
23		n0	⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑧 𝑧 ∈ 𝐴 )
24	23	biimpi	⊢ ( 𝐴 ≠ ∅ → ∃ 𝑧 𝑧 ∈ 𝐴 )
25	24	adantl	⊢ ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) → ∃ 𝑧 𝑧 ∈ 𝐴 )
26		disjel	⊢ ( ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ 𝑧 ∈ 𝐴 ) → ¬ 𝑧 ∈ 𝐵 )
27	5 26	sylan	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ¬ 𝑧 ∈ 𝐵 )
28		nelne1	⊢ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝐵 ) → 𝐴 ≠ 𝐵 )
29	28	adantll	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ 𝐵 ) → 𝐴 ≠ 𝐵 )
30	27 29	mpdan	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝐴 ≠ 𝐵 )
31	30	adantlr	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ∈ 𝐴 ) → 𝐴 ≠ 𝐵 )
32	25 31	exlimddv	⊢ ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) → 𝐴 ≠ 𝐵 )
33		id	⊢ ( 𝑦 = 𝐴 → 𝑦 = 𝐴 )
34		id	⊢ ( 𝑦 = 𝐵 → 𝑦 = 𝐵 )
35	33 34	disjprgw	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ( Disj 𝑦 ∈ { 𝐴 , 𝐵 } 𝑦 ↔ ( 𝐴 ∩ 𝐵 ) = ∅ ) )
36	21 22 32 35	syl3anc	⊢ ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) → ( Disj 𝑦 ∈ { 𝐴 , 𝐵 } 𝑦 ↔ ( 𝐴 ∩ 𝐵 ) = ∅ ) )
37	20 36	mpbird	⊢ ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) → Disj 𝑦 ∈ { 𝐴 , 𝐵 } 𝑦 )
38		breq1	⊢ ( 𝑧 = { 𝐴 , 𝐵 } → ( 𝑧 ≼ ω ↔ { 𝐴 , 𝐵 } ≼ ω ) )
39		disjeq1	⊢ ( 𝑧 = { 𝐴 , 𝐵 } → ( Disj 𝑦 ∈ 𝑧 𝑦 ↔ Disj 𝑦 ∈ { 𝐴 , 𝐵 } 𝑦 ) )
40	38 39	anbi12d	⊢ ( 𝑧 = { 𝐴 , 𝐵 } → ( ( 𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦 ) ↔ ( { 𝐴 , 𝐵 } ≼ ω ∧ Disj 𝑦 ∈ { 𝐴 , 𝐵 } 𝑦 ) ) )
41		unieq	⊢ ( 𝑧 = { 𝐴 , 𝐵 } → ∪ 𝑧 = ∪ { 𝐴 , 𝐵 } )
42	41	eleq1d	⊢ ( 𝑧 = { 𝐴 , 𝐵 } → ( ∪ 𝑧 ∈ 𝑆 ↔ ∪ { 𝐴 , 𝐵 } ∈ 𝑆 ) )
43	40 42	imbi12d	⊢ ( 𝑧 = { 𝐴 , 𝐵 } → ( ( ( 𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦 ) → ∪ 𝑧 ∈ 𝑆 ) ↔ ( ( { 𝐴 , 𝐵 } ≼ ω ∧ Disj 𝑦 ∈ { 𝐴 , 𝐵 } 𝑦 ) → ∪ { 𝐴 , 𝐵 } ∈ 𝑆 ) ) )
44		biid	⊢ ( ∅ ∈ 𝑠 ↔ ∅ ∈ 𝑠 )
45		difeq2	⊢ ( 𝑥 = 𝑧 → ( 𝑂 ∖ 𝑥 ) = ( 𝑂 ∖ 𝑧 ) )
46	45	eleq1d	⊢ ( 𝑥 = 𝑧 → ( ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ↔ ( 𝑂 ∖ 𝑧 ) ∈ 𝑠 ) )
47	46	cbvralvw	⊢ ( ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ↔ ∀ 𝑧 ∈ 𝑠 ( 𝑂 ∖ 𝑧 ) ∈ 𝑠 )
48		breq1	⊢ ( 𝑥 = 𝑧 → ( 𝑥 ≼ ω ↔ 𝑧 ≼ ω ) )
49		disjeq1	⊢ ( 𝑥 = 𝑧 → ( Disj 𝑦 ∈ 𝑥 𝑦 ↔ Disj 𝑦 ∈ 𝑧 𝑦 ) )
50	48 49	anbi12d	⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ↔ ( 𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦 ) ) )
51		unieq	⊢ ( 𝑥 = 𝑧 → ∪ 𝑥 = ∪ 𝑧 )
52	51	eleq1d	⊢ ( 𝑥 = 𝑧 → ( ∪ 𝑥 ∈ 𝑠 ↔ ∪ 𝑧 ∈ 𝑠 ) )
53	50 52	imbi12d	⊢ ( 𝑥 = 𝑧 → ( ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑠 ) ↔ ( ( 𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦 ) → ∪ 𝑧 ∈ 𝑠 ) ) )
54	53	cbvralvw	⊢ ( ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑠 ) ↔ ∀ 𝑧 ∈ 𝒫 𝑠 ( ( 𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦 ) → ∪ 𝑧 ∈ 𝑠 ) )
55	44 47 54	3anbi123i	⊢ ( ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑠 ) ) ↔ ( ∅ ∈ 𝑠 ∧ ∀ 𝑧 ∈ 𝑠 ( 𝑂 ∖ 𝑧 ) ∈ 𝑠 ∧ ∀ 𝑧 ∈ 𝒫 𝑠 ( ( 𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦 ) → ∪ 𝑧 ∈ 𝑠 ) ) )
56	55	rabbii	⊢ { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑠 ) ) } = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑧 ∈ 𝑠 ( 𝑂 ∖ 𝑧 ) ∈ 𝑠 ∧ ∀ 𝑧 ∈ 𝒫 𝑠 ( ( 𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦 ) → ∪ 𝑧 ∈ 𝑠 ) ) }
57	1 56	eqtri	⊢ 𝐿 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑧 ∈ 𝑠 ( 𝑂 ∖ 𝑧 ) ∈ 𝑠 ∧ ∀ 𝑧 ∈ 𝒫 𝑠 ( ( 𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦 ) → ∪ 𝑧 ∈ 𝑠 ) ) }
58	57	isldsys	⊢ ( 𝑆 ∈ 𝐿 ↔ ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ ( ∅ ∈ 𝑆 ∧ ∀ 𝑧 ∈ 𝑆 ( 𝑂 ∖ 𝑧 ) ∈ 𝑆 ∧ ∀ 𝑧 ∈ 𝒫 𝑆 ( ( 𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦 ) → ∪ 𝑧 ∈ 𝑆 ) ) ) )
59	2 58	sylib	⊢ ( 𝜑 → ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ ( ∅ ∈ 𝑆 ∧ ∀ 𝑧 ∈ 𝑆 ( 𝑂 ∖ 𝑧 ) ∈ 𝑆 ∧ ∀ 𝑧 ∈ 𝒫 𝑆 ( ( 𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦 ) → ∪ 𝑧 ∈ 𝑆 ) ) ) )
60	59	simprd	⊢ ( 𝜑 → ( ∅ ∈ 𝑆 ∧ ∀ 𝑧 ∈ 𝑆 ( 𝑂 ∖ 𝑧 ) ∈ 𝑆 ∧ ∀ 𝑧 ∈ 𝒫 𝑆 ( ( 𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦 ) → ∪ 𝑧 ∈ 𝑆 ) ) )
61	60	simp3d	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝒫 𝑆 ( ( 𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦 ) → ∪ 𝑧 ∈ 𝑆 ) )
62		prelpwi	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → { 𝐴 , 𝐵 } ∈ 𝒫 𝑆 )
63	3 4 62	syl2anc	⊢ ( 𝜑 → { 𝐴 , 𝐵 } ∈ 𝒫 𝑆 )
64	43 61 63	rspcdva	⊢ ( 𝜑 → ( ( { 𝐴 , 𝐵 } ≼ ω ∧ Disj 𝑦 ∈ { 𝐴 , 𝐵 } 𝑦 ) → ∪ { 𝐴 , 𝐵 } ∈ 𝑆 ) )
65	64	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) → ( ( { 𝐴 , 𝐵 } ≼ ω ∧ Disj 𝑦 ∈ { 𝐴 , 𝐵 } 𝑦 ) → ∪ { 𝐴 , 𝐵 } ∈ 𝑆 ) )
66	19 37 65	mp2and	⊢ ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) → ∪ { 𝐴 , 𝐵 } ∈ 𝑆 )
67	16 66	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) → ( 𝐴 ∪ 𝐵 ) ∈ 𝑆 )
68	13 67	pm2.61dane	⊢ ( 𝜑 → ( 𝐴 ∪ 𝐵 ) ∈ 𝑆 )