Metamath Proof Explorer

Theorem sigapildsys

Description: Sigma-algebra are exactly classes which are both lambda and pi-systems. (Contributed by Thierry Arnoux, 13-Jun-2020)

Ref Expression
Hypotheses dynkin.p ⊢ 𝑃 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( fi ‘ 𝑠 ) ⊆ 𝑠 }
dynkin.l ⊢ 𝐿 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑠 ) ) }
Assertion sigapildsys ( sigAlgebra ‘ 𝑂 ) = ( 𝑃 ∩ 𝐿 )

Proof

Step Hyp Ref Expression
1 dynkin.p ⊢ 𝑃 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( fi ‘ 𝑠 ) ⊆ 𝑠 }
2 dynkin.l ⊢ 𝐿 = { 𝑠 ∈ 𝒫 𝒫 𝑂 ∣ ( ∅ ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝑠 ( 𝑂 ∖ 𝑥 ) ∈ 𝑠 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑠 ) ) }
3 1 sigapisys ⊢ ( sigAlgebra ‘ 𝑂 ) ⊆ 𝑃
4 2 sigaldsys ⊢ ( sigAlgebra ‘ 𝑂 ) ⊆ 𝐿
5 3 4 ssini ⊢ ( sigAlgebra ‘ 𝑂 ) ⊆ ( 𝑃 ∩ 𝐿 )
6 id ⊢ ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) → 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) )
7 6 elin1d ⊢ ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) → 𝑡 ∈ 𝑃 )
8 1 ispisys ⊢ ( 𝑡 ∈ 𝑃 ↔ ( 𝑡 ∈ 𝒫 𝒫 𝑂 ∧ ( fi ‘ 𝑡 ) ⊆ 𝑡 ) )
9 7 8 sylib ⊢ ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) → ( 𝑡 ∈ 𝒫 𝒫 𝑂 ∧ ( fi ‘ 𝑡 ) ⊆ 𝑡 ) )
10 9 simpld ⊢ ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) → 𝑡 ∈ 𝒫 𝒫 𝑂 )
11 10 elpwid ⊢ ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) → 𝑡 ⊆ 𝒫 𝑂 )
12 dif0 ⊢ ( 𝑂 ∖ ∅ ) = 𝑂
13 6 elin2d ⊢ ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) → 𝑡 ∈ 𝐿 )
14 2 isldsys ⊢ ( 𝑡 ∈ 𝐿 ↔ ( 𝑡 ∈ 𝒫 𝒫 𝑂 ∧ ( ∅ ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ( 𝑂 ∖ 𝑥 ) ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝒫 𝑡 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑡 ) ) ) )
15 13 14 sylib ⊢ ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) → ( 𝑡 ∈ 𝒫 𝒫 𝑂 ∧ ( ∅ ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ( 𝑂 ∖ 𝑥 ) ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝒫 𝑡 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑡 ) ) ) )
16 15 simprd ⊢ ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) → ( ∅ ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ( 𝑂 ∖ 𝑥 ) ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝒫 𝑡 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑡 ) ) )
17 16 simp2d ⊢ ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) → ∀ 𝑥 ∈ 𝑡 ( 𝑂 ∖ 𝑥 ) ∈ 𝑡 )
18 16 simp1d ⊢ ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) → ∅ ∈ 𝑡 )
19 difeq2 ⊢ ( 𝑥 = ∅ → ( 𝑂 ∖ 𝑥 ) = ( 𝑂 ∖ ∅ ) )
20 eqidd ⊢ ( 𝑥 = ∅ → 𝑡 = 𝑡 )
21 19 20 eleq12d ⊢ ( 𝑥 = ∅ → ( ( 𝑂 ∖ 𝑥 ) ∈ 𝑡 ↔ ( 𝑂 ∖ ∅ ) ∈ 𝑡 ) )
22 21 rspcv ⊢ ( ∅ ∈ 𝑡 → ( ∀ 𝑥 ∈ 𝑡 ( 𝑂 ∖ 𝑥 ) ∈ 𝑡 → ( 𝑂 ∖ ∅ ) ∈ 𝑡 ) )
23 18 22 syl ⊢ ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) → ( ∀ 𝑥 ∈ 𝑡 ( 𝑂 ∖ 𝑥 ) ∈ 𝑡 → ( 𝑂 ∖ ∅ ) ∈ 𝑡 ) )
24 17 23 mpd ⊢ ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) → ( 𝑂 ∖ ∅ ) ∈ 𝑡 )
25 12 24 eqeltrrid ⊢ ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) → 𝑂 ∈ 𝑡 )
26 unieq ⊢ ( 𝑥 = ∅ → ∪ 𝑥 = ∪ ∅ )
27 uni0 ⊢ ∪ ∅ = ∅
28 26 27 eqtrdi ⊢ ( 𝑥 = ∅ → ∪ 𝑥 = ∅ )
29 28 adantl ⊢ ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 = ∅ ) → ∪ 𝑥 = ∅ )
30 18 ad3antrrr ⊢ ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 = ∅ ) → ∅ ∈ 𝑡 )
31 29 30 eqeltrd ⊢ ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 = ∅ ) → ∪ 𝑥 ∈ 𝑡 )
32 vex ⊢ 𝑥 ∈ V
33 32 0sdom ⊢ ( ∅ ≺ 𝑥 ↔ 𝑥 ≠ ∅ )
34 33 biimpri ⊢ ( 𝑥 ≠ ∅ → ∅ ≺ 𝑥 )
35 34 adantl ⊢ ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) → ∅ ≺ 𝑥 )
36 simplr ⊢ ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) → 𝑥 ≼ ω )
37 nnenom ⊢ ℕ ≈ ω
38 37 ensymi ⊢ ω ≈ ℕ
39 domentr ⊢ ( ( 𝑥 ≼ ω ∧ ω ≈ ℕ ) → 𝑥 ≼ ℕ )
40 36 38 39 sylancl ⊢ ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) → 𝑥 ≼ ℕ )
41 fodomr ⊢ ( ( ∅ ≺ 𝑥 ∧ 𝑥 ≼ ℕ ) → ∃ 𝑓 𝑓 : ℕ –onto→ 𝑥 )
42 35 40 41 syl2anc ⊢ ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) → ∃ 𝑓 𝑓 : ℕ –onto→ 𝑥 )
43 fveq2 ⊢ ( 𝑛 = 𝑖 → ( 𝑓 ‘ 𝑛 ) = ( 𝑓 ‘ 𝑖 ) )
44 43 iundisj ⊢ ∪ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) = ∪ 𝑛 ∈ ℕ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) )
45 fofn ⊢ ( 𝑓 : ℕ –onto→ 𝑥 → 𝑓 Fn ℕ )
46 fniunfv ⊢ ( 𝑓 Fn ℕ → ∪ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) = ∪ ran 𝑓 )
47 45 46 syl ⊢ ( 𝑓 : ℕ –onto→ 𝑥 → ∪ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) = ∪ ran 𝑓 )
48 forn ⊢ ( 𝑓 : ℕ –onto→ 𝑥 → ran 𝑓 = 𝑥 )
49 48 unieqd ⊢ ( 𝑓 : ℕ –onto→ 𝑥 → ∪ ran 𝑓 = ∪ 𝑥 )
50 47 49 eqtrd ⊢ ( 𝑓 : ℕ –onto→ 𝑥 → ∪ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) = ∪ 𝑥 )
51 44 50 eqtr3id ⊢ ( 𝑓 : ℕ –onto→ 𝑥 → ∪ 𝑛 ∈ ℕ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) = ∪ 𝑥 )
52 51 adantl ⊢ ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) → ∪ 𝑛 ∈ ℕ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) = ∪ 𝑥 )
53 fvex ⊢ ( 𝑓 ‘ 𝑛 ) ∈ V
54 difexg ⊢ ( ( 𝑓 ‘ 𝑛 ) ∈ V → ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ∈ V )
55 53 54 ax-mp ⊢ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ∈ V
56 55 dfiun3 ⊢ ∪ 𝑛 ∈ ℕ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) = ∪ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) )
57 nfv ⊢ Ⅎ 𝑛 ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 )
58 nfcv ⊢ Ⅎ 𝑛 𝑦
59 nfmpt1 ⊢ Ⅎ 𝑛 ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) )
60 59 nfrn ⊢ Ⅎ 𝑛 ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) )
61 58 60 nfel ⊢ Ⅎ 𝑛 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) )
62 57 61 nfan ⊢ Ⅎ 𝑛 ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) )
63 simpr ⊢ ( ( ( ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 = ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) → 𝑦 = ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) )
64 nfv ⊢ Ⅎ 𝑖 ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 )
65 nfcv ⊢ Ⅎ 𝑖 𝑦
66 nfcv ⊢ Ⅎ 𝑖 ℕ
67 nfcv ⊢ Ⅎ 𝑖 ( 𝑓 ‘ 𝑛 )
68 nfiu1 ⊢ Ⅎ 𝑖 ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 )
69 67 68 nfdif ⊢ Ⅎ 𝑖 ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) )
70 66 69 nfmpt ⊢ Ⅎ 𝑖 ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) )
71 70 nfrn ⊢ Ⅎ 𝑖 ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) )
72 65 71 nfel ⊢ Ⅎ 𝑖 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) )
73 64 72 nfan ⊢ Ⅎ 𝑖 ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) )
74 nfv ⊢ Ⅎ 𝑖 𝑛 ∈ ℕ
75 73 74 nfan ⊢ Ⅎ 𝑖 ( ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ) ∧ 𝑛 ∈ ℕ )
76 65 69 nfeq ⊢ Ⅎ 𝑖 𝑦 = ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) )
77 75 76 nfan ⊢ Ⅎ 𝑖 ( ( ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 = ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) )
78 6 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 = ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) → 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) )
79 simp-4r ⊢ ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) → 𝑥 ∈ 𝒫 𝑡 )
80 79 ad3antrrr ⊢ ( ( ( ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 = ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) → 𝑥 ∈ 𝒫 𝑡 )
81 80 elpwid ⊢ ( ( ( ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 = ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) → 𝑥 ⊆ 𝑡 )
82 fof ⊢ ( 𝑓 : ℕ –onto→ 𝑥 → 𝑓 : ℕ ⟶ 𝑥 )
83 82 ad4antlr ⊢ ( ( ( ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 = ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) → 𝑓 : ℕ ⟶ 𝑥 )
84 simplr ⊢ ( ( ( ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 = ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) → 𝑛 ∈ ℕ )
85 83 84 ffvelrnd ⊢ ( ( ( ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 = ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) → ( 𝑓 ‘ 𝑛 ) ∈ 𝑥 )
86 81 85 sseldd ⊢ ( ( ( ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 = ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) → ( 𝑓 ‘ 𝑛 ) ∈ 𝑡 )
87 fzofi ⊢ ( 1 ..^ 𝑛 ) ∈ Fin
88 87 a1i ⊢ ( ( ( ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 = ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) → ( 1 ..^ 𝑛 ) ∈ Fin )
89 81 adantr ⊢ ( ( ( ( ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 = ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ ( 1 ..^ 𝑛 ) ) → 𝑥 ⊆ 𝑡 )
90 83 adantr ⊢ ( ( ( ( ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 = ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ ( 1 ..^ 𝑛 ) ) → 𝑓 : ℕ ⟶ 𝑥 )
91 fzossnn ⊢ ( 1 ..^ 𝑛 ) ⊆ ℕ
92 91 a1i ⊢ ( ( ( ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 = ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) → ( 1 ..^ 𝑛 ) ⊆ ℕ )
93 92 sselda ⊢ ( ( ( ( ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 = ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ ( 1 ..^ 𝑛 ) ) → 𝑖 ∈ ℕ )
94 90 93 ffvelrnd ⊢ ( ( ( ( ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 = ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ ( 1 ..^ 𝑛 ) ) → ( 𝑓 ‘ 𝑖 ) ∈ 𝑥 )
95 89 94 sseldd ⊢ ( ( ( ( ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 = ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ ( 1 ..^ 𝑛 ) ) → ( 𝑓 ‘ 𝑖 ) ∈ 𝑡 )
96 1 2 77 78 86 88 95 sigapildsyslem ⊢ ( ( ( ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 = ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) → ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ∈ 𝑡 )
97 63 96 eqeltrd ⊢ ( ( ( ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 = ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) → 𝑦 ∈ 𝑡 )
98 simpr ⊢ ( ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ) → 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) )
99 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) )
100 99 55 elrnmpti ⊢ ( 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ↔ ∃ 𝑛 ∈ ℕ 𝑦 = ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) )
101 98 100 sylib ⊢ ( ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ) → ∃ 𝑛 ∈ ℕ 𝑦 = ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) )
102 62 97 101 r19.29af ⊢ ( ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ) → 𝑦 ∈ 𝑡 )
103 102 ex ⊢ ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) → ( 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) → 𝑦 ∈ 𝑡 ) )
104 103 ssrdv ⊢ ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) → ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ⊆ 𝑡 )
105 nnex ⊢ ℕ ∈ V
106 105 mptex ⊢ ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ∈ V
107 106 rnex ⊢ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ∈ V
108 elpwg ⊢ ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ∈ V → ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ∈ 𝒫 𝑡 ↔ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ⊆ 𝑡 ) )
109 107 108 ax-mp ⊢ ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ∈ 𝒫 𝑡 ↔ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ⊆ 𝑡 )
110 104 109 sylibr ⊢ ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) → ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ∈ 𝒫 𝑡 )
111 16 simp3d ⊢ ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) → ∀ 𝑥 ∈ 𝒫 𝑡 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑡 ) )
112 111 ad4antr ⊢ ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) → ∀ 𝑥 ∈ 𝒫 𝑡 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑡 ) )
113 nnct ⊢ ℕ ≼ ω
114 mptct ⊢ ( ℕ ≼ ω → ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ≼ ω )
115 113 114 ax-mp ⊢ ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ≼ ω
116 rnct ⊢ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ≼ ω → ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ≼ ω )
117 115 116 mp1i ⊢ ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) → ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ≼ ω )
118 43 iundisj2 ⊢ Disj 𝑛 ∈ ℕ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) )
119 disjrnmpt ⊢ ( Disj 𝑛 ∈ ℕ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) → Disj 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) 𝑦 )
120 118 119 mp1i ⊢ ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) → Disj 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) 𝑦 )
121 breq1 ⊢ ( 𝑥 = ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) → ( 𝑥 ≼ ω ↔ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ≼ ω ) )
122 disjeq1 ⊢ ( 𝑥 = ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) → ( Disj 𝑦 ∈ 𝑥 𝑦 ↔ Disj 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) 𝑦 ) )
123 121 122 anbi12d ⊢ ( 𝑥 = ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) → ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ↔ ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ≼ ω ∧ Disj 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) 𝑦 ) ) )
124 unieq ⊢ ( 𝑥 = ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) → ∪ 𝑥 = ∪ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) )
125 124 eleq1d ⊢ ( 𝑥 = ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) → ( ∪ 𝑥 ∈ 𝑡 ↔ ∪ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ∈ 𝑡 ) )
126 123 125 imbi12d ⊢ ( 𝑥 = ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) → ( ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑡 ) ↔ ( ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ≼ ω ∧ Disj 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) 𝑦 ) → ∪ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ∈ 𝑡 ) ) )
127 126 rspcv ⊢ ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ∈ 𝒫 𝑡 → ( ∀ 𝑥 ∈ 𝒫 𝑡 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑡 ) → ( ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ≼ ω ∧ Disj 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) 𝑦 ) → ∪ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ∈ 𝑡 ) ) )
128 127 imp ⊢ ( ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ∈ 𝒫 𝑡 ∧ ∀ 𝑥 ∈ 𝒫 𝑡 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑡 ) ) → ( ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ≼ ω ∧ Disj 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) 𝑦 ) → ∪ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ∈ 𝑡 ) )
129 128 imp ⊢ ( ( ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ∈ 𝒫 𝑡 ∧ ∀ 𝑥 ∈ 𝒫 𝑡 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑡 ) ) ∧ ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ≼ ω ∧ Disj 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) 𝑦 ) ) → ∪ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ∈ 𝑡 )
130 110 112 117 120 129 syl22anc ⊢ ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) → ∪ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ∈ 𝑡 )
131 56 130 eqeltrid ⊢ ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) → ∪ 𝑛 ∈ ℕ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ∈ 𝑡 )
132 52 131 eqeltrrd ⊢ ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) → ∪ 𝑥 ∈ 𝑡 )
133 42 132 exlimddv ⊢ ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) → ∪ 𝑥 ∈ 𝑡 )
134 31 133 pm2.61dane ⊢ ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) → ∪ 𝑥 ∈ 𝑡 )
135 134 ex ⊢ ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) → ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑡 ) )
136 135 ralrimiva ⊢ ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) → ∀ 𝑥 ∈ 𝒫 𝑡 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑡 ) )
137 25 17 136 3jca ⊢ ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) → ( 𝑂 ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ( 𝑂 ∖ 𝑥 ) ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝒫 𝑡 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑡 ) ) )
138 11 137 jca ⊢ ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) → ( 𝑡 ⊆ 𝒫 𝑂 ∧ ( 𝑂 ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ( 𝑂 ∖ 𝑥 ) ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝒫 𝑡 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑡 ) ) ) )
139 vex ⊢ 𝑡 ∈ V
140 issiga ⊢ ( 𝑡 ∈ V → ( 𝑡 ∈ ( sigAlgebra ‘ 𝑂 ) ↔ ( 𝑡 ⊆ 𝒫 𝑂 ∧ ( 𝑂 ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ( 𝑂 ∖ 𝑥 ) ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝒫 𝑡 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑡 ) ) ) ) )
141 139 140 ax-mp ⊢ ( 𝑡 ∈ ( sigAlgebra ‘ 𝑂 ) ↔ ( 𝑡 ⊆ 𝒫 𝑂 ∧ ( 𝑂 ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ( 𝑂 ∖ 𝑥 ) ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝒫 𝑡 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑡 ) ) ) )
142 138 141 sylibr ⊢ ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) → 𝑡 ∈ ( sigAlgebra ‘ 𝑂 ) )
143 142 ssriv ⊢ ( 𝑃 ∩ 𝐿 ) ⊆ ( sigAlgebra ‘ 𝑂 )
144 5 143 eqssi ⊢ ( sigAlgebra ‘ 𝑂 ) = ( 𝑃 ∩ 𝐿 )