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 bilanri ⊢ ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) → ∅ ≺ 𝑥 )
35 simplr ⊢ ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) → 𝑥 ≼ ω )
36 nnenom ⊢ ℕ ≈ ω
37 36 ensymi ⊢ ω ≈ ℕ
38 domentr ⊢ ( ( 𝑥 ≼ ω ∧ ω ≈ ℕ ) → 𝑥 ≼ ℕ )
39 35 37 38 sylancl ⊢ ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) → 𝑥 ≼ ℕ )
40 fodomr ⊢ ( ( ∅ ≺ 𝑥 ∧ 𝑥 ≼ ℕ ) → ∃ 𝑓 𝑓 : ℕ –onto→ 𝑥 )
41 34 39 40 syl2anc ⊢ ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) → ∃ 𝑓 𝑓 : ℕ –onto→ 𝑥 )
42 fveq2 ⊢ ( 𝑛 = 𝑖 → ( 𝑓 ‘ 𝑛 ) = ( 𝑓 ‘ 𝑖 ) )
43 42 iundisj ⊢ ∪ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) = ∪ 𝑛 ∈ ℕ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) )
44 fofn ⊢ ( 𝑓 : ℕ –onto→ 𝑥 → 𝑓 Fn ℕ )
45 fniunfv ⊢ ( 𝑓 Fn ℕ → ∪ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) = ∪ ran 𝑓 )
46 44 45 syl ⊢ ( 𝑓 : ℕ –onto→ 𝑥 → ∪ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) = ∪ ran 𝑓 )
47 forn ⊢ ( 𝑓 : ℕ –onto→ 𝑥 → ran 𝑓 = 𝑥 )
48 47 unieqd ⊢ ( 𝑓 : ℕ –onto→ 𝑥 → ∪ ran 𝑓 = ∪ 𝑥 )
49 46 48 eqtrd ⊢ ( 𝑓 : ℕ –onto→ 𝑥 → ∪ 𝑛 ∈ ℕ ( 𝑓 ‘ 𝑛 ) = ∪ 𝑥 )
50 43 49 eqtr3id ⊢ ( 𝑓 : ℕ –onto→ 𝑥 → ∪ 𝑛 ∈ ℕ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) = ∪ 𝑥 )
51 50 adantl ⊢ ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) → ∪ 𝑛 ∈ ℕ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) = ∪ 𝑥 )
52 fvex ⊢ ( 𝑓 ‘ 𝑛 ) ∈ V
53 difexg ⊢ ( ( 𝑓 ‘ 𝑛 ) ∈ V → ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ∈ V )
54 52 53 ax-mp ⊢ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ∈ V
55 54 dfiun3 ⊢ ∪ 𝑛 ∈ ℕ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) = ∪ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) )
56 nfv ⊢ Ⅎ 𝑛 ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 )
57 nfcv ⊢ Ⅎ 𝑛 𝑦
58 nfmpt1 ⊢ Ⅎ 𝑛 ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) )
59 58 nfrn ⊢ Ⅎ 𝑛 ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) )
60 57 59 nfel ⊢ Ⅎ 𝑛 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) )
61 56 60 nfan ⊢ Ⅎ 𝑛 ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) )
62 simpr ⊢ ( ( ( ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 = ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) → 𝑦 = ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) )
63 nfv ⊢ Ⅎ 𝑖 ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 )
64 nfcv ⊢ Ⅎ 𝑖 𝑦
65 nfcv ⊢ Ⅎ 𝑖 ℕ
66 nfcv ⊢ Ⅎ 𝑖 ( 𝑓 ‘ 𝑛 )
67 nfiu1 ⊢ Ⅎ 𝑖 ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 )
68 66 67 nfdif ⊢ Ⅎ 𝑖 ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) )
69 65 68 nfmpt ⊢ Ⅎ 𝑖 ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) )
70 69 nfrn ⊢ Ⅎ 𝑖 ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) )
71 64 70 nfel ⊢ Ⅎ 𝑖 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) )
72 63 71 nfan ⊢ Ⅎ 𝑖 ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) )
73 nfv ⊢ Ⅎ 𝑖 𝑛 ∈ ℕ
74 72 73 nfan ⊢ Ⅎ 𝑖 ( ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ) ∧ 𝑛 ∈ ℕ )
75 64 68 nfeq ⊢ Ⅎ 𝑖 𝑦 = ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) )
76 74 75 nfan ⊢ Ⅎ 𝑖 ( ( ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 = ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) )
77 6 ad7antr ⊢ ( ( ( ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 = ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) → 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) )
78 simp-4r ⊢ ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) → 𝑥 ∈ 𝒫 𝑡 )
79 78 ad3antrrr ⊢ ( ( ( ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 = ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) → 𝑥 ∈ 𝒫 𝑡 )
80 79 elpwid ⊢ ( ( ( ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 = ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) → 𝑥 ⊆ 𝑡 )
81 fof ⊢ ( 𝑓 : ℕ –onto→ 𝑥 → 𝑓 : ℕ ⟶ 𝑥 )
82 81 ad4antlr ⊢ ( ( ( ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 = ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) → 𝑓 : ℕ ⟶ 𝑥 )
83 simplr ⊢ ( ( ( ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 = ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) → 𝑛 ∈ ℕ )
84 82 83 ffvelcdmd ⊢ ( ( ( ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 = ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) → ( 𝑓 ‘ 𝑛 ) ∈ 𝑥 )
85 80 84 sseldd ⊢ ( ( ( ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 = ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) → ( 𝑓 ‘ 𝑛 ) ∈ 𝑡 )
86 fzofi ⊢ ( 1 ..^ 𝑛 ) ∈ Fin
87 86 a1i ⊢ ( ( ( ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 = ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) → ( 1 ..^ 𝑛 ) ∈ Fin )
88 80 adantr ⊢ ( ( ( ( ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 = ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ ( 1 ..^ 𝑛 ) ) → 𝑥 ⊆ 𝑡 )
89 82 adantr ⊢ ( ( ( ( ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 = ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ ( 1 ..^ 𝑛 ) ) → 𝑓 : ℕ ⟶ 𝑥 )
90 fzossnn ⊢ ( 1 ..^ 𝑛 ) ⊆ ℕ
91 90 a1i ⊢ ( ( ( ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 = ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) → ( 1 ..^ 𝑛 ) ⊆ ℕ )
92 91 sselda ⊢ ( ( ( ( ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 = ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ ( 1 ..^ 𝑛 ) ) → 𝑖 ∈ ℕ )
93 89 92 ffvelcdmd ⊢ ( ( ( ( ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 = ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ ( 1 ..^ 𝑛 ) ) → ( 𝑓 ‘ 𝑖 ) ∈ 𝑥 )
94 88 93 sseldd ⊢ ( ( ( ( ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 = ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ∧ 𝑖 ∈ ( 1 ..^ 𝑛 ) ) → ( 𝑓 ‘ 𝑖 ) ∈ 𝑡 )
95 1 2 76 77 85 87 94 sigapildsyslem ⊢ ( ( ( ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 = ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) → ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ∈ 𝑡 )
96 62 95 eqeltrd ⊢ ( ( ( ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ) ∧ 𝑛 ∈ ℕ ) ∧ 𝑦 = ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) → 𝑦 ∈ 𝑡 )
97 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) = ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) )
98 97 54 elrnmpti ⊢ ( 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ↔ ∃ 𝑛 ∈ ℕ 𝑦 = ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) )
99 98 bilani ⊢ ( ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ) → ∃ 𝑛 ∈ ℕ 𝑦 = ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) )
100 61 96 99 r19.29af ⊢ ( ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) ∧ 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ) → 𝑦 ∈ 𝑡 )
101 100 ex ⊢ ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) → ( 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) → 𝑦 ∈ 𝑡 ) )
102 101 ssrdv ⊢ ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) → ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ⊆ 𝑡 )
103 nnex ⊢ ℕ ∈ V
104 103 mptex ⊢ ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ∈ V
105 104 rnex ⊢ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ∈ V
106 elpwg ⊢ ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ∈ V → ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ∈ 𝒫 𝑡 ↔ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ⊆ 𝑡 ) )
107 105 106 ax-mp ⊢ ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ∈ 𝒫 𝑡 ↔ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ⊆ 𝑡 )
108 102 107 sylibr ⊢ ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) → ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ∈ 𝒫 𝑡 )
109 16 simp3d ⊢ ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) → ∀ 𝑥 ∈ 𝒫 𝑡 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑡 ) )
110 109 ad4antr ⊢ ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) → ∀ 𝑥 ∈ 𝒫 𝑡 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑡 ) )
111 nnct ⊢ ℕ ≼ ω
112 mptct ⊢ ( ℕ ≼ ω → ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ≼ ω )
113 111 112 ax-mp ⊢ ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ≼ ω
114 rnct ⊢ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ≼ ω → ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ≼ ω )
115 113 114 mp1i ⊢ ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) → ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ≼ ω )
116 42 iundisj2 ⊢ Disj 𝑛 ∈ ℕ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) )
117 disjrnmpt ⊢ ( Disj 𝑛 ∈ ℕ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) → Disj 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) 𝑦 )
118 116 117 mp1i ⊢ ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) → Disj 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) 𝑦 )
119 breq1 ⊢ ( 𝑥 = ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) → ( 𝑥 ≼ ω ↔ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ≼ ω ) )
120 disjeq1 ⊢ ( 𝑥 = ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) → ( Disj 𝑦 ∈ 𝑥 𝑦 ↔ Disj 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) 𝑦 ) )
121 119 120 anbi12d ⊢ ( 𝑥 = ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) → ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ↔ ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ≼ ω ∧ Disj 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) 𝑦 ) ) )
122 unieq ⊢ ( 𝑥 = ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) → ∪ 𝑥 = ∪ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) )
123 122 eleq1d ⊢ ( 𝑥 = ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) → ( ∪ 𝑥 ∈ 𝑡 ↔ ∪ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ∈ 𝑡 ) )
124 121 123 imbi12d ⊢ ( 𝑥 = ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) → ( ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑡 ) ↔ ( ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ≼ ω ∧ Disj 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) 𝑦 ) → ∪ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ∈ 𝑡 ) ) )
125 124 rspcv ⊢ ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ∈ 𝒫 𝑡 → ( ∀ 𝑥 ∈ 𝒫 𝑡 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑡 ) → ( ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ≼ ω ∧ Disj 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) 𝑦 ) → ∪ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ∈ 𝑡 ) ) )
126 125 imp ⊢ ( ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ∈ 𝒫 𝑡 ∧ ∀ 𝑥 ∈ 𝒫 𝑡 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑡 ) ) → ( ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ≼ ω ∧ Disj 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) 𝑦 ) → ∪ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ∈ 𝑡 ) )
127 126 imp ⊢ ( ( ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ∈ 𝒫 𝑡 ∧ ∀ 𝑥 ∈ 𝒫 𝑡 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ∪ 𝑥 ∈ 𝑡 ) ) ∧ ( ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ≼ ω ∧ Disj 𝑦 ∈ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) 𝑦 ) ) → ∪ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ∈ 𝑡 )
128 108 110 115 118 127 syl22anc ⊢ ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) → ∪ ran ( 𝑛 ∈ ℕ ↦ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ) ∈ 𝑡 )
129 55 128 eqeltrid ⊢ ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) → ∪ 𝑛 ∈ ℕ ( ( 𝑓 ‘ 𝑛 ) ∖ ∪ 𝑖 ∈ ( 1 ..^ 𝑛 ) ( 𝑓 ‘ 𝑖 ) ) ∈ 𝑡 )
130 51 129 eqeltrrd ⊢ ( ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) ∧ 𝑓 : ℕ –onto→ 𝑥 ) → ∪ 𝑥 ∈ 𝑡 )
131 41 130 exlimddv ⊢ ( ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) ∧ 𝑥 ≠ ∅ ) → ∪ 𝑥 ∈ 𝑡 )
132 31 131 pm2.61dane ⊢ ( ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) ∧ 𝑥 ≼ ω ) → ∪ 𝑥 ∈ 𝑡 )
133 132 ex ⊢ ( ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) ∧ 𝑥 ∈ 𝒫 𝑡 ) → ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑡 ) )
134 133 ralrimiva ⊢ ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) → ∀ 𝑥 ∈ 𝒫 𝑡 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑡 ) )
135 25 17 134 3jca ⊢ ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) → ( 𝑂 ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ( 𝑂 ∖ 𝑥 ) ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝒫 𝑡 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑡 ) ) )
136 11 135 jca ⊢ ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) → ( 𝑡 ⊆ 𝒫 𝑂 ∧ ( 𝑂 ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ( 𝑂 ∖ 𝑥 ) ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝒫 𝑡 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑡 ) ) ) )
137 vex ⊢ 𝑡 ∈ V
138 issiga ⊢ ( 𝑡 ∈ V → ( 𝑡 ∈ ( sigAlgebra ‘ 𝑂 ) ↔ ( 𝑡 ⊆ 𝒫 𝑂 ∧ ( 𝑂 ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ( 𝑂 ∖ 𝑥 ) ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝒫 𝑡 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑡 ) ) ) ) )
139 137 138 ax-mp ⊢ ( 𝑡 ∈ ( sigAlgebra ‘ 𝑂 ) ↔ ( 𝑡 ⊆ 𝒫 𝑂 ∧ ( 𝑂 ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝑡 ( 𝑂 ∖ 𝑥 ) ∈ 𝑡 ∧ ∀ 𝑥 ∈ 𝒫 𝑡 ( 𝑥 ≼ ω → ∪ 𝑥 ∈ 𝑡 ) ) ) )
140 136 139 sylibr ⊢ ( 𝑡 ∈ ( 𝑃 ∩ 𝐿 ) → 𝑡 ∈ ( sigAlgebra ‘ 𝑂 ) )
141 140 ssriv ⊢ ( 𝑃 ∩ 𝐿 ) ⊆ ( sigAlgebra ‘ 𝑂 )
142 5 141 eqssi ⊢ ( sigAlgebra ‘ 𝑂 ) = ( 𝑃 ∩ 𝐿 )