Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  subsaliuncl Structured version   Visualization version   GIF version

Theorem subsaliuncl 41079
Description: A subspace sigma-algebra is closed under countable union. This is Lemma 121A (iii) of [Fremlin1] p. 35. (Contributed by Glauco Siliprandi, 26-Jun-2021.)
Hypotheses
Ref Expression
subsaliuncl.1 (𝜑𝑆 ∈ SAlg)
subsaliuncl.2 (𝜑𝐷𝑉)
subsaliuncl.3 𝑇 = (𝑆t 𝐷)
subsaliuncl.4 (𝜑𝐹:ℕ⟶𝑇)
Assertion
Ref Expression
subsaliuncl (𝜑 𝑛 ∈ ℕ (𝐹𝑛) ∈ 𝑇)
Distinct variable groups:   𝐷,𝑛   𝑛,𝐹   𝑆,𝑛   𝜑,𝑛
Allowed substitution hints:   𝑇(𝑛)   𝑉(𝑛)

Proof of Theorem subsaliuncl
Dummy variables 𝑒 𝑓 𝑧 𝑚 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2760 . . . . . . . . 9 {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)} = {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)}
2 subsaliuncl.1 . . . . . . . . 9 (𝜑𝑆 ∈ SAlg)
31, 2rabexd 4965 . . . . . . . 8 (𝜑 → {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)} ∈ V)
43ralrimivw 3105 . . . . . . 7 (𝜑 → ∀𝑛 ∈ ℕ {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)} ∈ V)
5 eqid 2760 . . . . . . . 8 (𝑛 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)}) = (𝑛 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)})
65fnmpt 6181 . . . . . . 7 (∀𝑛 ∈ ℕ {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)} ∈ V → (𝑛 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)}) Fn ℕ)
74, 6syl 17 . . . . . 6 (𝜑 → (𝑛 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)}) Fn ℕ)
8 nnex 11218 . . . . . . 7 ℕ ∈ V
9 fnrndomg 9550 . . . . . . 7 (ℕ ∈ V → ((𝑛 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)}) Fn ℕ → ran (𝑛 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)}) ≼ ℕ))
108, 9ax-mp 5 . . . . . 6 ((𝑛 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)}) Fn ℕ → ran (𝑛 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)}) ≼ ℕ)
117, 10syl 17 . . . . 5 (𝜑 → ran (𝑛 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)}) ≼ ℕ)
12 nnenom 12973 . . . . . 6 ℕ ≈ ω
1312a1i 11 . . . . 5 (𝜑 → ℕ ≈ ω)
14 domentr 8180 . . . . 5 ((ran (𝑛 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)}) ≼ ℕ ∧ ℕ ≈ ω) → ran (𝑛 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)}) ≼ ω)
1511, 13, 14syl2anc 696 . . . 4 (𝜑 → ran (𝑛 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)}) ≼ ω)
16 vex 3343 . . . . . . . 8 𝑦 ∈ V
175elrnmpt 5527 . . . . . . . 8 (𝑦 ∈ V → (𝑦 ∈ ran (𝑛 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)}) ↔ ∃𝑛 ∈ ℕ 𝑦 = {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)}))
1816, 17ax-mp 5 . . . . . . 7 (𝑦 ∈ ran (𝑛 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)}) ↔ ∃𝑛 ∈ ℕ 𝑦 = {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)})
1918biimpi 206 . . . . . 6 (𝑦 ∈ ran (𝑛 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)}) → ∃𝑛 ∈ ℕ 𝑦 = {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)})
2019adantl 473 . . . . 5 ((𝜑𝑦 ∈ ran (𝑛 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)})) → ∃𝑛 ∈ ℕ 𝑦 = {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)})
21 simp3 1133 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ ∧ 𝑦 = {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)}) → 𝑦 = {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)})
22 subsaliuncl.4 . . . . . . . . . . . . . 14 (𝜑𝐹:ℕ⟶𝑇)
2322ffvelrnda 6522 . . . . . . . . . . . . 13 ((𝜑𝑛 ∈ ℕ) → (𝐹𝑛) ∈ 𝑇)
24 subsaliuncl.3 . . . . . . . . . . . . 13 𝑇 = (𝑆t 𝐷)
2523, 24syl6eleq 2849 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → (𝐹𝑛) ∈ (𝑆t 𝐷))
26 subsaliuncl.2 . . . . . . . . . . . . . . 15 (𝜑𝐷𝑉)
2726elexd 3354 . . . . . . . . . . . . . 14 (𝜑𝐷 ∈ V)
28 elrest 16290 . . . . . . . . . . . . . 14 ((𝑆 ∈ SAlg ∧ 𝐷 ∈ V) → ((𝐹𝑛) ∈ (𝑆t 𝐷) ↔ ∃𝑥𝑆 (𝐹𝑛) = (𝑥𝐷)))
292, 27, 28syl2anc 696 . . . . . . . . . . . . 13 (𝜑 → ((𝐹𝑛) ∈ (𝑆t 𝐷) ↔ ∃𝑥𝑆 (𝐹𝑛) = (𝑥𝐷)))
3029adantr 472 . . . . . . . . . . . 12 ((𝜑𝑛 ∈ ℕ) → ((𝐹𝑛) ∈ (𝑆t 𝐷) ↔ ∃𝑥𝑆 (𝐹𝑛) = (𝑥𝐷)))
3125, 30mpbid 222 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ℕ) → ∃𝑥𝑆 (𝐹𝑛) = (𝑥𝐷))
32 rabn0 4101 . . . . . . . . . . 11 ({𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)} ≠ ∅ ↔ ∃𝑥𝑆 (𝐹𝑛) = (𝑥𝐷))
3331, 32sylibr 224 . . . . . . . . . 10 ((𝜑𝑛 ∈ ℕ) → {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)} ≠ ∅)
34333adant3 1127 . . . . . . . . 9 ((𝜑𝑛 ∈ ℕ ∧ 𝑦 = {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)}) → {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)} ≠ ∅)
3521, 34eqnetrd 2999 . . . . . . . 8 ((𝜑𝑛 ∈ ℕ ∧ 𝑦 = {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)}) → 𝑦 ≠ ∅)
36353exp 1113 . . . . . . 7 (𝜑 → (𝑛 ∈ ℕ → (𝑦 = {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)} → 𝑦 ≠ ∅)))
3736rexlimdv 3168 . . . . . 6 (𝜑 → (∃𝑛 ∈ ℕ 𝑦 = {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)} → 𝑦 ≠ ∅))
3837adantr 472 . . . . 5 ((𝜑𝑦 ∈ ran (𝑛 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)})) → (∃𝑛 ∈ ℕ 𝑦 = {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)} → 𝑦 ≠ ∅))
3920, 38mpd 15 . . . 4 ((𝜑𝑦 ∈ ran (𝑛 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)})) → 𝑦 ≠ ∅)
4015, 39axccdom 39915 . . 3 (𝜑 → ∃𝑓(𝑓 Fn ran (𝑛 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)}) ∧ ∀𝑦 ∈ ran (𝑛 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)})(𝑓𝑦) ∈ 𝑦))
41 simpl 474 . . . . . 6 ((𝜑 ∧ (𝑓 Fn ran (𝑛 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)}) ∧ ∀𝑦 ∈ ran (𝑛 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)})(𝑓𝑦) ∈ 𝑦)) → 𝜑)
42 fveq2 6352 . . . . . . . . . . . . 13 (𝑛 = 𝑚 → (𝐹𝑛) = (𝐹𝑚))
4342eqeq1d 2762 . . . . . . . . . . . 12 (𝑛 = 𝑚 → ((𝐹𝑛) = (𝑥𝐷) ↔ (𝐹𝑚) = (𝑥𝐷)))
4443rabbidv 3329 . . . . . . . . . . 11 (𝑛 = 𝑚 → {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)} = {𝑥𝑆 ∣ (𝐹𝑚) = (𝑥𝐷)})
4544cbvmptv 4902 . . . . . . . . . 10 (𝑛 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)}) = (𝑚 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑚) = (𝑥𝐷)})
4645rneqi 5507 . . . . . . . . 9 ran (𝑛 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)}) = ran (𝑚 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑚) = (𝑥𝐷)})
4746fneq2i 6147 . . . . . . . 8 (𝑓 Fn ran (𝑛 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)}) ↔ 𝑓 Fn ran (𝑚 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑚) = (𝑥𝐷)}))
4847biimpi 206 . . . . . . 7 (𝑓 Fn ran (𝑛 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)}) → 𝑓 Fn ran (𝑚 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑚) = (𝑥𝐷)}))
4948ad2antrl 766 . . . . . 6 ((𝜑 ∧ (𝑓 Fn ran (𝑛 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)}) ∧ ∀𝑦 ∈ ran (𝑛 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)})(𝑓𝑦) ∈ 𝑦)) → 𝑓 Fn ran (𝑚 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑚) = (𝑥𝐷)}))
5046raleqi 3281 . . . . . . . . 9 (∀𝑦 ∈ ran (𝑛 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)})(𝑓𝑦) ∈ 𝑦 ↔ ∀𝑦 ∈ ran (𝑚 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑚) = (𝑥𝐷)})(𝑓𝑦) ∈ 𝑦)
5150biimpi 206 . . . . . . . 8 (∀𝑦 ∈ ran (𝑛 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)})(𝑓𝑦) ∈ 𝑦 → ∀𝑦 ∈ ran (𝑚 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑚) = (𝑥𝐷)})(𝑓𝑦) ∈ 𝑦)
5251adantl 473 . . . . . . 7 ((𝜑 ∧ ∀𝑦 ∈ ran (𝑛 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)})(𝑓𝑦) ∈ 𝑦) → ∀𝑦 ∈ ran (𝑚 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑚) = (𝑥𝐷)})(𝑓𝑦) ∈ 𝑦)
5352adantrl 754 . . . . . 6 ((𝜑 ∧ (𝑓 Fn ran (𝑛 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)}) ∧ ∀𝑦 ∈ ran (𝑛 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)})(𝑓𝑦) ∈ 𝑦)) → ∀𝑦 ∈ ran (𝑚 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑚) = (𝑥𝐷)})(𝑓𝑦) ∈ 𝑦)
54 nfv 1992 . . . . . . 7 𝑧(𝜑𝑓 Fn ran (𝑚 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑚) = (𝑥𝐷)}) ∧ ∀𝑦 ∈ ran (𝑚 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑚) = (𝑥𝐷)})(𝑓𝑦) ∈ 𝑦)
5523ad2ant1 1128 . . . . . . 7 ((𝜑𝑓 Fn ran (𝑚 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑚) = (𝑥𝐷)}) ∧ ∀𝑦 ∈ ran (𝑚 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑚) = (𝑥𝐷)})(𝑓𝑦) ∈ 𝑦) → 𝑆 ∈ SAlg)
56 ineq1 3950 . . . . . . . . . . . 12 (𝑥 = 𝑧 → (𝑥𝐷) = (𝑧𝐷))
5756eqeq2d 2770 . . . . . . . . . . 11 (𝑥 = 𝑧 → ((𝐹𝑚) = (𝑥𝐷) ↔ (𝐹𝑚) = (𝑧𝐷)))
5857cbvrabv 3339 . . . . . . . . . 10 {𝑥𝑆 ∣ (𝐹𝑚) = (𝑥𝐷)} = {𝑧𝑆 ∣ (𝐹𝑚) = (𝑧𝐷)}
5958mpteq2i 4893 . . . . . . . . 9 (𝑚 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑚) = (𝑥𝐷)}) = (𝑚 ∈ ℕ ↦ {𝑧𝑆 ∣ (𝐹𝑚) = (𝑧𝐷)})
6045, 59eqtr2i 2783 . . . . . . . 8 (𝑚 ∈ ℕ ↦ {𝑧𝑆 ∣ (𝐹𝑚) = (𝑧𝐷)}) = (𝑛 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)})
6160coeq2i 5438 . . . . . . 7 (𝑓 ∘ (𝑚 ∈ ℕ ↦ {𝑧𝑆 ∣ (𝐹𝑚) = (𝑧𝐷)})) = (𝑓 ∘ (𝑛 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)}))
6247biimpri 218 . . . . . . . 8 (𝑓 Fn ran (𝑚 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑚) = (𝑥𝐷)}) → 𝑓 Fn ran (𝑛 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)}))
63623ad2ant2 1129 . . . . . . 7 ((𝜑𝑓 Fn ran (𝑚 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑚) = (𝑥𝐷)}) ∧ ∀𝑦 ∈ ran (𝑚 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑚) = (𝑥𝐷)})(𝑓𝑦) ∈ 𝑦) → 𝑓 Fn ran (𝑛 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)}))
6446eqcomi 2769 . . . . . . . . . . 11 ran (𝑚 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑚) = (𝑥𝐷)}) = ran (𝑛 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)})
6564raleqi 3281 . . . . . . . . . 10 (∀𝑦 ∈ ran (𝑚 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑚) = (𝑥𝐷)})(𝑓𝑦) ∈ 𝑦 ↔ ∀𝑦 ∈ ran (𝑛 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)})(𝑓𝑦) ∈ 𝑦)
66 fveq2 6352 . . . . . . . . . . . 12 (𝑦 = 𝑧 → (𝑓𝑦) = (𝑓𝑧))
67 id 22 . . . . . . . . . . . 12 (𝑦 = 𝑧𝑦 = 𝑧)
6866, 67eleq12d 2833 . . . . . . . . . . 11 (𝑦 = 𝑧 → ((𝑓𝑦) ∈ 𝑦 ↔ (𝑓𝑧) ∈ 𝑧))
6968cbvralv 3310 . . . . . . . . . 10 (∀𝑦 ∈ ran (𝑛 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)})(𝑓𝑦) ∈ 𝑦 ↔ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)})(𝑓𝑧) ∈ 𝑧)
7065, 69bitri 264 . . . . . . . . 9 (∀𝑦 ∈ ran (𝑚 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑚) = (𝑥𝐷)})(𝑓𝑦) ∈ 𝑦 ↔ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)})(𝑓𝑧) ∈ 𝑧)
7170biimpi 206 . . . . . . . 8 (∀𝑦 ∈ ran (𝑚 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑚) = (𝑥𝐷)})(𝑓𝑦) ∈ 𝑦 → ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)})(𝑓𝑧) ∈ 𝑧)
72713ad2ant3 1130 . . . . . . 7 ((𝜑𝑓 Fn ran (𝑚 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑚) = (𝑥𝐷)}) ∧ ∀𝑦 ∈ ran (𝑚 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑚) = (𝑥𝐷)})(𝑓𝑦) ∈ 𝑦) → ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)})(𝑓𝑧) ∈ 𝑧)
7354, 55, 5, 61, 63, 72subsaliuncllem 41078 . . . . . 6 ((𝜑𝑓 Fn ran (𝑚 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑚) = (𝑥𝐷)}) ∧ ∀𝑦 ∈ ran (𝑚 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑚) = (𝑥𝐷)})(𝑓𝑦) ∈ 𝑦) → ∃𝑒 ∈ (𝑆𝑚 ℕ)∀𝑛 ∈ ℕ (𝐹𝑛) = ((𝑒𝑛) ∩ 𝐷))
7441, 49, 53, 73syl3anc 1477 . . . . 5 ((𝜑 ∧ (𝑓 Fn ran (𝑛 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)}) ∧ ∀𝑦 ∈ ran (𝑛 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)})(𝑓𝑦) ∈ 𝑦)) → ∃𝑒 ∈ (𝑆𝑚 ℕ)∀𝑛 ∈ ℕ (𝐹𝑛) = ((𝑒𝑛) ∩ 𝐷))
7574ex 449 . . . 4 (𝜑 → ((𝑓 Fn ran (𝑛 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)}) ∧ ∀𝑦 ∈ ran (𝑛 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)})(𝑓𝑦) ∈ 𝑦) → ∃𝑒 ∈ (𝑆𝑚 ℕ)∀𝑛 ∈ ℕ (𝐹𝑛) = ((𝑒𝑛) ∩ 𝐷)))
7675exlimdv 2010 . . 3 (𝜑 → (∃𝑓(𝑓 Fn ran (𝑛 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)}) ∧ ∀𝑦 ∈ ran (𝑛 ∈ ℕ ↦ {𝑥𝑆 ∣ (𝐹𝑛) = (𝑥𝐷)})(𝑓𝑦) ∈ 𝑦) → ∃𝑒 ∈ (𝑆𝑚 ℕ)∀𝑛 ∈ ℕ (𝐹𝑛) = ((𝑒𝑛) ∩ 𝐷)))
7740, 76mpd 15 . 2 (𝜑 → ∃𝑒 ∈ (𝑆𝑚 ℕ)∀𝑛 ∈ ℕ (𝐹𝑛) = ((𝑒𝑛) ∩ 𝐷))
7823ad2ant1 1128 . . . . . 6 ((𝜑𝑒 ∈ (𝑆𝑚 ℕ) ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) = ((𝑒𝑛) ∩ 𝐷)) → 𝑆 ∈ SAlg)
79273ad2ant1 1128 . . . . . 6 ((𝜑𝑒 ∈ (𝑆𝑚 ℕ) ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) = ((𝑒𝑛) ∩ 𝐷)) → 𝐷 ∈ V)
802adantr 472 . . . . . . . 8 ((𝜑𝑒 ∈ (𝑆𝑚 ℕ)) → 𝑆 ∈ SAlg)
81 nnct 12974 . . . . . . . . 9 ℕ ≼ ω
8281a1i 11 . . . . . . . 8 ((𝜑𝑒 ∈ (𝑆𝑚 ℕ)) → ℕ ≼ ω)
83 elmapi 8045 . . . . . . . . . 10 (𝑒 ∈ (𝑆𝑚 ℕ) → 𝑒:ℕ⟶𝑆)
8483adantl 473 . . . . . . . . 9 ((𝜑𝑒 ∈ (𝑆𝑚 ℕ)) → 𝑒:ℕ⟶𝑆)
8584ffvelrnda 6522 . . . . . . . 8 (((𝜑𝑒 ∈ (𝑆𝑚 ℕ)) ∧ 𝑛 ∈ ℕ) → (𝑒𝑛) ∈ 𝑆)
8680, 82, 85saliuncl 41045 . . . . . . 7 ((𝜑𝑒 ∈ (𝑆𝑚 ℕ)) → 𝑛 ∈ ℕ (𝑒𝑛) ∈ 𝑆)
87863adant3 1127 . . . . . 6 ((𝜑𝑒 ∈ (𝑆𝑚 ℕ) ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) = ((𝑒𝑛) ∩ 𝐷)) → 𝑛 ∈ ℕ (𝑒𝑛) ∈ 𝑆)
88 eqid 2760 . . . . . 6 ( 𝑛 ∈ ℕ (𝑒𝑛) ∩ 𝐷) = ( 𝑛 ∈ ℕ (𝑒𝑛) ∩ 𝐷)
8978, 79, 87, 88elrestd 39790 . . . . 5 ((𝜑𝑒 ∈ (𝑆𝑚 ℕ) ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) = ((𝑒𝑛) ∩ 𝐷)) → ( 𝑛 ∈ ℕ (𝑒𝑛) ∩ 𝐷) ∈ (𝑆t 𝐷))
90 nfra1 3079 . . . . . . . . 9 𝑛𝑛 ∈ ℕ (𝐹𝑛) = ((𝑒𝑛) ∩ 𝐷)
91 rspa 3068 . . . . . . . . 9 ((∀𝑛 ∈ ℕ (𝐹𝑛) = ((𝑒𝑛) ∩ 𝐷) ∧ 𝑛 ∈ ℕ) → (𝐹𝑛) = ((𝑒𝑛) ∩ 𝐷))
9290, 91iuneq2df 39711 . . . . . . . 8 (∀𝑛 ∈ ℕ (𝐹𝑛) = ((𝑒𝑛) ∩ 𝐷) → 𝑛 ∈ ℕ (𝐹𝑛) = 𝑛 ∈ ℕ ((𝑒𝑛) ∩ 𝐷))
93 iunin1 4737 . . . . . . . . 9 𝑛 ∈ ℕ ((𝑒𝑛) ∩ 𝐷) = ( 𝑛 ∈ ℕ (𝑒𝑛) ∩ 𝐷)
9493a1i 11 . . . . . . . 8 (∀𝑛 ∈ ℕ (𝐹𝑛) = ((𝑒𝑛) ∩ 𝐷) → 𝑛 ∈ ℕ ((𝑒𝑛) ∩ 𝐷) = ( 𝑛 ∈ ℕ (𝑒𝑛) ∩ 𝐷))
9592, 94eqtrd 2794 . . . . . . 7 (∀𝑛 ∈ ℕ (𝐹𝑛) = ((𝑒𝑛) ∩ 𝐷) → 𝑛 ∈ ℕ (𝐹𝑛) = ( 𝑛 ∈ ℕ (𝑒𝑛) ∩ 𝐷))
96953ad2ant3 1130 . . . . . 6 ((𝜑𝑒 ∈ (𝑆𝑚 ℕ) ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) = ((𝑒𝑛) ∩ 𝐷)) → 𝑛 ∈ ℕ (𝐹𝑛) = ( 𝑛 ∈ ℕ (𝑒𝑛) ∩ 𝐷))
9724a1i 11 . . . . . 6 ((𝜑𝑒 ∈ (𝑆𝑚 ℕ) ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) = ((𝑒𝑛) ∩ 𝐷)) → 𝑇 = (𝑆t 𝐷))
9896, 97eleq12d 2833 . . . . 5 ((𝜑𝑒 ∈ (𝑆𝑚 ℕ) ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) = ((𝑒𝑛) ∩ 𝐷)) → ( 𝑛 ∈ ℕ (𝐹𝑛) ∈ 𝑇 ↔ ( 𝑛 ∈ ℕ (𝑒𝑛) ∩ 𝐷) ∈ (𝑆t 𝐷)))
9989, 98mpbird 247 . . . 4 ((𝜑𝑒 ∈ (𝑆𝑚 ℕ) ∧ ∀𝑛 ∈ ℕ (𝐹𝑛) = ((𝑒𝑛) ∩ 𝐷)) → 𝑛 ∈ ℕ (𝐹𝑛) ∈ 𝑇)
100993exp 1113 . . 3 (𝜑 → (𝑒 ∈ (𝑆𝑚 ℕ) → (∀𝑛 ∈ ℕ (𝐹𝑛) = ((𝑒𝑛) ∩ 𝐷) → 𝑛 ∈ ℕ (𝐹𝑛) ∈ 𝑇)))
101100rexlimdv 3168 . 2 (𝜑 → (∃𝑒 ∈ (𝑆𝑚 ℕ)∀𝑛 ∈ ℕ (𝐹𝑛) = ((𝑒𝑛) ∩ 𝐷) → 𝑛 ∈ ℕ (𝐹𝑛) ∈ 𝑇))
10277, 101mpd 15 1 (𝜑 𝑛 ∈ ℕ (𝐹𝑛) ∈ 𝑇)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1072   = wceq 1632  wex 1853  wcel 2139  wne 2932  wral 3050  wrex 3051  {crab 3054  Vcvv 3340  cin 3714  c0 4058   ciun 4672   class class class wbr 4804  cmpt 4881  ran crn 5267  ccom 5270   Fn wfn 6044  wf 6045  cfv 6049  (class class class)co 6813  ωcom 7230  𝑚 cmap 8023  cen 8118  cdom 8119  cn 11212  t crest 16283  SAlgcsalg 41031
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-inf2 8711  ax-cc 9449  ax-ac2 9477  ax-cnex 10184  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-mulcom 10192  ax-addass 10193  ax-mulass 10194  ax-distr 10195  ax-i2m1 10196  ax-1ne0 10197  ax-1rid 10198  ax-rnegex 10199  ax-rrecex 10200  ax-cnre 10201  ax-pre-lttri 10202  ax-pre-lttrn 10203  ax-pre-ltadd 10204  ax-pre-mulgt0 10205
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-se 5226  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-isom 6058  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-om 7231  df-1st 7333  df-2nd 7334  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-1o 7729  df-oadd 7733  df-er 7911  df-map 8025  df-en 8122  df-dom 8123  df-sdom 8124  df-fin 8125  df-card 8955  df-acn 8958  df-ac 9129  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-sub 10460  df-neg 10461  df-nn 11213  df-n0 11485  df-z 11570  df-uz 11880  df-rest 16285  df-salg 41032
This theorem is referenced by:  subsalsal  41080
  Copyright terms: Public domain W3C validator