Theorem pwldsys

Description: The power set of the universe set O is always a lambda-system. (Contributed by Thierry Arnoux, 21-Jun-2020)

	Ref	Expression
Hypothesis	isldsys.l	⊢ 𝐿 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑠 ) ) }
Assertion	pwldsys	⊢ ( 𝑂 ∈ 𝑉 → 𝒫 𝑂 ∈ 𝐿 )

Proof

Step	Hyp	Ref	Expression
1		isldsys.l	⊢ 𝐿 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑠 ) ) }
2		pwexg	⊢ ( 𝑂 ∈ 𝑉 → 𝒫 𝑂 ∈ V )
3		pwidg	⊢ ( 𝒫 𝑂 ∈ V → 𝒫 𝑂 ∈ 𝒫 𝒫 𝑂 )
4	2 3	syl	⊢ ( 𝑂 ∈ 𝑉 → 𝒫 𝑂 ∈ 𝒫 𝒫 𝑂 )
5		0elpw	⊢ ∅ ∈ 𝒫 𝑂
6	5	a1i	⊢ ( 𝑂 ∈ 𝑉 → ∅ ∈ 𝒫 𝑂 )
7		pwidg	⊢ ( 𝑂 ∈ 𝑉 → 𝑂 ∈ 𝒫 𝑂 )
8	7	adantr	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝑥 ∈ 𝒫 𝑂 ) → 𝑂 ∈ 𝒫 𝑂 )
9	8	elpwdifcl	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝑥 ∈ 𝒫 𝑂 ) → ( 𝑂 ∖ 𝑥 ) ∈ 𝒫 𝑂 )
10	9	ralrimiva	⊢ ( 𝑂 ∈ 𝑉 → ∀ 𝑥 ∈ 𝒫 𝑂 ( 𝑂 ∖ 𝑥 ) ∈ 𝒫 𝑂 )
11		elpwi	⊢ ( 𝑥 ∈ 𝒫 𝒫 𝑂 → 𝑥 ⊆ 𝒫 𝑂 )
12		sspwuni	⊢ ( 𝑥 ⊆ 𝒫 𝑂 ↔ ∪ 𝑥 ⊆ 𝑂 )
13	11 12	sylib	⊢ ( 𝑥 ∈ 𝒫 𝒫 𝑂 → ∪ 𝑥 ⊆ 𝑂 )
14	13	adantl	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝑥 ∈ 𝒫 𝒫 𝑂 ) → ∪ 𝑥 ⊆ 𝑂 )
15		vuniex	⊢ ∪ 𝑥 ∈ V
16	15	elpw	⊢ ( ∪ 𝑥 ∈ 𝒫 𝑂 ↔ ∪ 𝑥 ⊆ 𝑂 )
17	14 16	sylibr	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝑥 ∈ 𝒫 𝒫 𝑂 ) → ∪ 𝑥 ∈ 𝒫 𝑂 )
18	17	a1d	⊢ ( ( 𝑂 ∈ 𝑉 ∧ 𝑥 ∈ 𝒫 𝒫 𝑂 ) → ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝒫 𝑂 ) )
19	18	ralrimiva	⊢ ( 𝑂 ∈ 𝑉 → ∀ 𝑥 ∈ 𝒫 𝒫 𝑂 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝒫 𝑂 ) )
20	6 10 19	3jca	⊢ ( 𝑂 ∈ 𝑉 → ( ∅ ∈ 𝒫 𝑂 ∧ ∀ 𝑥 ∈ 𝒫 𝑂 ( 𝑂 ∖ 𝑥 ) ∈ 𝒫 𝑂 ∧ ∀ 𝑥 ∈ 𝒫 𝒫 𝑂 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝒫 𝑂 ) ) )
21	1	isldsys	⊢ ( 𝒫 𝑂 ∈ 𝐿 ↔ ( 𝒫 𝑂 ∈ 𝒫 𝒫 𝑂 ∧ ( ∅ ∈ 𝒫 𝑂 ∧ ∀ 𝑥 ∈ 𝒫 𝑂 ( 𝑂 ∖ 𝑥 ) ∈ 𝒫 𝑂 ∧ ∀ 𝑥 ∈ 𝒫 𝒫 𝑂 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝒫 𝑂 ) ) ) )
22	4 20 21	sylanbrc	⊢ ( 𝑂 ∈ 𝑉 → 𝒫 𝑂 ∈ 𝐿 )