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 30030
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 30023 . . 3 (sigAlgebra‘𝑂) ⊆ 𝑃
3 dynkin.l . . . 4 𝐿 = {𝑠 ∈ 𝒫 𝒫 𝑂 ∣ (∅ ∈ 𝑠 ∧ ∀𝑥𝑠 (𝑂𝑥) ∈ 𝑠 ∧ ∀𝑥 ∈ 𝒫 𝑠((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥𝑠))}
43sigaldsys 30027 . . 3 (sigAlgebra‘𝑂) ⊆ 𝐿
52, 4ssini 3819 . 2 (sigAlgebra‘𝑂) ⊆ (𝑃𝐿)
6 id 22 . . . . . . . . 9 (𝑡 ∈ (𝑃𝐿) → 𝑡 ∈ (𝑃𝐿))
76elin1d 3785 . . . . . . . 8 (𝑡 ∈ (𝑃𝐿) → 𝑡𝑃)
81ispisys 30020 . . . . . . . 8 (𝑡𝑃 ↔ (𝑡 ∈ 𝒫 𝒫 𝑂 ∧ (fi‘𝑡) ⊆ 𝑡))
97, 8sylib 208 . . . . . . 7 (𝑡 ∈ (𝑃𝐿) → (𝑡 ∈ 𝒫 𝒫 𝑂 ∧ (fi‘𝑡) ⊆ 𝑡))
109simpld 475 . . . . . 6 (𝑡 ∈ (𝑃𝐿) → 𝑡 ∈ 𝒫 𝒫 𝑂)
1110elpwid 4146 . . . . 5 (𝑡 ∈ (𝑃𝐿) → 𝑡 ⊆ 𝒫 𝑂)
12 dif0 3929 . . . . . . 7 (𝑂 ∖ ∅) = 𝑂
136elin2d 3786 . . . . . . . . . . 11 (𝑡 ∈ (𝑃𝐿) → 𝑡𝐿)
143isldsys 30024 . . . . . . . . . . 11 (𝑡𝐿 ↔ (𝑡 ∈ 𝒫 𝒫 𝑂 ∧ (∅ ∈ 𝑡 ∧ ∀𝑥𝑡 (𝑂𝑥) ∈ 𝑡 ∧ ∀𝑥 ∈ 𝒫 𝑡((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥𝑡))))
1513, 14sylib 208 . . . . . . . . . 10 (𝑡 ∈ (𝑃𝐿) → (𝑡 ∈ 𝒫 𝒫 𝑂 ∧ (∅ ∈ 𝑡 ∧ ∀𝑥𝑡 (𝑂𝑥) ∈ 𝑡 ∧ ∀𝑥 ∈ 𝒫 𝑡((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥𝑡))))
1615simprd 479 . . . . . . . . 9 (𝑡 ∈ (𝑃𝐿) → (∅ ∈ 𝑡 ∧ ∀𝑥𝑡 (𝑂𝑥) ∈ 𝑡 ∧ ∀𝑥 ∈ 𝒫 𝑡((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥𝑡)))
1716simp2d 1072 . . . . . . . 8 (𝑡 ∈ (𝑃𝐿) → ∀𝑥𝑡 (𝑂𝑥) ∈ 𝑡)
1816simp1d 1071 . . . . . . . . 9 (𝑡 ∈ (𝑃𝐿) → ∅ ∈ 𝑡)
19 difeq2 3705 . . . . . . . . . . 11 (𝑥 = ∅ → (𝑂𝑥) = (𝑂 ∖ ∅))
20 eqidd 2622 . . . . . . . . . . 11 (𝑥 = ∅ → 𝑡 = 𝑡)
2119, 20eleq12d 2692 . . . . . . . . . 10 (𝑥 = ∅ → ((𝑂𝑥) ∈ 𝑡 ↔ (𝑂 ∖ ∅) ∈ 𝑡))
2221rspcv 3294 . . . . . . . . 9 (∅ ∈ 𝑡 → (∀𝑥𝑡 (𝑂𝑥) ∈ 𝑡 → (𝑂 ∖ ∅) ∈ 𝑡))
2318, 22syl 17 . . . . . . . 8 (𝑡 ∈ (𝑃𝐿) → (∀𝑥𝑡 (𝑂𝑥) ∈ 𝑡 → (𝑂 ∖ ∅) ∈ 𝑡))
2417, 23mpd 15 . . . . . . 7 (𝑡 ∈ (𝑃𝐿) → (𝑂 ∖ ∅) ∈ 𝑡)
2512, 24syl5eqelr 2703 . . . . . 6 (𝑡 ∈ (𝑃𝐿) → 𝑂𝑡)
26 unieq 4415 . . . . . . . . . . . 12 (𝑥 = ∅ → 𝑥 = ∅)
27 uni0 4436 . . . . . . . . . . . 12 ∅ = ∅
2826, 27syl6eq 2671 . . . . . . . . . . 11 (𝑥 = ∅ → 𝑥 = ∅)
2928adantl 482 . . . . . . . . . 10 ((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 = ∅) → 𝑥 = ∅)
3018ad3antrrr 765 . . . . . . . . . 10 ((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 = ∅) → ∅ ∈ 𝑡)
3129, 30eqeltrd 2698 . . . . . . . . 9 ((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 = ∅) → 𝑥𝑡)
32 vex 3192 . . . . . . . . . . . . . 14 𝑥 ∈ V
33320sdom 8043 . . . . . . . . . . . . 13 (∅ ≺ 𝑥𝑥 ≠ ∅)
3433biimpri 218 . . . . . . . . . . . 12 (𝑥 ≠ ∅ → ∅ ≺ 𝑥)
3534adantl 482 . . . . . . . . . . 11 ((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) → ∅ ≺ 𝑥)
36 simplr 791 . . . . . . . . . . . 12 ((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) → 𝑥 ≼ ω)
37 nnenom 12727 . . . . . . . . . . . . 13 ℕ ≈ ω
3837ensymi 7958 . . . . . . . . . . . 12 ω ≈ ℕ
39 domentr 7967 . . . . . . . . . . . 12 ((𝑥 ≼ ω ∧ ω ≈ ℕ) → 𝑥 ≼ ℕ)
4036, 38, 39sylancl 693 . . . . . . . . . . 11 ((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) → 𝑥 ≼ ℕ)
41 fodomr 8063 . . . . . . . . . . 11 ((∅ ≺ 𝑥𝑥 ≼ ℕ) → ∃𝑓 𝑓:ℕ–onto𝑥)
4235, 40, 41syl2anc 692 . . . . . . . . . 10 ((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) → ∃𝑓 𝑓:ℕ–onto𝑥)
43 fveq2 6153 . . . . . . . . . . . . . 14 (𝑛 = 𝑖 → (𝑓𝑛) = (𝑓𝑖))
4443iundisj 23239 . . . . . . . . . . . . 13 𝑛 ∈ ℕ (𝑓𝑛) = 𝑛 ∈ ℕ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))
45 fofn 6079 . . . . . . . . . . . . . . 15 (𝑓:ℕ–onto𝑥𝑓 Fn ℕ)
46 fniunfv 6465 . . . . . . . . . . . . . . 15 (𝑓 Fn ℕ → 𝑛 ∈ ℕ (𝑓𝑛) = ran 𝑓)
4745, 46syl 17 . . . . . . . . . . . . . 14 (𝑓:ℕ–onto𝑥 𝑛 ∈ ℕ (𝑓𝑛) = ran 𝑓)
48 forn 6080 . . . . . . . . . . . . . . 15 (𝑓:ℕ–onto𝑥 → ran 𝑓 = 𝑥)
4948unieqd 4417 . . . . . . . . . . . . . 14 (𝑓:ℕ–onto𝑥 ran 𝑓 = 𝑥)
5047, 49eqtrd 2655 . . . . . . . . . . . . 13 (𝑓:ℕ–onto𝑥 𝑛 ∈ ℕ (𝑓𝑛) = 𝑥)
5144, 50syl5eqr 2669 . . . . . . . . . . . 12 (𝑓:ℕ–onto𝑥 𝑛 ∈ ℕ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)) = 𝑥)
5251adantl 482 . . . . . . . . . . 11 (((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) → 𝑛 ∈ ℕ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)) = 𝑥)
53 fvex 6163 . . . . . . . . . . . . . 14 (𝑓𝑛) ∈ V
54 difexg 4773 . . . . . . . . . . . . . 14 ((𝑓𝑛) ∈ V → ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)) ∈ V)
5553, 54ax-mp 5 . . . . . . . . . . . . 13 ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)) ∈ V
5655dfiun3 5345 . . . . . . . . . . . 12 𝑛 ∈ ℕ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)) = ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))
57 nfv 1840 . . . . . . . . . . . . . . . . . 18 𝑛((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥)
58 nfcv 2761 . . . . . . . . . . . . . . . . . . 19 𝑛𝑦
59 nfmpt1 4712 . . . . . . . . . . . . . . . . . . . 20 𝑛(𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))
6059nfrn 5333 . . . . . . . . . . . . . . . . . . 19 𝑛ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))
6158, 60nfel 2773 . . . . . . . . . . . . . . . . . 18 𝑛 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))
6257, 61nfan 1825 . . . . . . . . . . . . . . . . 17 𝑛(((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) ∧ 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))))
63 simpr 477 . . . . . . . . . . . . . . . . . 18 ((((((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) ∧ 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))) ∧ 𝑛 ∈ ℕ) ∧ 𝑦 = ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) → 𝑦 = ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))
64 nfv 1840 . . . . . . . . . . . . . . . . . . . . . 22 𝑖((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥)
65 nfcv 2761 . . . . . . . . . . . . . . . . . . . . . . 23 𝑖𝑦
66 nfcv 2761 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑖
67 nfcv 2761 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑖(𝑓𝑛)
68 nfiu1 4521 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑖 𝑖 ∈ (1..^𝑛)(𝑓𝑖)
6967, 68nfdif 3714 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑖((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))
7066, 69nfmpt 4711 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑖(𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))
7170nfrn 5333 . . . . . . . . . . . . . . . . . . . . . . 23 𝑖ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))
7265, 71nfel 2773 . . . . . . . . . . . . . . . . . . . . . 22 𝑖 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))
7364, 72nfan 1825 . . . . . . . . . . . . . . . . . . . . 21 𝑖(((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) ∧ 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))))
74 nfv 1840 . . . . . . . . . . . . . . . . . . . . 21 𝑖 𝑛 ∈ ℕ
7573, 74nfan 1825 . . . . . . . . . . . . . . . . . . . 20 𝑖((((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) ∧ 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))) ∧ 𝑛 ∈ ℕ)
7665, 69nfeq 2772 . . . . . . . . . . . . . . . . . . . 20 𝑖 𝑦 = ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))
7775, 76nfan 1825 . . . . . . . . . . . . . . . . . . 19 𝑖(((((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) ∧ 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))) ∧ 𝑛 ∈ ℕ) ∧ 𝑦 = ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))
786ad7antr 773 . . . . . . . . . . . . . . . . . . 19 ((((((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) ∧ 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))) ∧ 𝑛 ∈ ℕ) ∧ 𝑦 = ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) → 𝑡 ∈ (𝑃𝐿))
79 simp-4r 806 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) → 𝑥 ∈ 𝒫 𝑡)
8079ad3antrrr 765 . . . . . . . . . . . . . . . . . . . . 21 ((((((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) ∧ 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))) ∧ 𝑛 ∈ ℕ) ∧ 𝑦 = ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) → 𝑥 ∈ 𝒫 𝑡)
8180elpwid 4146 . . . . . . . . . . . . . . . . . . . 20 ((((((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) ∧ 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))) ∧ 𝑛 ∈ ℕ) ∧ 𝑦 = ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) → 𝑥𝑡)
82 fof 6077 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓:ℕ–onto𝑥𝑓:ℕ⟶𝑥)
8382ad4antlr 768 . . . . . . . . . . . . . . . . . . . . 21 ((((((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) ∧ 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))) ∧ 𝑛 ∈ ℕ) ∧ 𝑦 = ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) → 𝑓:ℕ⟶𝑥)
84 simplr 791 . . . . . . . . . . . . . . . . . . . . 21 ((((((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) ∧ 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))) ∧ 𝑛 ∈ ℕ) ∧ 𝑦 = ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) → 𝑛 ∈ ℕ)
8583, 84ffvelrnd 6321 . . . . . . . . . . . . . . . . . . . 20 ((((((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) ∧ 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))) ∧ 𝑛 ∈ ℕ) ∧ 𝑦 = ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) → (𝑓𝑛) ∈ 𝑥)
8681, 85sseldd 3588 . . . . . . . . . . . . . . . . . . 19 ((((((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) ∧ 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))) ∧ 𝑛 ∈ ℕ) ∧ 𝑦 = ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) → (𝑓𝑛) ∈ 𝑡)
87 fzofi 12721 . . . . . . . . . . . . . . . . . . . 20 (1..^𝑛) ∈ Fin
8887a1i 11 . . . . . . . . . . . . . . . . . . 19 ((((((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) ∧ 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))) ∧ 𝑛 ∈ ℕ) ∧ 𝑦 = ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) → (1..^𝑛) ∈ Fin)
8981adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((((((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) ∧ 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))) ∧ 𝑛 ∈ ℕ) ∧ 𝑦 = ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ∧ 𝑖 ∈ (1..^𝑛)) → 𝑥𝑡)
9083adantr 481 . . . . . . . . . . . . . . . . . . . . 21 (((((((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) ∧ 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))) ∧ 𝑛 ∈ ℕ) ∧ 𝑦 = ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ∧ 𝑖 ∈ (1..^𝑛)) → 𝑓:ℕ⟶𝑥)
91 fzossnn 12465 . . . . . . . . . . . . . . . . . . . . . . 23 (1..^𝑛) ⊆ ℕ
9291a1i 11 . . . . . . . . . . . . . . . . . . . . . 22 ((((((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) ∧ 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))) ∧ 𝑛 ∈ ℕ) ∧ 𝑦 = ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) → (1..^𝑛) ⊆ ℕ)
9392sselda 3587 . . . . . . . . . . . . . . . . . . . . 21 (((((((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) ∧ 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))) ∧ 𝑛 ∈ ℕ) ∧ 𝑦 = ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ∧ 𝑖 ∈ (1..^𝑛)) → 𝑖 ∈ ℕ)
9490, 93ffvelrnd 6321 . . . . . . . . . . . . . . . . . . . 20 (((((((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) ∧ 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))) ∧ 𝑛 ∈ ℕ) ∧ 𝑦 = ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ∧ 𝑖 ∈ (1..^𝑛)) → (𝑓𝑖) ∈ 𝑥)
9589, 94sseldd 3588 . . . . . . . . . . . . . . . . . . 19 (((((((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) ∧ 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))) ∧ 𝑛 ∈ ℕ) ∧ 𝑦 = ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ∧ 𝑖 ∈ (1..^𝑛)) → (𝑓𝑖) ∈ 𝑡)
961, 3, 77, 78, 86, 88, 95sigapildsyslem 30029 . . . . . . . . . . . . . . . . . 18 ((((((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) ∧ 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))) ∧ 𝑛 ∈ ℕ) ∧ 𝑦 = ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) → ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)) ∈ 𝑡)
9763, 96eqeltrd 2698 . . . . . . . . . . . . . . . . 17 ((((((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) ∧ 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))) ∧ 𝑛 ∈ ℕ) ∧ 𝑦 = ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) → 𝑦𝑡)
98 simpr 477 . . . . . . . . . . . . . . . . . 18 ((((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) ∧ 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))) → 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))))
99 eqid 2621 . . . . . . . . . . . . . . . . . . 19 (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) = (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))
10099, 55elrnmpti 5341 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ↔ ∃𝑛 ∈ ℕ 𝑦 = ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))
10198, 100sylib 208 . . . . . . . . . . . . . . . . 17 ((((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) ∧ 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))) → ∃𝑛 ∈ ℕ 𝑦 = ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))
10262, 97, 101r19.29af 3070 . . . . . . . . . . . . . . . 16 ((((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) ∧ 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))) → 𝑦𝑡)
103102ex 450 . . . . . . . . . . . . . . 15 (((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) → (𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) → 𝑦𝑡))
104103ssrdv 3593 . . . . . . . . . . . . . 14 (((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) → ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ⊆ 𝑡)
105 nnex 10978 . . . . . . . . . . . . . . . . 17 ℕ ∈ V
106105mptex 6446 . . . . . . . . . . . . . . . 16 (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ∈ V
107106rnex 7054 . . . . . . . . . . . . . . 15 ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ∈ V
108 elpwg 4143 . . . . . . . . . . . . . . 15 (ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ∈ V → (ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ∈ 𝒫 𝑡 ↔ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ⊆ 𝑡))
109107, 108ax-mp 5 . . . . . . . . . . . . . 14 (ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ∈ 𝒫 𝑡 ↔ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ⊆ 𝑡)
110104, 109sylibr 224 . . . . . . . . . . . . 13 (((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) → ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ∈ 𝒫 𝑡)
11116simp3d 1073 . . . . . . . . . . . . . 14 (𝑡 ∈ (𝑃𝐿) → ∀𝑥 ∈ 𝒫 𝑡((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥𝑡))
112111ad4antr 767 . . . . . . . . . . . . 13 (((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) → ∀𝑥 ∈ 𝒫 𝑡((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥𝑡))
113 nnct 12728 . . . . . . . . . . . . . . 15 ℕ ≼ ω
114 mptct 9312 . . . . . . . . . . . . . . 15 (ℕ ≼ ω → (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ≼ ω)
115113, 114ax-mp 5 . . . . . . . . . . . . . 14 (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ≼ ω
116 rnct 9299 . . . . . . . . . . . . . 14 ((𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ≼ ω → ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ≼ ω)
117115, 116mp1i 13 . . . . . . . . . . . . 13 (((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) → ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ≼ ω)
11843iundisj2 23240 . . . . . . . . . . . . . 14 Disj 𝑛 ∈ ℕ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))
119 disjrnmpt 29266 . . . . . . . . . . . . . 14 (Disj 𝑛 ∈ ℕ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)) → Disj 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))𝑦)
120118, 119mp1i 13 . . . . . . . . . . . . 13 (((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) → Disj 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))𝑦)
121 breq1 4621 . . . . . . . . . . . . . . . . . 18 (𝑥 = ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) → (𝑥 ≼ ω ↔ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ≼ ω))
122 disjeq1 4595 . . . . . . . . . . . . . . . . . 18 (𝑥 = ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) → (Disj 𝑦𝑥 𝑦Disj 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))𝑦))
123121, 122anbi12d 746 . . . . . . . . . . . . . . . . 17 (𝑥 = ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) → ((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) ↔ (ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ≼ ω ∧ Disj 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))𝑦)))
124 unieq 4415 . . . . . . . . . . . . . . . . . 18 (𝑥 = ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) → 𝑥 = ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))))
125124eleq1d 2683 . . . . . . . . . . . . . . . . 17 (𝑥 = ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) → ( 𝑥𝑡 ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ∈ 𝑡))
126123, 125imbi12d 334 . . . . . . . . . . . . . . . 16 (𝑥 = ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) → (((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥𝑡) ↔ ((ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ≼ ω ∧ Disj 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))𝑦) → ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ∈ 𝑡)))
127126rspcv 3294 . . . . . . . . . . . . . . 15 (ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ∈ 𝒫 𝑡 → (∀𝑥 ∈ 𝒫 𝑡((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥𝑡) → ((ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ≼ ω ∧ Disj 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))𝑦) → ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ∈ 𝑡)))
128127imp 445 . . . . . . . . . . . . . 14 ((ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ∈ 𝒫 𝑡 ∧ ∀𝑥 ∈ 𝒫 𝑡((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥𝑡)) → ((ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ≼ ω ∧ Disj 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))𝑦) → ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ∈ 𝑡))
129128imp 445 . . . . . . . . . . . . 13 (((ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ∈ 𝒫 𝑡 ∧ ∀𝑥 ∈ 𝒫 𝑡((𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦) → 𝑥𝑡)) ∧ (ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ≼ ω ∧ Disj 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)))𝑦)) → ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ∈ 𝑡)
130110, 112, 117, 120, 129syl22anc 1324 . . . . . . . . . . . 12 (((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) → ran (𝑛 ∈ ℕ ↦ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖))) ∈ 𝑡)
13156, 130syl5eqel 2702 . . . . . . . . . . 11 (((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) → 𝑛 ∈ ℕ ((𝑓𝑛) ∖ 𝑖 ∈ (1..^𝑛)(𝑓𝑖)) ∈ 𝑡)
13252, 131eqeltrrd 2699 . . . . . . . . . 10 (((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) ∧ 𝑓:ℕ–onto𝑥) → 𝑥𝑡)
13342, 132exlimddv 1860 . . . . . . . . 9 ((((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) ∧ 𝑥 ≠ ∅) → 𝑥𝑡)
13431, 133pm2.61dane 2877 . . . . . . . 8 (((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) ∧ 𝑥 ≼ ω) → 𝑥𝑡)
135134ex 450 . . . . . . 7 ((𝑡 ∈ (𝑃𝐿) ∧ 𝑥 ∈ 𝒫 𝑡) → (𝑥 ≼ ω → 𝑥𝑡))
136135ralrimiva 2961 . . . . . 6 (𝑡 ∈ (𝑃𝐿) → ∀𝑥 ∈ 𝒫 𝑡(𝑥 ≼ ω → 𝑥𝑡))
13725, 17, 1363jca 1240 . . . . 5 (𝑡 ∈ (𝑃𝐿) → (𝑂𝑡 ∧ ∀𝑥𝑡 (𝑂𝑥) ∈ 𝑡 ∧ ∀𝑥 ∈ 𝒫 𝑡(𝑥 ≼ ω → 𝑥𝑡)))
13811, 137jca 554 . . . 4 (𝑡 ∈ (𝑃𝐿) → (𝑡 ⊆ 𝒫 𝑂 ∧ (𝑂𝑡 ∧ ∀𝑥𝑡 (𝑂𝑥) ∈ 𝑡 ∧ ∀𝑥 ∈ 𝒫 𝑡(𝑥 ≼ ω → 𝑥𝑡))))
139 vex 3192 . . . . 5 𝑡 ∈ V
140 issiga 29979 . . . . 5 (𝑡 ∈ V → (𝑡 ∈ (sigAlgebra‘𝑂) ↔ (𝑡 ⊆ 𝒫 𝑂 ∧ (𝑂𝑡 ∧ ∀𝑥𝑡 (𝑂𝑥) ∈ 𝑡 ∧ ∀𝑥 ∈ 𝒫 𝑡(𝑥 ≼ ω → 𝑥𝑡)))))
141139, 140ax-mp 5 . . . 4 (𝑡 ∈ (sigAlgebra‘𝑂) ↔ (𝑡 ⊆ 𝒫 𝑂 ∧ (𝑂𝑡 ∧ ∀𝑥𝑡 (𝑂𝑥) ∈ 𝑡 ∧ ∀𝑥 ∈ 𝒫 𝑡(𝑥 ≼ ω → 𝑥𝑡))))
142138, 141sylibr 224 . . 3 (𝑡 ∈ (𝑃𝐿) → 𝑡 ∈ (sigAlgebra‘𝑂))
143142ssriv 3591 . 2 (𝑃𝐿) ⊆ (sigAlgebra‘𝑂)
1445, 143eqssi 3603 1 (sigAlgebra‘𝑂) = (𝑃𝐿)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1036   = wceq 1480  wex 1701  wcel 1987  wne 2790  wral 2907  wrex 2908  {crab 2911  Vcvv 3189  cdif 3556  cin 3558  wss 3559  c0 3896  𝒫 cpw 4135   cuni 4407   ciun 4490  Disj wdisj 4588   class class class wbr 4618  cmpt 4678  ran crn 5080   Fn wfn 5847  wf 5848  ontowfo 5850  cfv 5852  (class class class)co 6610  ωcom 7019  cen 7904  cdom 7905  csdm 7906  Fincfn 7907  ficfi 8268  1c1 9889  cn 10972  ..^cfzo 12414  sigAlgebracsiga 29975
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-inf2 8490  ax-ac2 9237  ax-cnex 9944  ax-resscn 9945  ax-1cn 9946  ax-icn 9947  ax-addcl 9948  ax-addrcl 9949  ax-mulcl 9950  ax-mulrcl 9951  ax-mulcom 9952  ax-addass 9953  ax-mulass 9954  ax-distr 9955  ax-i2m1 9956  ax-1ne0 9957  ax-1rid 9958  ax-rnegex 9959  ax-rrecex 9960  ax-cnre 9961  ax-pre-lttri 9962  ax-pre-lttrn 9963  ax-pre-ltadd 9964  ax-pre-mulgt0 9965
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-iin 4493  df-disj 4589  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-se 5039  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-isom 5861  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-om 7020  df-1st 7120  df-2nd 7121  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-1o 7512  df-2o 7513  df-oadd 7516  df-er 7694  df-map 7811  df-en 7908  df-dom 7909  df-sdom 7910  df-fin 7911  df-fi 8269  df-sup 8300  df-inf 8301  df-oi 8367  df-card 8717  df-acn 8720  df-ac 8891  df-cda 8942  df-pnf 10028  df-mnf 10029  df-xr 10030  df-ltxr 10031  df-le 10032  df-sub 10220  df-neg 10221  df-nn 10973  df-n0 11245  df-z 11330  df-uz 11640  df-fz 12277  df-fzo 12415  df-siga 29976
This theorem is referenced by:  dynkin  30035
  Copyright terms: Public domain W3C validator