| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . . . . . . 9
⊢ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)} = {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)} |
| 2 | | subsaliuncl.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝑆 ∈ SAlg) |
| 3 | 1, 2 | rabexd 5340 |
. . . . . . . 8
⊢ (𝜑 → {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)} ∈ V) |
| 4 | 3 | ralrimivw 3150 |
. . . . . . 7
⊢ (𝜑 → ∀𝑛 ∈ ℕ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)} ∈ V) |
| 5 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)}) = (𝑛 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)}) |
| 6 | 5 | fnmpt 6708 |
. . . . . . 7
⊢
(∀𝑛 ∈
ℕ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)} ∈ V → (𝑛 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)}) Fn ℕ) |
| 7 | 4, 6 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑛 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)}) Fn ℕ) |
| 8 | | nnex 12272 |
. . . . . . 7
⊢ ℕ
∈ V |
| 9 | | fnrndomg 10576 |
. . . . . . 7
⊢ (ℕ
∈ V → ((𝑛 ∈
ℕ ↦ {𝑥 ∈
𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)}) Fn ℕ → ran (𝑛 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)}) ≼ ℕ)) |
| 10 | 8, 9 | ax-mp 5 |
. . . . . 6
⊢ ((𝑛 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)}) Fn ℕ → ran (𝑛 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)}) ≼ ℕ) |
| 11 | 7, 10 | syl 17 |
. . . . 5
⊢ (𝜑 → ran (𝑛 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)}) ≼ ℕ) |
| 12 | | nnenom 14021 |
. . . . . 6
⊢ ℕ
≈ ω |
| 13 | 12 | a1i 11 |
. . . . 5
⊢ (𝜑 → ℕ ≈
ω) |
| 14 | | domentr 9053 |
. . . . 5
⊢ ((ran
(𝑛 ∈ ℕ ↦
{𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)}) ≼ ℕ ∧ ℕ ≈
ω) → ran (𝑛
∈ ℕ ↦ {𝑥
∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)}) ≼ ω) |
| 15 | 11, 13, 14 | syl2anc 584 |
. . . 4
⊢ (𝜑 → ran (𝑛 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)}) ≼ ω) |
| 16 | | vex 3484 |
. . . . . . . 8
⊢ 𝑦 ∈ V |
| 17 | 5 | elrnmpt 5969 |
. . . . . . . 8
⊢ (𝑦 ∈ V → (𝑦 ∈ ran (𝑛 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)}) ↔ ∃𝑛 ∈ ℕ 𝑦 = {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)})) |
| 18 | 16, 17 | ax-mp 5 |
. . . . . . 7
⊢ (𝑦 ∈ ran (𝑛 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)}) ↔ ∃𝑛 ∈ ℕ 𝑦 = {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)}) |
| 19 | 18 | biimpi 216 |
. . . . . 6
⊢ (𝑦 ∈ ran (𝑛 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)}) → ∃𝑛 ∈ ℕ 𝑦 = {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)}) |
| 20 | 19 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)})) → ∃𝑛 ∈ ℕ 𝑦 = {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)}) |
| 21 | | simp3 1139 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑦 = {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)}) → 𝑦 = {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)}) |
| 22 | | subsaliuncl.4 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹:ℕ⟶𝑇) |
| 23 | 22 | ffvelcdmda 7104 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ 𝑇) |
| 24 | | subsaliuncl.3 |
. . . . . . . . . . . . 13
⊢ 𝑇 = (𝑆 ↾t 𝐷) |
| 25 | 23, 24 | eleqtrdi 2851 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) ∈ (𝑆 ↾t 𝐷)) |
| 26 | | subsaliuncl.2 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐷 ∈ 𝑉) |
| 27 | 26 | elexd 3504 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐷 ∈ V) |
| 28 | | elrest 17472 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈ SAlg ∧ 𝐷 ∈ V) → ((𝐹‘𝑛) ∈ (𝑆 ↾t 𝐷) ↔ ∃𝑥 ∈ 𝑆 (𝐹‘𝑛) = (𝑥 ∩ 𝐷))) |
| 29 | 2, 27, 28 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐹‘𝑛) ∈ (𝑆 ↾t 𝐷) ↔ ∃𝑥 ∈ 𝑆 (𝐹‘𝑛) = (𝑥 ∩ 𝐷))) |
| 30 | 29 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐹‘𝑛) ∈ (𝑆 ↾t 𝐷) ↔ ∃𝑥 ∈ 𝑆 (𝐹‘𝑛) = (𝑥 ∩ 𝐷))) |
| 31 | 25, 30 | mpbid 232 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ∃𝑥 ∈ 𝑆 (𝐹‘𝑛) = (𝑥 ∩ 𝐷)) |
| 32 | | rabn0 4389 |
. . . . . . . . . . 11
⊢ ({𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)} ≠ ∅ ↔ ∃𝑥 ∈ 𝑆 (𝐹‘𝑛) = (𝑥 ∩ 𝐷)) |
| 33 | 31, 32 | sylibr 234 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)} ≠ ∅) |
| 34 | 33 | 3adant3 1133 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑦 = {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)}) → {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)} ≠ ∅) |
| 35 | 21, 34 | eqnetrd 3008 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ ∧ 𝑦 = {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)}) → 𝑦 ≠ ∅) |
| 36 | 35 | 3exp 1120 |
. . . . . . 7
⊢ (𝜑 → (𝑛 ∈ ℕ → (𝑦 = {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)} → 𝑦 ≠ ∅))) |
| 37 | 36 | rexlimdv 3153 |
. . . . . 6
⊢ (𝜑 → (∃𝑛 ∈ ℕ 𝑦 = {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)} → 𝑦 ≠ ∅)) |
| 38 | 37 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)})) → (∃𝑛 ∈ ℕ 𝑦 = {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)} → 𝑦 ≠ ∅)) |
| 39 | 20, 38 | mpd 15 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ ran (𝑛 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)})) → 𝑦 ≠ ∅) |
| 40 | 15, 39 | axccdom 45227 |
. . 3
⊢ (𝜑 → ∃𝑓(𝑓 Fn ran (𝑛 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)}) ∧ ∀𝑦 ∈ ran (𝑛 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)})(𝑓‘𝑦) ∈ 𝑦)) |
| 41 | | simpl 482 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 Fn ran (𝑛 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)}) ∧ ∀𝑦 ∈ ran (𝑛 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)})(𝑓‘𝑦) ∈ 𝑦)) → 𝜑) |
| 42 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑚 → (𝐹‘𝑛) = (𝐹‘𝑚)) |
| 43 | 42 | eqeq1d 2739 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑚 → ((𝐹‘𝑛) = (𝑥 ∩ 𝐷) ↔ (𝐹‘𝑚) = (𝑥 ∩ 𝐷))) |
| 44 | 43 | rabbidv 3444 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑚 → {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)} = {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑚) = (𝑥 ∩ 𝐷)}) |
| 45 | 44 | cbvmptv 5255 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)}) = (𝑚 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑚) = (𝑥 ∩ 𝐷)}) |
| 46 | 45 | rneqi 5948 |
. . . . . . . . 9
⊢ ran
(𝑛 ∈ ℕ ↦
{𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)}) = ran (𝑚 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑚) = (𝑥 ∩ 𝐷)}) |
| 47 | 46 | fneq2i 6666 |
. . . . . . . 8
⊢ (𝑓 Fn ran (𝑛 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)}) ↔ 𝑓 Fn ran (𝑚 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑚) = (𝑥 ∩ 𝐷)})) |
| 48 | 47 | biimpi 216 |
. . . . . . 7
⊢ (𝑓 Fn ran (𝑛 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)}) → 𝑓 Fn ran (𝑚 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑚) = (𝑥 ∩ 𝐷)})) |
| 49 | 48 | ad2antrl 728 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 Fn ran (𝑛 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)}) ∧ ∀𝑦 ∈ ran (𝑛 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)})(𝑓‘𝑦) ∈ 𝑦)) → 𝑓 Fn ran (𝑚 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑚) = (𝑥 ∩ 𝐷)})) |
| 50 | 46 | raleqi 3324 |
. . . . . . . . 9
⊢
(∀𝑦 ∈
ran (𝑛 ∈ ℕ
↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)})(𝑓‘𝑦) ∈ 𝑦 ↔ ∀𝑦 ∈ ran (𝑚 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑚) = (𝑥 ∩ 𝐷)})(𝑓‘𝑦) ∈ 𝑦) |
| 51 | 50 | biimpi 216 |
. . . . . . . 8
⊢
(∀𝑦 ∈
ran (𝑛 ∈ ℕ
↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)})(𝑓‘𝑦) ∈ 𝑦 → ∀𝑦 ∈ ran (𝑚 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑚) = (𝑥 ∩ 𝐷)})(𝑓‘𝑦) ∈ 𝑦) |
| 52 | 51 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ ∀𝑦 ∈ ran (𝑛 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)})(𝑓‘𝑦) ∈ 𝑦) → ∀𝑦 ∈ ran (𝑚 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑚) = (𝑥 ∩ 𝐷)})(𝑓‘𝑦) ∈ 𝑦) |
| 53 | 52 | adantrl 716 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓 Fn ran (𝑛 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)}) ∧ ∀𝑦 ∈ ran (𝑛 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)})(𝑓‘𝑦) ∈ 𝑦)) → ∀𝑦 ∈ ran (𝑚 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑚) = (𝑥 ∩ 𝐷)})(𝑓‘𝑦) ∈ 𝑦) |
| 54 | | nfv 1914 |
. . . . . . 7
⊢
Ⅎ𝑧(𝜑 ∧ 𝑓 Fn ran (𝑚 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑚) = (𝑥 ∩ 𝐷)}) ∧ ∀𝑦 ∈ ran (𝑚 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑚) = (𝑥 ∩ 𝐷)})(𝑓‘𝑦) ∈ 𝑦) |
| 55 | 2 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 Fn ran (𝑚 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑚) = (𝑥 ∩ 𝐷)}) ∧ ∀𝑦 ∈ ran (𝑚 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑚) = (𝑥 ∩ 𝐷)})(𝑓‘𝑦) ∈ 𝑦) → 𝑆 ∈ SAlg) |
| 56 | | ineq1 4213 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (𝑥 ∩ 𝐷) = (𝑧 ∩ 𝐷)) |
| 57 | 56 | eqeq2d 2748 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → ((𝐹‘𝑚) = (𝑥 ∩ 𝐷) ↔ (𝐹‘𝑚) = (𝑧 ∩ 𝐷))) |
| 58 | 57 | cbvrabv 3447 |
. . . . . . . . . 10
⊢ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑚) = (𝑥 ∩ 𝐷)} = {𝑧 ∈ 𝑆 ∣ (𝐹‘𝑚) = (𝑧 ∩ 𝐷)} |
| 59 | 58 | mpteq2i 5247 |
. . . . . . . . 9
⊢ (𝑚 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑚) = (𝑥 ∩ 𝐷)}) = (𝑚 ∈ ℕ ↦ {𝑧 ∈ 𝑆 ∣ (𝐹‘𝑚) = (𝑧 ∩ 𝐷)}) |
| 60 | 45, 59 | eqtr2i 2766 |
. . . . . . . 8
⊢ (𝑚 ∈ ℕ ↦ {𝑧 ∈ 𝑆 ∣ (𝐹‘𝑚) = (𝑧 ∩ 𝐷)}) = (𝑛 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)}) |
| 61 | 60 | coeq2i 5871 |
. . . . . . 7
⊢ (𝑓 ∘ (𝑚 ∈ ℕ ↦ {𝑧 ∈ 𝑆 ∣ (𝐹‘𝑚) = (𝑧 ∩ 𝐷)})) = (𝑓 ∘ (𝑛 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)})) |
| 62 | 47 | biimpri 228 |
. . . . . . . 8
⊢ (𝑓 Fn ran (𝑚 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑚) = (𝑥 ∩ 𝐷)}) → 𝑓 Fn ran (𝑛 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)})) |
| 63 | 62 | 3ad2ant2 1135 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 Fn ran (𝑚 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑚) = (𝑥 ∩ 𝐷)}) ∧ ∀𝑦 ∈ ran (𝑚 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑚) = (𝑥 ∩ 𝐷)})(𝑓‘𝑦) ∈ 𝑦) → 𝑓 Fn ran (𝑛 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)})) |
| 64 | 46 | eqcomi 2746 |
. . . . . . . . . . 11
⊢ ran
(𝑚 ∈ ℕ ↦
{𝑥 ∈ 𝑆 ∣ (𝐹‘𝑚) = (𝑥 ∩ 𝐷)}) = ran (𝑛 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)}) |
| 65 | 64 | raleqi 3324 |
. . . . . . . . . 10
⊢
(∀𝑦 ∈
ran (𝑚 ∈ ℕ
↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑚) = (𝑥 ∩ 𝐷)})(𝑓‘𝑦) ∈ 𝑦 ↔ ∀𝑦 ∈ ran (𝑛 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)})(𝑓‘𝑦) ∈ 𝑦) |
| 66 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑧 → (𝑓‘𝑦) = (𝑓‘𝑧)) |
| 67 | | id 22 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑧 → 𝑦 = 𝑧) |
| 68 | 66, 67 | eleq12d 2835 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑧 → ((𝑓‘𝑦) ∈ 𝑦 ↔ (𝑓‘𝑧) ∈ 𝑧)) |
| 69 | 68 | cbvralvw 3237 |
. . . . . . . . . 10
⊢
(∀𝑦 ∈
ran (𝑛 ∈ ℕ
↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)})(𝑓‘𝑦) ∈ 𝑦 ↔ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)})(𝑓‘𝑧) ∈ 𝑧) |
| 70 | 65, 69 | bitri 275 |
. . . . . . . . 9
⊢
(∀𝑦 ∈
ran (𝑚 ∈ ℕ
↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑚) = (𝑥 ∩ 𝐷)})(𝑓‘𝑦) ∈ 𝑦 ↔ ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)})(𝑓‘𝑧) ∈ 𝑧) |
| 71 | 70 | biimpi 216 |
. . . . . . . 8
⊢
(∀𝑦 ∈
ran (𝑚 ∈ ℕ
↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑚) = (𝑥 ∩ 𝐷)})(𝑓‘𝑦) ∈ 𝑦 → ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)})(𝑓‘𝑧) ∈ 𝑧) |
| 72 | 71 | 3ad2ant3 1136 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑓 Fn ran (𝑚 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑚) = (𝑥 ∩ 𝐷)}) ∧ ∀𝑦 ∈ ran (𝑚 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑚) = (𝑥 ∩ 𝐷)})(𝑓‘𝑦) ∈ 𝑦) → ∀𝑧 ∈ ran (𝑛 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)})(𝑓‘𝑧) ∈ 𝑧) |
| 73 | 54, 55, 5, 61, 63, 72 | subsaliuncllem 46372 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 Fn ran (𝑚 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑚) = (𝑥 ∩ 𝐷)}) ∧ ∀𝑦 ∈ ran (𝑚 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑚) = (𝑥 ∩ 𝐷)})(𝑓‘𝑦) ∈ 𝑦) → ∃𝑒 ∈ (𝑆 ↑m ℕ)∀𝑛 ∈ ℕ (𝐹‘𝑛) = ((𝑒‘𝑛) ∩ 𝐷)) |
| 74 | 41, 49, 53, 73 | syl3anc 1373 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓 Fn ran (𝑛 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)}) ∧ ∀𝑦 ∈ ran (𝑛 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)})(𝑓‘𝑦) ∈ 𝑦)) → ∃𝑒 ∈ (𝑆 ↑m ℕ)∀𝑛 ∈ ℕ (𝐹‘𝑛) = ((𝑒‘𝑛) ∩ 𝐷)) |
| 75 | 74 | ex 412 |
. . . 4
⊢ (𝜑 → ((𝑓 Fn ran (𝑛 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)}) ∧ ∀𝑦 ∈ ran (𝑛 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)})(𝑓‘𝑦) ∈ 𝑦) → ∃𝑒 ∈ (𝑆 ↑m ℕ)∀𝑛 ∈ ℕ (𝐹‘𝑛) = ((𝑒‘𝑛) ∩ 𝐷))) |
| 76 | 75 | exlimdv 1933 |
. . 3
⊢ (𝜑 → (∃𝑓(𝑓 Fn ran (𝑛 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)}) ∧ ∀𝑦 ∈ ran (𝑛 ∈ ℕ ↦ {𝑥 ∈ 𝑆 ∣ (𝐹‘𝑛) = (𝑥 ∩ 𝐷)})(𝑓‘𝑦) ∈ 𝑦) → ∃𝑒 ∈ (𝑆 ↑m ℕ)∀𝑛 ∈ ℕ (𝐹‘𝑛) = ((𝑒‘𝑛) ∩ 𝐷))) |
| 77 | 40, 76 | mpd 15 |
. 2
⊢ (𝜑 → ∃𝑒 ∈ (𝑆 ↑m ℕ)∀𝑛 ∈ ℕ (𝐹‘𝑛) = ((𝑒‘𝑛) ∩ 𝐷)) |
| 78 | 2 | 3ad2ant1 1134 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ∈ (𝑆 ↑m ℕ) ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) = ((𝑒‘𝑛) ∩ 𝐷)) → 𝑆 ∈ SAlg) |
| 79 | 27 | 3ad2ant1 1134 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ∈ (𝑆 ↑m ℕ) ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) = ((𝑒‘𝑛) ∩ 𝐷)) → 𝐷 ∈ V) |
| 80 | 2 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑒 ∈ (𝑆 ↑m ℕ)) → 𝑆 ∈ SAlg) |
| 81 | | nnct 14022 |
. . . . . . . . 9
⊢ ℕ
≼ ω |
| 82 | 81 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑒 ∈ (𝑆 ↑m ℕ)) → ℕ
≼ ω) |
| 83 | | elmapi 8889 |
. . . . . . . . . 10
⊢ (𝑒 ∈ (𝑆 ↑m ℕ) → 𝑒:ℕ⟶𝑆) |
| 84 | 83 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑒 ∈ (𝑆 ↑m ℕ)) → 𝑒:ℕ⟶𝑆) |
| 85 | 84 | ffvelcdmda 7104 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑒 ∈ (𝑆 ↑m ℕ)) ∧ 𝑛 ∈ ℕ) → (𝑒‘𝑛) ∈ 𝑆) |
| 86 | 80, 82, 85 | saliuncl 46338 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑒 ∈ (𝑆 ↑m ℕ)) →
∪ 𝑛 ∈ ℕ (𝑒‘𝑛) ∈ 𝑆) |
| 87 | 86 | 3adant3 1133 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ∈ (𝑆 ↑m ℕ) ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) = ((𝑒‘𝑛) ∩ 𝐷)) → ∪ 𝑛 ∈ ℕ (𝑒‘𝑛) ∈ 𝑆) |
| 88 | | eqid 2737 |
. . . . . 6
⊢ (∪ 𝑛 ∈ ℕ (𝑒‘𝑛) ∩ 𝐷) = (∪
𝑛 ∈ ℕ (𝑒‘𝑛) ∩ 𝐷) |
| 89 | 78, 79, 87, 88 | elrestd 45113 |
. . . . 5
⊢ ((𝜑 ∧ 𝑒 ∈ (𝑆 ↑m ℕ) ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) = ((𝑒‘𝑛) ∩ 𝐷)) → (∪ 𝑛 ∈ ℕ (𝑒‘𝑛) ∩ 𝐷) ∈ (𝑆 ↾t 𝐷)) |
| 90 | | nfra1 3284 |
. . . . . . . . 9
⊢
Ⅎ𝑛∀𝑛 ∈ ℕ (𝐹‘𝑛) = ((𝑒‘𝑛) ∩ 𝐷) |
| 91 | | rspa 3248 |
. . . . . . . . 9
⊢
((∀𝑛 ∈
ℕ (𝐹‘𝑛) = ((𝑒‘𝑛) ∩ 𝐷) ∧ 𝑛 ∈ ℕ) → (𝐹‘𝑛) = ((𝑒‘𝑛) ∩ 𝐷)) |
| 92 | 90, 91 | iuneq2df 45052 |
. . . . . . . 8
⊢
(∀𝑛 ∈
ℕ (𝐹‘𝑛) = ((𝑒‘𝑛) ∩ 𝐷) → ∪
𝑛 ∈ ℕ (𝐹‘𝑛) = ∪ 𝑛 ∈ ℕ ((𝑒‘𝑛) ∩ 𝐷)) |
| 93 | | iunin1 5072 |
. . . . . . . . 9
⊢ ∪ 𝑛 ∈ ℕ ((𝑒‘𝑛) ∩ 𝐷) = (∪
𝑛 ∈ ℕ (𝑒‘𝑛) ∩ 𝐷) |
| 94 | 93 | a1i 11 |
. . . . . . . 8
⊢
(∀𝑛 ∈
ℕ (𝐹‘𝑛) = ((𝑒‘𝑛) ∩ 𝐷) → ∪
𝑛 ∈ ℕ ((𝑒‘𝑛) ∩ 𝐷) = (∪
𝑛 ∈ ℕ (𝑒‘𝑛) ∩ 𝐷)) |
| 95 | 92, 94 | eqtrd 2777 |
. . . . . . 7
⊢
(∀𝑛 ∈
ℕ (𝐹‘𝑛) = ((𝑒‘𝑛) ∩ 𝐷) → ∪
𝑛 ∈ ℕ (𝐹‘𝑛) = (∪
𝑛 ∈ ℕ (𝑒‘𝑛) ∩ 𝐷)) |
| 96 | 95 | 3ad2ant3 1136 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ∈ (𝑆 ↑m ℕ) ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) = ((𝑒‘𝑛) ∩ 𝐷)) → ∪ 𝑛 ∈ ℕ (𝐹‘𝑛) = (∪
𝑛 ∈ ℕ (𝑒‘𝑛) ∩ 𝐷)) |
| 97 | 24 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑒 ∈ (𝑆 ↑m ℕ) ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) = ((𝑒‘𝑛) ∩ 𝐷)) → 𝑇 = (𝑆 ↾t 𝐷)) |
| 98 | 96, 97 | eleq12d 2835 |
. . . . 5
⊢ ((𝜑 ∧ 𝑒 ∈ (𝑆 ↑m ℕ) ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) = ((𝑒‘𝑛) ∩ 𝐷)) → (∪ 𝑛 ∈ ℕ (𝐹‘𝑛) ∈ 𝑇 ↔ (∪
𝑛 ∈ ℕ (𝑒‘𝑛) ∩ 𝐷) ∈ (𝑆 ↾t 𝐷))) |
| 99 | 89, 98 | mpbird 257 |
. . . 4
⊢ ((𝜑 ∧ 𝑒 ∈ (𝑆 ↑m ℕ) ∧
∀𝑛 ∈ ℕ
(𝐹‘𝑛) = ((𝑒‘𝑛) ∩ 𝐷)) → ∪ 𝑛 ∈ ℕ (𝐹‘𝑛) ∈ 𝑇) |
| 100 | 99 | 3exp 1120 |
. . 3
⊢ (𝜑 → (𝑒 ∈ (𝑆 ↑m ℕ) →
(∀𝑛 ∈ ℕ
(𝐹‘𝑛) = ((𝑒‘𝑛) ∩ 𝐷) → ∪
𝑛 ∈ ℕ (𝐹‘𝑛) ∈ 𝑇))) |
| 101 | 100 | rexlimdv 3153 |
. 2
⊢ (𝜑 → (∃𝑒 ∈ (𝑆 ↑m ℕ)∀𝑛 ∈ ℕ (𝐹‘𝑛) = ((𝑒‘𝑛) ∩ 𝐷) → ∪
𝑛 ∈ ℕ (𝐹‘𝑛) ∈ 𝑇)) |
| 102 | 77, 101 | mpd 15 |
1
⊢ (𝜑 → ∪ 𝑛 ∈ ℕ (𝐹‘𝑛) ∈ 𝑇) |