Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sigapildsys Structured version   Visualization version   GIF version

Theorem sigapildsys 30759
Description: Sigma-algebra are exactly classes which are both lambda and pi-systems. (Contributed by Thierry Arnoux, 13-Jun-2020.)
Hypotheses
Ref Expression
dynkin.p 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠}
dynkin.l 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥𝑠 (𝑂𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥𝑠))}
Assertion
Ref Expression
sigapildsys (sigAlgebra‘𝑂) = (𝑃𝐿)
Distinct variable groups:   𝑥,𝑠,𝑦   𝑥,𝐿,𝑦   𝑂,𝑠,𝑥   𝑥,𝑃,𝑦
Allowed substitution hints:   𝑃(𝑠)   𝐿(𝑠)   𝑂(𝑦)

Proof of Theorem sigapildsys
Dummy variables 𝑓 𝑖 𝑛 𝑡 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dynkin.p . . . 4 𝑃 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (fi‘𝑠) ⊆ 𝑠}
21sigapisys 30752 . . 3 (sigAlgebra‘𝑂) ⊆ 𝑃
3 dynkin.l . . . 4 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥𝑠 (𝑂𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥𝑠))}
43sigaldsys 30756 . . 3 (sigAlgebra‘𝑂) ⊆ 𝐿
52, 4ssini 4060 . 2 (sigAlgebra‘𝑂) ⊆ (𝑃𝐿)
6 id 22 . . . . . . . . 9 (𝑡 ∈ (𝑃𝐿) → 𝑡 ∈ (𝑃𝐿))
76elin1d 4029 . . . . . . . 8 (𝑡 ∈ (𝑃𝐿) → 𝑡𝑃)
81ispisys 30749 . . . . . . . 8 (𝑡𝑃 ↔ (𝑡 ∈ 𝒫 𝒫 𝑂 ∧ (fi‘𝑡) ⊆ 𝑡))
97, 8sylib 210 . . . . . . 7 (𝑡 ∈ (𝑃𝐿) → (𝑡 ∈ 𝒫 𝒫 𝑂 ∧ (fi‘𝑡) ⊆ 𝑡))
109simpld 490 . . . . . 6 (𝑡 ∈ (𝑃𝐿) → 𝑡 ∈ 𝒫 𝒫 𝑂)
1110elpwid 4390 . . . . 5 (𝑡 ∈ (𝑃𝐿) → 𝑡 ⊆ 𝒫 𝑂)
12 dif0 4180 . . . . . . 7 (𝑂 ∖ ∅) = 𝑂
136elin2d 4030 . . . . . . . . . . 11 (𝑡 ∈ (𝑃𝐿) → 𝑡𝐿)
143isldsys 30753 . . . . . . . . . . 11 (𝑡𝐿 ↔ (𝑡 ∈ 𝒫 𝒫 𝑂 ∧ (∅ ∈ 𝑡 ∧ ∀𝑥𝑡 (𝑂𝑥) ∈ 𝑡 ∧ ∀𝑥 ∈ 𝒫 𝑡((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥𝑡))))
1513, 14sylib 210 . . . . . . . . . 10 (𝑡 ∈ (𝑃𝐿) → (𝑡 ∈ 𝒫 𝒫 𝑂 ∧ (∅ ∈ 𝑡 ∧ ∀𝑥𝑡 (𝑂𝑥) ∈ 𝑡 ∧ ∀𝑥 ∈ 𝒫 𝑡((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥𝑡))))
1615simprd 491 . . . . . . . . 9 (𝑡 ∈ (𝑃𝐿) → (∅ ∈ 𝑡 ∧ ∀𝑥𝑡 (𝑂𝑥) ∈ 𝑡 ∧ ∀𝑥 ∈ 𝒫 𝑡((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥𝑡)))
1716simp2d 1177 . . . . . . . 8 (𝑡 ∈ (𝑃𝐿) → ∀𝑥𝑡 (𝑂𝑥) ∈ 𝑡)
1816simp1d 1176 . . . . . . . . 9 (𝑡 ∈ (𝑃𝐿) → ∅ ∈ 𝑡)
19 difeq2 3949 . . . . . . . . . . 11 (𝑥 = ∅ → (𝑂𝑥) = (𝑂 ∖ ∅))
20 eqidd 2826 . . . . . . . . . . 11 (𝑥 = ∅ → 𝑡 = 𝑡)
2119, 20eleq12d 2900 . . . . . . . . . 10 (𝑥 = ∅ → ((𝑂𝑥) ∈ 𝑡 ↔ (𝑂 ∖ ∅) ∈ 𝑡))
2221rspcv 3522 . . . . . . . . 9 (∅ ∈ 𝑡 → (∀𝑥𝑡 (𝑂𝑥) ∈ 𝑡 → (𝑂 ∖ ∅) ∈ 𝑡))
2318, 22syl 17 . . . . . . . 8 (𝑡 ∈ (𝑃𝐿) → (∀𝑥𝑡 (𝑂𝑥) ∈ 𝑡 → (𝑂 ∖ ∅) ∈ 𝑡))
2417, 23mpd 15 . . . . . . 7 (𝑡 ∈ (𝑃𝐿) → (𝑂 ∖ ∅) ∈ 𝑡)
2512, 24syl5eqelr 2911 . . . . . 6 (𝑡 ∈ (𝑃𝐿) → 𝑂𝑡)
26 unieq 4666 . . . . . . . . . . . 12 (𝑥 = ∅ → 𝑥 = ∅)
27 uni0 4687 . . . . . . . . . . . 12 ∅ = ∅
2826, 27syl6eq 2877 . . . . . . . . . . 11 (𝑥 = ∅ → 𝑥 = ∅)
2928adantl 475 . . . . . . . . . 10 ((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 = ∅) → 𝑥 = ∅)
3018ad3antrrr 721 . . . . . . . . . 10 ((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 = ∅) → ∅ ∈ 𝑡)
3129, 30eqeltrd 2906 . . . . . . . . 9 ((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 = ∅) → 𝑥𝑡)
32 vex 3417 . . . . . . . . . . . . . 14 𝑥 ∈ V
33320sdom 8360 . . . . . . . . . . . . 13 (∅ ≺ 𝑥𝑥 ≠ ∅)
3433biimpri 220 . . . . . . . . . . . 12 (𝑥 ≠ ∅ → ∅ ≺ 𝑥)
3534adantl 475 . . . . . . . . . . 11 ((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) → ∅ ≺ 𝑥)
36 simplr 785 . . . . . . . . . . . 12 ((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) → 𝑥 ≼ ω)
37 nnenom 13074 . . . . . . . . . . . . 13 ℕ ≈ ω
3837ensymi 8272 . . . . . . . . . . . 12 ω ≈ ℕ
39 domentr 8281 . . . . . . . . . . . 12 ((𝑥 ≼ ω ∧ ω ≈ ℕ) → 𝑥 ≼ ℕ)
4036, 38, 39sylancl 580 . . . . . . . . . . 11 ((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) → 𝑥 ≼ ℕ)
41 fodomr 8380 . . . . . . . . . . 11 ((∅ ≺ 𝑥𝑥 ≼ ℕ) → ∃𝑓 𝑓:ℕ–onto𝑥)
4235, 40, 41syl2anc 579 . . . . . . . . . 10 ((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) → ∃𝑓 𝑓:ℕ–onto𝑥)
43 fveq2 6433 . . . . . . . . . . . . . 14 (𝑛 = 𝑖 → (𝑓𝑛) = (𝑓𝑖))
4443iundisj 23714 . . . . . . . . . . . . 13 𝑛 ∈ ℕ (𝑓𝑛) = 𝑛 ∈ ℕ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))
45 fofn 6355 . . . . . . . . . . . . . . 15 (𝑓:ℕ–onto𝑥𝑓 Fn ℕ)
46 fniunfv 6760 . . . . . . . . . . . . . . 15 (𝑓 Fn ℕ → 𝑛 ∈ ℕ (𝑓𝑛) = ran 𝑓)
4745, 46syl 17 . . . . . . . . . . . . . 14 (𝑓:ℕ–onto𝑥 𝑛 ∈ ℕ (𝑓𝑛) = ran 𝑓)
48 forn 6356 . . . . . . . . . . . . . . 15 (𝑓:ℕ–onto𝑥 → ran 𝑓 = 𝑥)
4948unieqd 4668 . . . . . . . . . . . . . 14 (𝑓:ℕ–onto𝑥 ran 𝑓 = 𝑥)
5047, 49eqtrd 2861 . . . . . . . . . . . . 13 (𝑓:ℕ–onto𝑥 𝑛 ∈ ℕ (𝑓𝑛) = 𝑥)
5144, 50syl5eqr 2875 . . . . . . . . . . . 12 (𝑓:ℕ–onto𝑥 𝑛 ∈ ℕ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)) = 𝑥)
5251adantl 475 . . . . . . . . . . 11 (((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) → 𝑛 ∈ ℕ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)) = 𝑥)
53 fvex 6446 . . . . . . . . . . . . . 14 (𝑓𝑛) ∈ V
54 difexg 5033 . . . . . . . . . . . . . 14 ((𝑓𝑛) ∈ V → ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)) ∈ V)
5553, 54ax-mp 5 . . . . . . . . . . . . 13 ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)) ∈ V
5655dfiun3 5613 . . . . . . . . . . . 12 𝑛 ∈ ℕ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)) = ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))
57 nfv 2013 . . . . . . . . . . . . . . . . . 18 𝑛((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥)
58 nfcv 2969 . . . . . . . . . . . . . . . . . . 19 𝑛𝑦
59 nfmpt1 4970 . . . . . . . . . . . . . . . . . . . 20 𝑛(𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))
6059nfrn 5601 . . . . . . . . . . . . . . . . . . 19 𝑛ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))
6158, 60nfel 2982 . . . . . . . . . . . . . . . . . 18 𝑛 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))
6257, 61nfan 2002 . . . . . . . . . . . . . . . . 17 𝑛(((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) ∧ 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))))
63 simpr 479 . . . . . . . . . . . . . . . . . 18 ((((((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) ∧ 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))) ∧ 𝑛 ∈ ℕ) ∧ 𝑦 = ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) → 𝑦 = ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))
64 nfv 2013 . . . . . . . . . . . . . . . . . . . . . 22 𝑖((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥)
65 nfcv 2969 . . . . . . . . . . . . . . . . . . . . . . 23 𝑖𝑦
66 nfcv 2969 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑖
67 nfcv 2969 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑖(𝑓𝑛)
68 nfiu1 4770 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑖 𝑖 ∈ (1..^𝑛)(𝑓𝑖)
6967, 68nfdif 3958 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑖((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))
7066, 69nfmpt 4969 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑖(𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))
7170nfrn 5601 . . . . . . . . . . . . . . . . . . . . . . 23 𝑖ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))
7265, 71nfel 2982 . . . . . . . . . . . . . . . . . . . . . 22 𝑖 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))
7364, 72nfan 2002 . . . . . . . . . . . . . . . . . . . . 21 𝑖(((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) ∧ 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))))
74 nfv 2013 . . . . . . . . . . . . . . . . . . . . 21 𝑖 𝑛 ∈ ℕ
7573, 74nfan 2002 . . . . . . . . . . . . . . . . . . . 20 𝑖((((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) ∧ 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))) ∧ 𝑛 ∈ ℕ)
7665, 69nfeq 2981 . . . . . . . . . . . . . . . . . . . 20 𝑖 𝑦 = ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))
7775, 76nfan 2002 . . . . . . . . . . . . . . . . . . 19 𝑖(((((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) ∧ 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))) ∧ 𝑛 ∈ ℕ) ∧ 𝑦 = ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))
786ad7antr 736 . . . . . . . . . . . . . . . . . . 19 ((((((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) ∧ 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))) ∧ 𝑛 ∈ ℕ) ∧ 𝑦 = ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) → 𝑡 ∈ (𝑃𝐿))
79 simp-4r 803 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) → 𝑥 ∈ 𝒫 𝑡)
8079ad3antrrr 721 . . . . . . . . . . . . . . . . . . . . 21 ((((((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) ∧ 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))) ∧ 𝑛 ∈ ℕ) ∧ 𝑦 = ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) → 𝑥 ∈ 𝒫 𝑡)
8180elpwid 4390 . . . . . . . . . . . . . . . . . . . 20 ((((((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) ∧ 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))) ∧ 𝑛 ∈ ℕ) ∧ 𝑦 = ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) → 𝑥𝑡)
82 fof 6353 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓:ℕ–onto𝑥𝑓:ℕ⟶𝑥)
8382ad4antlr 726 . . . . . . . . . . . . . . . . . . . . 21 ((((((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) ∧ 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))) ∧ 𝑛 ∈ ℕ) ∧ 𝑦 = ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) → 𝑓:ℕ⟶𝑥)
84 simplr 785 . . . . . . . . . . . . . . . . . . . . 21 ((((((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) ∧ 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))) ∧ 𝑛 ∈ ℕ) ∧ 𝑦 = ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) → 𝑛 ∈ ℕ)
8583, 84ffvelrnd 6609 . . . . . . . . . . . . . . . . . . . 20 ((((((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) ∧ 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))) ∧ 𝑛 ∈ ℕ) ∧ 𝑦 = ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) → (𝑓𝑛) ∈ 𝑥)
8681, 85sseldd 3828 . . . . . . . . . . . . . . . . . . 19 ((((((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) ∧ 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))) ∧ 𝑛 ∈ ℕ) ∧ 𝑦 = ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) → (𝑓𝑛) ∈ 𝑡)
87 fzofi 13068 . . . . . . . . . . . . . . . . . . . 20 (1..^𝑛) ∈ Fin
8887a1i 11 . . . . . . . . . . . . . . . . . . 19 ((((((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) ∧ 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))) ∧ 𝑛 ∈ ℕ) ∧ 𝑦 = ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) → (1..^𝑛) ∈ Fin)
8981adantr 474 . . . . . . . . . . . . . . . . . . . 20 (((((((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) ∧ 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))) ∧ 𝑛 ∈ ℕ) ∧ 𝑦 = ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ∧ 𝑖 ∈ (1..^𝑛)) → 𝑥𝑡)
9083adantr 474 . . . . . . . . . . . . . . . . . . . . 21 (((((((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) ∧ 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))) ∧ 𝑛 ∈ ℕ) ∧ 𝑦 = ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ∧ 𝑖 ∈ (1..^𝑛)) → 𝑓:ℕ⟶𝑥)
91 fzossnn 12812 . . . . . . . . . . . . . . . . . . . . . . 23 (1..^𝑛) ⊆ ℕ
9291a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((((((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) ∧ 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))) ∧ 𝑛 ∈ ℕ) ∧ 𝑦 = ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) → (1..^𝑛) ⊆ ℕ)
9392sselda 3827 . . . . . . . . . . . . . . . . . . . . 21 (((((((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) ∧ 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))) ∧ 𝑛 ∈ ℕ) ∧ 𝑦 = ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ∧ 𝑖 ∈ (1..^𝑛)) → 𝑖 ∈ ℕ)
9490, 93ffvelrnd 6609 . . . . . . . . . . . . . . . . . . . 20 (((((((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) ∧ 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))) ∧ 𝑛 ∈ ℕ) ∧ 𝑦 = ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ∧ 𝑖 ∈ (1..^𝑛)) → (𝑓𝑖) ∈ 𝑥)
9589, 94sseldd 3828 . . . . . . . . . . . . . . . . . . 19 (((((((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) ∧ 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))) ∧ 𝑛 ∈ ℕ) ∧ 𝑦 = ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ∧ 𝑖 ∈ (1..^𝑛)) → (𝑓𝑖) ∈ 𝑡)
961, 3, 77, 78, 86, 88, 95sigapildsyslem 30758 . . . . . . . . . . . . . . . . . 18 ((((((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) ∧ 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))) ∧ 𝑛 ∈ ℕ) ∧ 𝑦 = ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) → ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)) ∈ 𝑡)
9763, 96eqeltrd 2906 . . . . . . . . . . . . . . . . 17 ((((((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) ∧ 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))) ∧ 𝑛 ∈ ℕ) ∧ 𝑦 = ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) → 𝑦𝑡)
98 simpr 479 . . . . . . . . . . . . . . . . . 18 ((((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) ∧ 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))) → 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))))
99 eqid 2825 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) = (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))
10099, 55elrnmpti 5609 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ↔ ∃𝑛 ∈ ℕ 𝑦 = ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))
10198, 100sylib 210 . . . . . . . . . . . . . . . . 17 ((((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) ∧ 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))) → ∃𝑛 ∈ ℕ 𝑦 = ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))
10262, 97, 101r19.29af 3286 . . . . . . . . . . . . . . . 16 ((((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) ∧ 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))) → 𝑦𝑡)
103102ex 403 . . . . . . . . . . . . . . 15 (((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) → (𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) → 𝑦𝑡))
104103ssrdv 3833 . . . . . . . . . . . . . 14 (((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) → ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ⊆ 𝑡)
105 nnex 11357 . . . . . . . . . . . . . . . . 17 ℕ ∈ V
106105mptex 6742 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ∈ V
107106rnex 7362 . . . . . . . . . . . . . . 15 ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ∈ V
108 elpwg 4386 . . . . . . . . . . . . . . 15 (ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ∈ V → (ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ∈ 𝒫 𝑡 ↔ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ⊆ 𝑡))
109107, 108ax-mp 5 . . . . . . . . . . . . . 14 (ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ∈ 𝒫 𝑡 ↔ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ⊆ 𝑡)
110104, 109sylibr 226 . . . . . . . . . . . . 13 (((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) → ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ∈ 𝒫 𝑡)
11116simp3d 1178 . . . . . . . . . . . . . 14 (𝑡 ∈ (𝑃𝐿) → ∀𝑥 ∈ 𝒫 𝑡((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥𝑡))
112111ad4antr 724 . . . . . . . . . . . . 13 (((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) → ∀𝑥 ∈ 𝒫 𝑡((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥𝑡))
113 nnct 13075 . . . . . . . . . . . . . . 15 ℕ ≼ ω
114 mptct 9675 . . . . . . . . . . . . . . 15 (ℕ ≼ ω → (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ≼ ω)
115113, 114ax-mp 5 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ≼ ω
116 rnct 9662 . . . . . . . . . . . . . 14 ((𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ≼ ω → ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ≼ ω)
117115, 116mp1i 13 . . . . . . . . . . . . 13 (((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) → ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ≼ ω)
11843iundisj2 23715 . . . . . . . . . . . . . 14 Disj 𝑛 ∈ ℕ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))
119 disjrnmpt 29934 . . . . . . . . . . . . . 14 (Disj 𝑛 ∈ ℕ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)) → Disj 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))𝑦)
120118, 119mp1i 13 . . . . . . . . . . . . 13 (((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) → Disj 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))𝑦)
121 breq1 4876 . . . . . . . . . . . . . . . . . 18 (𝑥 = ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) → (𝑥 ≼ ω ↔ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ≼ ω))
122 disjeq1 4848 . . . . . . . . . . . . . . . . . 18 (𝑥 = ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) → (Disj 𝑦𝑥 𝑦Disj 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))𝑦))
123121, 122anbi12d 624 . . . . . . . . . . . . . . . . 17 (𝑥 = ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) → ((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) ↔ (ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ≼ ω ∧ Disj 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))𝑦)))
124 unieq 4666 . . . . . . . . . . . . . . . . . 18 (𝑥 = ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) → 𝑥 = ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))))
125124eleq1d 2891 . . . . . . . . . . . . . . . . 17 (𝑥 = ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) → ( 𝑥𝑡 ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ∈ 𝑡))
126123, 125imbi12d 336 . . . . . . . . . . . . . . . 16 (𝑥 = ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) → (((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥𝑡) ↔ ((ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ≼ ω ∧ Disj 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))𝑦) → ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ∈ 𝑡)))
127126rspcv 3522 . . . . . . . . . . . . . . 15 (ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ∈ 𝒫 𝑡 → (∀𝑥 ∈ 𝒫 𝑡((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥𝑡) → ((ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ≼ ω ∧ Disj 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))𝑦) → ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ∈ 𝑡)))
128127imp 397 . . . . . . . . . . . . . 14 ((ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ∈ 𝒫 𝑡 ∧ ∀𝑥 ∈ 𝒫 𝑡((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥𝑡)) → ((ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ≼ ω ∧ Disj 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))𝑦) → ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ∈ 𝑡))
129128imp 397 . . . . . . . . . . . . 13 (((ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ∈ 𝒫 𝑡 ∧ ∀𝑥 ∈ 𝒫 𝑡((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥𝑡)) ∧ (ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ≼ ω ∧ Disj 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))𝑦)) → ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ∈ 𝑡)
130110, 112, 117, 120, 129syl22anc 872 . . . . . . . . . . . 12 (((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) → ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ∈ 𝑡)
13156, 130syl5eqel 2910 . . . . . . . . . . 11 (((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) → 𝑛 ∈ ℕ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)) ∈ 𝑡)
13252, 131eqeltrrd 2907 . . . . . . . . . 10 (((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) → 𝑥𝑡)
13342, 132exlimddv 2034 . . . . . . . . 9 ((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) → 𝑥𝑡)
13431, 133pm2.61dane 3086 . . . . . . . 8 (((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) → 𝑥𝑡)
135134ex 403 . . . . . . 7 ((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) → (𝑥 ≼ ω → 𝑥𝑡))
136135ralrimiva 3175 . . . . . 6 (𝑡 ∈ (𝑃𝐿) → ∀𝑥 ∈ 𝒫 𝑡(𝑥 ≼ ω → 𝑥𝑡))
13725, 17, 1363jca 1162 . . . . 5 (𝑡 ∈ (𝑃𝐿) → (𝑂𝑡 ∧ ∀𝑥𝑡 (𝑂𝑥) ∈ 𝑡 ∧ ∀𝑥 ∈ 𝒫 𝑡(𝑥 ≼ ω → 𝑥𝑡)))
13811, 137jca 507 . . . 4 (𝑡 ∈ (𝑃𝐿) → (𝑡 ⊆ 𝒫 𝑂 ∧ (𝑂𝑡 ∧ ∀𝑥𝑡 (𝑂𝑥) ∈ 𝑡 ∧ ∀𝑥 ∈ 𝒫 𝑡(𝑥 ≼ ω → 𝑥𝑡))))
139 vex 3417 . . . . 5 𝑡 ∈ V
140 issiga 30708 . . . . 5 (𝑡 ∈ V → (𝑡 ∈ (sigAlgebra‘𝑂) ↔ (𝑡 ⊆ 𝒫 𝑂 ∧ (𝑂𝑡 ∧ ∀𝑥𝑡 (𝑂𝑥) ∈ 𝑡 ∧ ∀𝑥 ∈ 𝒫 𝑡(𝑥 ≼ ω → 𝑥𝑡)))))
141139, 140ax-mp 5 . . . 4 (𝑡 ∈ (sigAlgebra‘𝑂) ↔ (𝑡 ⊆ 𝒫 𝑂 ∧ (𝑂𝑡 ∧ ∀𝑥𝑡 (𝑂𝑥) ∈ 𝑡 ∧ ∀𝑥 ∈ 𝒫 𝑡(𝑥 ≼ ω → 𝑥𝑡))))
142138, 141sylibr 226 . . 3 (𝑡 ∈ (𝑃𝐿) → 𝑡 ∈ (sigAlgebra‘𝑂))
143142ssriv 3831 . 2 (𝑃𝐿) ⊆ (sigAlgebra‘𝑂)
1445, 143eqssi 3843 1 (sigAlgebra‘𝑂) = (𝑃𝐿)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 386  w3a 1111   = wceq 1656  wex 1878  wcel 2164  wne 2999  wral 3117  wrex 3118  {crab 3121  Vcvv 3414  cdif 3795  cin 3797  wss 3798  c0 4144  𝒫 cpw 4378   cuni 4658   ciun 4740  Disj wdisj 4841   class class class wbr 4873  cmpt 4952  ran crn 5343   Fn wfn 6118  wf 6119  ontowfo 6121  cfv 6123  (class class class)co 6905  ωcom 7326  cen 8219  cdom 8220  csdm 8221  Fincfn 8222  ficfi 8585  1c1 10253  cn 11350  ..^cfzo 12760  sigAlgebracsiga 30704
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-rep 4994  ax-sep 5005  ax-nul 5013  ax-pow 5065  ax-pr 5127  ax-un 7209  ax-inf2 8815  ax-ac2 9600  ax-cnex 10308  ax-resscn 10309  ax-1cn 10310  ax-icn 10311  ax-addcl 10312  ax-addrcl 10313  ax-mulcl 10314  ax-mulrcl 10315  ax-mulcom 10316  ax-addass 10317  ax-mulass 10318  ax-distr 10319  ax-i2m1 10320  ax-1ne0 10321  ax-1rid 10322  ax-rnegex 10323  ax-rrecex 10324  ax-cnre 10325  ax-pre-lttri 10326  ax-pre-lttrn 10327  ax-pre-ltadd 10328  ax-pre-mulgt0 10329
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3or 1112  df-3an 1113  df-tru 1660  df-fal 1670  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-nel 3103  df-ral 3122  df-rex 3123  df-reu 3124  df-rmo 3125  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-pss 3814  df-nul 4145  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4659  df-int 4698  df-iun 4742  df-iin 4743  df-disj 4842  df-br 4874  df-opab 4936  df-mpt 4953  df-tr 4976  df-id 5250  df-eprel 5255  df-po 5263  df-so 5264  df-fr 5301  df-se 5302  df-we 5303  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-rn 5353  df-res 5354  df-ima 5355  df-pred 5920  df-ord 5966  df-on 5967  df-lim 5968  df-suc 5969  df-iota 6086  df-fun 6125  df-fn 6126  df-f 6127  df-f1 6128  df-fo 6129  df-f1o 6130  df-fv 6131  df-isom 6132  df-riota 6866  df-ov 6908  df-oprab 6909  df-mpt2 6910  df-om 7327  df-1st 7428  df-2nd 7429  df-wrecs 7672  df-recs 7734  df-rdg 7772  df-1o 7826  df-2o 7827  df-oadd 7830  df-er 8009  df-map 8124  df-en 8223  df-dom 8224  df-sdom 8225  df-fin 8226  df-fi 8586  df-sup 8617  df-inf 8618  df-oi 8684  df-card 9078  df-acn 9081  df-ac 9252  df-cda 9305  df-pnf 10393  df-mnf 10394  df-xr 10395  df-ltxr 10396  df-le 10397  df-sub 10587  df-neg 10588  df-nn 11351  df-n0 11619  df-z 11705  df-uz 11969  df-fz 12620  df-fzo 12761  df-siga 30705
This theorem is referenced by:  dynkin  30764
  Copyright terms: Public domain W3C validator