Metamath Proof Explorer

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 ⊢ L = s ∈ 𝒫 𝒫 O | ∅ ∈ s ∧ ∀ x ∈ s O ∖ x ∈ s ∧ ∀ x ∈ 𝒫 s x ≼ ω ∧ Disj y ∈ x y → ⋃ x ∈ s
Assertion pwldsys ⊢ O ∈ V → 𝒫 O ∈ L

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 pwexg ⊢ O ∈ V → 𝒫 O ∈ V
3 pwidg ⊢ 𝒫 O ∈ V → 𝒫 O ∈ 𝒫 𝒫 O
4 2 3 syl ⊢ O ∈ V → 𝒫 O ∈ 𝒫 𝒫 O
5 0elpw ⊢ ∅ ∈ 𝒫 O
6 5 a1i ⊢ O ∈ V → ∅ ∈ 𝒫 O
7 pwidg ⊢ O ∈ V → O ∈ 𝒫 O
8 7 adantr ⊢ O ∈ V ∧ x ∈ 𝒫 O → O ∈ 𝒫 O
9 8 elpwdifcl ⊢ O ∈ V ∧ x ∈ 𝒫 O → O ∖ x ∈ 𝒫 O
10 9 ralrimiva ⊢ O ∈ V → ∀ x ∈ 𝒫 O O ∖ x ∈ 𝒫 O
11 elpwi ⊢ x ∈ 𝒫 𝒫 O → x ⊆ 𝒫 O
12 sspwuni ⊢ x ⊆ 𝒫 O ↔ ⋃ x ⊆ O
13 11 12 sylib ⊢ x ∈ 𝒫 𝒫 O → ⋃ x ⊆ O
14 13 adantl ⊢ O ∈ V ∧ x ∈ 𝒫 𝒫 O → ⋃ x ⊆ O
15 vuniex ⊢ ⋃ x ∈ V
16 15 elpw ⊢ ⋃ x ∈ 𝒫 O ↔ ⋃ x ⊆ O
17 14 16 sylibr ⊢ O ∈ V ∧ x ∈ 𝒫 𝒫 O → ⋃ x ∈ 𝒫 O
18 17 a1d ⊢ O ∈ V ∧ x ∈ 𝒫 𝒫 O → x ≼ ω ∧ Disj y ∈ x y → ⋃ x ∈ 𝒫 O
19 18 ralrimiva ⊢ O ∈ V → ∀ x ∈ 𝒫 𝒫 O x ≼ ω ∧ Disj y ∈ x y → ⋃ x ∈ 𝒫 O
20 6 10 19 3jca ⊢ O ∈ V → ∅ ∈ 𝒫 O ∧ ∀ x ∈ 𝒫 O O ∖ x ∈ 𝒫 O ∧ ∀ x ∈ 𝒫 𝒫 O x ≼ ω ∧ Disj y ∈ x y → ⋃ x ∈ 𝒫 O
21 1 isldsys ⊢ 𝒫 O ∈ L ↔ 𝒫 O ∈ 𝒫 𝒫 O ∧ ∅ ∈ 𝒫 O ∧ ∀ x ∈ 𝒫 O O ∖ x ∈ 𝒫 O ∧ ∀ x ∈ 𝒫 𝒫 O x ≼ ω ∧ Disj y ∈ x y → ⋃ x ∈ 𝒫 O
22 4 20 21 sylanbrc ⊢ O ∈ V → 𝒫 O ∈ L