Metamath Proof Explorer

Theorem issalnnd

Description: Sufficient condition to prove that S is sigma-algebra. (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses issalnnd.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
issalnnd.z ⊢ ( 𝜑 → ∅ ∈ 𝑆 )
issalnnd.x ⊢ 𝑋 = ∪ 𝑆
issalnnd.d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( 𝑋 ∖ 𝑦 ) ∈ 𝑆 )
issalnnd.i ⊢ ( ( 𝜑 ∧ 𝑒 : ℕ ⟶ 𝑆 ) → ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ∈ 𝑆 )
Assertion issalnnd ( 𝜑 → 𝑆 ∈ SAlg )

Proof

Step Hyp Ref Expression
1 issalnnd.s ⊢ ( 𝜑 → 𝑆 ∈ 𝑉 )
2 issalnnd.z ⊢ ( 𝜑 → ∅ ∈ 𝑆 )
3 issalnnd.x ⊢ 𝑋 = ∪ 𝑆
4 issalnnd.d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( 𝑋 ∖ 𝑦 ) ∈ 𝑆 )
5 issalnnd.i ⊢ ( ( 𝜑 ∧ 𝑒 : ℕ ⟶ 𝑆 ) → ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ∈ 𝑆 )
6 unieq ⊢ ( 𝑦 = ∅ → ∪ 𝑦 = ∪ ∅ )
7 uni0 ⊢ ∪ ∅ = ∅
8 7 a1i ⊢ ( 𝑦 = ∅ → ∪ ∅ = ∅ )
9 6 8 eqtrd ⊢ ( 𝑦 = ∅ → ∪ 𝑦 = ∅ )
10 9 adantl ⊢ ( ( 𝜑 ∧ 𝑦 = ∅ ) → ∪ 𝑦 = ∅ )
11 2 adantr ⊢ ( ( 𝜑 ∧ 𝑦 = ∅ ) → ∅ ∈ 𝑆 )
12 10 11 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑦 = ∅ ) → ∪ 𝑦 ∈ 𝑆 )
13 12 3ad2antl1 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω ) ∧ 𝑦 = ∅ ) → ∪ 𝑦 ∈ 𝑆 )
14 neqne ⊢ ( ¬ 𝑦 = ∅ → 𝑦 ≠ ∅ )
15 14 adantl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω ) ∧ ¬ 𝑦 = ∅ ) → 𝑦 ≠ ∅ )
16 nnfoctb ⊢ ( ( 𝑦 ≼ ω ∧ 𝑦 ≠ ∅ ) → ∃ 𝑒 𝑒 : ℕ –onto→ 𝑦 )
17 16 3ad2antl3 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω ) ∧ 𝑦 ≠ ∅ ) → ∃ 𝑒 𝑒 : ℕ –onto→ 𝑦 )
18 founiiun ⊢ ( 𝑒 : ℕ –onto→ 𝑦 → ∪ 𝑦 = ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) )
19 18 adantl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 𝑆 ) ∧ 𝑒 : ℕ –onto→ 𝑦 ) → ∪ 𝑦 = ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) )
20 simpll ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 𝑆 ) ∧ 𝑒 : ℕ –onto→ 𝑦 ) → 𝜑 )
21 fof ⊢ ( 𝑒 : ℕ –onto→ 𝑦 → 𝑒 : ℕ ⟶ 𝑦 )
22 21 adantl ⊢ ( ( 𝑦 ∈ 𝒫 𝑆 ∧ 𝑒 : ℕ –onto→ 𝑦 ) → 𝑒 : ℕ ⟶ 𝑦 )
23 elpwi ⊢ ( 𝑦 ∈ 𝒫 𝑆 → 𝑦 ⊆ 𝑆 )
24 23 adantr ⊢ ( ( 𝑦 ∈ 𝒫 𝑆 ∧ 𝑒 : ℕ –onto→ 𝑦 ) → 𝑦 ⊆ 𝑆 )
25 22 24 fssd ⊢ ( ( 𝑦 ∈ 𝒫 𝑆 ∧ 𝑒 : ℕ –onto→ 𝑦 ) → 𝑒 : ℕ ⟶ 𝑆 )
26 25 adantll ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 𝑆 ) ∧ 𝑒 : ℕ –onto→ 𝑦 ) → 𝑒 : ℕ ⟶ 𝑆 )
27 20 26 5 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 𝑆 ) ∧ 𝑒 : ℕ –onto→ 𝑦 ) → ∪ 𝑛 ∈ ℕ ( 𝑒 ‘ 𝑛 ) ∈ 𝑆 )
28 19 27 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 𝑆 ) ∧ 𝑒 : ℕ –onto→ 𝑦 ) → ∪ 𝑦 ∈ 𝑆 )
29 28 ex ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 𝑆 ) → ( 𝑒 : ℕ –onto→ 𝑦 → ∪ 𝑦 ∈ 𝑆 ) )
30 29 adantr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 𝑆 ) ∧ 𝑦 ≠ ∅ ) → ( 𝑒 : ℕ –onto→ 𝑦 → ∪ 𝑦 ∈ 𝑆 ) )
31 30 3adantl3 ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω ) ∧ 𝑦 ≠ ∅ ) → ( 𝑒 : ℕ –onto→ 𝑦 → ∪ 𝑦 ∈ 𝑆 ) )
32 31 exlimdv ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω ) ∧ 𝑦 ≠ ∅ ) → ( ∃ 𝑒 𝑒 : ℕ –onto→ 𝑦 → ∪ 𝑦 ∈ 𝑆 ) )
33 17 32 mpd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω ) ∧ 𝑦 ≠ ∅ ) → ∪ 𝑦 ∈ 𝑆 )
34 15 33 syldan ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω ) ∧ ¬ 𝑦 = ∅ ) → ∪ 𝑦 ∈ 𝑆 )
35 13 34 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 𝑆 ∧ 𝑦 ≼ ω ) → ∪ 𝑦 ∈ 𝑆 )
36 1 2 3 4 35 issald ⊢ ( 𝜑 → 𝑆 ∈ SAlg )