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	bilani	⊢ ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) → ∃ 𝑧 𝑧 ∈ 𝐴 )
25		disjel	⊢ ( ( ( 𝐴 ∩ 𝐵 ) = ∅ ∧ 𝑧 ∈ 𝐴 ) → ¬ 𝑧 ∈ 𝐵 )
26	5 25	sylan	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ¬ 𝑧 ∈ 𝐵 )
27		nelne1	⊢ ( ( 𝑧 ∈ 𝐴 ∧ ¬ 𝑧 ∈ 𝐵 ) → 𝐴 ≠ 𝐵 )
28	27	adantll	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) ∧ ¬ 𝑧 ∈ 𝐵 ) → 𝐴 ≠ 𝐵 )
29	26 28	mpdan	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → 𝐴 ≠ 𝐵 )
30	29	adantlr	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) ∧ 𝑧 ∈ 𝐴 ) → 𝐴 ≠ 𝐵 )
31	24 30	exlimddv	⊢ ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) → 𝐴 ≠ 𝐵 )
32		id	⊢ ( 𝑦 = 𝐴 → 𝑦 = 𝐴 )
33		id	⊢ ( 𝑦 = 𝐵 → 𝑦 = 𝐵 )
34	32 33	disjprg	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ≠ 𝐵 ) → ( Disj 𝑦 ∈ { 𝐴 , 𝐵 } 𝑦 ↔ ( 𝐴 ∩ 𝐵 ) = ∅ ) )
35	21 22 31 34	syl3anc	⊢ ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) → ( Disj 𝑦 ∈ { 𝐴 , 𝐵 } 𝑦 ↔ ( 𝐴 ∩ 𝐵 ) = ∅ ) )
36	20 35	mpbird	⊢ ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) → Disj 𝑦 ∈ { 𝐴 , 𝐵 } 𝑦 )
37		breq1	⊢ ( 𝑧 = { 𝐴 , 𝐵 } → ( 𝑧 ≼ ω ↔ { 𝐴 , 𝐵 } ≼ ω ) )
38		disjeq1	⊢ ( 𝑧 = { 𝐴 , 𝐵 } → ( Disj 𝑦 ∈ 𝑧 𝑦 ↔ Disj 𝑦 ∈ { 𝐴 , 𝐵 } 𝑦 ) )
39	37 38	anbi12d	⊢ ( 𝑧 = { 𝐴 , 𝐵 } → ( ( 𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦 ) ↔ ( { 𝐴 , 𝐵 } ≼ ω ∧ Disj 𝑦 ∈ { 𝐴 , 𝐵 } 𝑦 ) ) )
40		unieq	⊢ ( 𝑧 = { 𝐴 , 𝐵 } → ∪ 𝑧 = ∪ { 𝐴 , 𝐵 } )
41	40	eleq1d	⊢ ( 𝑧 = { 𝐴 , 𝐵 } → ( ∪ 𝑧 ∈ 𝑆 ↔ ∪ { 𝐴 , 𝐵 } ∈ 𝑆 ) )
42	39 41	imbi12d	⊢ ( 𝑧 = { 𝐴 , 𝐵 } → ( ( ( 𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦 ) → ∪ 𝑧 ∈ 𝑆 ) ↔ ( ( { 𝐴 , 𝐵 } ≼ ω ∧ Disj 𝑦 ∈ { 𝐴 , 𝐵 } 𝑦 ) → ∪ { 𝐴 , 𝐵 } ∈ 𝑆 ) ) )
43		biid	⊢ ( ∅ ∈ 𝑠 ↔ ∅ ∈ 𝑠 )
44		difeq2	⊢ ( 𝑥 = 𝑧 → ( 𝑂 ∖ 𝑥 ) = ( 𝑂 ∖ 𝑧 ) )
45	44	eleq1d	⊢ ( 𝑥 = 𝑧 → ( ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ↔ ( 𝑂 ∖ 𝑧 ) ∈ 𝑠 ) )
46	45	cbvralvw	⊢ ( ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ↔ ∀ 𝑧 ∈ 𝑠 ( 𝑂 ∖ 𝑧 ) ∈ 𝑠 )
47		breq1	⊢ ( 𝑥 = 𝑧 → ( 𝑥 ≼ ω ↔ 𝑧 ≼ ω ) )
48		disjeq1	⊢ ( 𝑥 = 𝑧 → ( Disj 𝑦 ∈ 𝑥 𝑦 ↔ Disj 𝑦 ∈ 𝑧 𝑦 ) )
49	47 48	anbi12d	⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ↔ ( 𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦 ) ) )
50		unieq	⊢ ( 𝑥 = 𝑧 → ∪ 𝑥 = ∪ 𝑧 )
51	50	eleq1d	⊢ ( 𝑥 = 𝑧 → ( ∪ 𝑥 ∈ 𝑠 ↔ ∪ 𝑧 ∈ 𝑠 ) )
52	49 51	imbi12d	⊢ ( 𝑥 = 𝑧 → ( ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑠 ) ↔ ( ( 𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦 ) → ∪ 𝑧 ∈ 𝑠 ) ) )
53	52	cbvralvw	⊢ ( ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑠 ) ↔ ∀ 𝑧 ∈ 𝒫 𝑠 ( ( 𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦 ) → ∪ 𝑧 ∈ 𝑠 ) )
54	43 46 53	3anbi123i	⊢ ( ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑠 ) ) ↔ ( ∅ ∈ 𝑠 ∧ ∀ 𝑧 ∈ 𝑠 ( 𝑂 ∖ 𝑧 ) ∈ 𝑠 ∧ ∀ 𝑧 ∈ 𝒫 𝑠 ( ( 𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦 ) → ∪ 𝑧 ∈ 𝑠 ) ) )
55	54	rabbii	⊢ { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑠 ) ) } = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑧 ∈ 𝑠 ( 𝑂 ∖ 𝑧 ) ∈ 𝑠 ∧ ∀ 𝑧 ∈ 𝒫 𝑠 ( ( 𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦 ) → ∪ 𝑧 ∈ 𝑠 ) ) }
56	1 55	eqtri	⊢ 𝐿 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑧 ∈ 𝑠 ( 𝑂 ∖ 𝑧 ) ∈ 𝑠 ∧ ∀ 𝑧 ∈ 𝒫 𝑠 ( ( 𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦 ) → ∪ 𝑧 ∈ 𝑠 ) ) }
57	56	isldsys	⊢ ( 𝑆 ∈ 𝐿 ↔ ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ ( ∅ ∈ 𝑆 ∧ ∀ 𝑧 ∈ 𝑆 ( 𝑂 ∖ 𝑧 ) ∈ 𝑆 ∧ ∀ 𝑧 ∈ 𝒫 𝑆 ( ( 𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦 ) → ∪ 𝑧 ∈ 𝑆 ) ) ) )
58	2 57	sylib	⊢ ( 𝜑 → ( 𝑆 ∈ 𝒫 𝒫 𝑂 ∧ ( ∅ ∈ 𝑆 ∧ ∀ 𝑧 ∈ 𝑆 ( 𝑂 ∖ 𝑧 ) ∈ 𝑆 ∧ ∀ 𝑧 ∈ 𝒫 𝑆 ( ( 𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦 ) → ∪ 𝑧 ∈ 𝑆 ) ) ) )
59	58	simprd	⊢ ( 𝜑 → ( ∅ ∈ 𝑆 ∧ ∀ 𝑧 ∈ 𝑆 ( 𝑂 ∖ 𝑧 ) ∈ 𝑆 ∧ ∀ 𝑧 ∈ 𝒫 𝑆 ( ( 𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦 ) → ∪ 𝑧 ∈ 𝑆 ) ) )
60	59	simp3d	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝒫 𝑆 ( ( 𝑧 ≼ ω ∧ Disj 𝑦 ∈ 𝑧 𝑦 ) → ∪ 𝑧 ∈ 𝑆 ) )
61		prelpwi	⊢ ( ( 𝐴 ∈ 𝑆 ∧ 𝐵 ∈ 𝑆 ) → { 𝐴 , 𝐵 } ∈ 𝒫 𝑆 )
62	3 4 61	syl2anc	⊢ ( 𝜑 → { 𝐴 , 𝐵 } ∈ 𝒫 𝑆 )
63	42 60 62	rspcdva	⊢ ( 𝜑 → ( ( { 𝐴 , 𝐵 } ≼ ω ∧ Disj 𝑦 ∈ { 𝐴 , 𝐵 } 𝑦 ) → ∪ { 𝐴 , 𝐵 } ∈ 𝑆 ) )
64	63	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) → ( ( { 𝐴 , 𝐵 } ≼ ω ∧ Disj 𝑦 ∈ { 𝐴 , 𝐵 } 𝑦 ) → ∪ { 𝐴 , 𝐵 } ∈ 𝑆 ) )
65	19 36 64	mp2and	⊢ ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) → ∪ { 𝐴 , 𝐵 } ∈ 𝑆 )
66	16 65	eqeltrrd	⊢ ( ( 𝜑 ∧ 𝐴 ≠ ∅ ) → ( 𝐴 ∪ 𝐵 ) ∈ 𝑆 )
67	13 66	pm2.61dane	⊢ ( 𝜑 → ( 𝐴 ∪ 𝐵 ) ∈ 𝑆 )