Proof of Theorem isfin3ds
Step | Hyp | Ref
| Expression |
1 | | suceq 6283 |
. . . . . . . . 9
⊢ (𝑏 = 𝑥 → suc 𝑏 = suc 𝑥) |
2 | 1 | fveq2d 6726 |
. . . . . . . 8
⊢ (𝑏 = 𝑥 → (𝑎‘suc 𝑏) = (𝑎‘suc 𝑥)) |
3 | | fveq2 6722 |
. . . . . . . 8
⊢ (𝑏 = 𝑥 → (𝑎‘𝑏) = (𝑎‘𝑥)) |
4 | 2, 3 | sseq12d 3939 |
. . . . . . 7
⊢ (𝑏 = 𝑥 → ((𝑎‘suc 𝑏) ⊆ (𝑎‘𝑏) ↔ (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥))) |
5 | 4 | cbvralvw 3363 |
. . . . . 6
⊢
(∀𝑏 ∈
ω (𝑎‘suc 𝑏) ⊆ (𝑎‘𝑏) ↔ ∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥)) |
6 | | fveq1 6721 |
. . . . . . . 8
⊢ (𝑎 = 𝑓 → (𝑎‘suc 𝑥) = (𝑓‘suc 𝑥)) |
7 | | fveq1 6721 |
. . . . . . . 8
⊢ (𝑎 = 𝑓 → (𝑎‘𝑥) = (𝑓‘𝑥)) |
8 | 6, 7 | sseq12d 3939 |
. . . . . . 7
⊢ (𝑎 = 𝑓 → ((𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) ↔ (𝑓‘suc 𝑥) ⊆ (𝑓‘𝑥))) |
9 | 8 | ralbidv 3118 |
. . . . . 6
⊢ (𝑎 = 𝑓 → (∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) ↔ ∀𝑥 ∈ ω (𝑓‘suc 𝑥) ⊆ (𝑓‘𝑥))) |
10 | 5, 9 | syl5bb 286 |
. . . . 5
⊢ (𝑎 = 𝑓 → (∀𝑏 ∈ ω (𝑎‘suc 𝑏) ⊆ (𝑎‘𝑏) ↔ ∀𝑥 ∈ ω (𝑓‘suc 𝑥) ⊆ (𝑓‘𝑥))) |
11 | | rneq 5810 |
. . . . . . 7
⊢ (𝑎 = 𝑓 → ran 𝑎 = ran 𝑓) |
12 | 11 | inteqd 4869 |
. . . . . 6
⊢ (𝑎 = 𝑓 → ∩ ran
𝑎 = ∩ ran 𝑓) |
13 | 12, 11 | eleq12d 2832 |
. . . . 5
⊢ (𝑎 = 𝑓 → (∩ ran
𝑎 ∈ ran 𝑎 ↔ ∩ ran 𝑓 ∈ ran 𝑓)) |
14 | 10, 13 | imbi12d 348 |
. . . 4
⊢ (𝑎 = 𝑓 → ((∀𝑏 ∈ ω (𝑎‘suc 𝑏) ⊆ (𝑎‘𝑏) → ∩ ran
𝑎 ∈ ran 𝑎) ↔ (∀𝑥 ∈ ω (𝑓‘suc 𝑥) ⊆ (𝑓‘𝑥) → ∩ ran
𝑓 ∈ ran 𝑓))) |
15 | 14 | cbvralvw 3363 |
. . 3
⊢
(∀𝑎 ∈
(𝒫 𝑔
↑m ω)(∀𝑏 ∈ ω (𝑎‘suc 𝑏) ⊆ (𝑎‘𝑏) → ∩ ran
𝑎 ∈ ran 𝑎) ↔ ∀𝑓 ∈ (𝒫 𝑔 ↑m
ω)(∀𝑥 ∈
ω (𝑓‘suc 𝑥) ⊆ (𝑓‘𝑥) → ∩ ran
𝑓 ∈ ran 𝑓)) |
16 | | pweq 4534 |
. . . . 5
⊢ (𝑔 = 𝐴 → 𝒫 𝑔 = 𝒫 𝐴) |
17 | 16 | oveq1d 7233 |
. . . 4
⊢ (𝑔 = 𝐴 → (𝒫 𝑔 ↑m ω) = (𝒫
𝐴 ↑m
ω)) |
18 | 17 | raleqdv 3330 |
. . 3
⊢ (𝑔 = 𝐴 → (∀𝑓 ∈ (𝒫 𝑔 ↑m ω)(∀𝑥 ∈ ω (𝑓‘suc 𝑥) ⊆ (𝑓‘𝑥) → ∩ ran
𝑓 ∈ ran 𝑓) ↔ ∀𝑓 ∈ (𝒫 𝐴 ↑m
ω)(∀𝑥 ∈
ω (𝑓‘suc 𝑥) ⊆ (𝑓‘𝑥) → ∩ ran
𝑓 ∈ ran 𝑓))) |
19 | 15, 18 | syl5bb 286 |
. 2
⊢ (𝑔 = 𝐴 → (∀𝑎 ∈ (𝒫 𝑔 ↑m ω)(∀𝑏 ∈ ω (𝑎‘suc 𝑏) ⊆ (𝑎‘𝑏) → ∩ ran
𝑎 ∈ ran 𝑎) ↔ ∀𝑓 ∈ (𝒫 𝐴 ↑m
ω)(∀𝑥 ∈
ω (𝑓‘suc 𝑥) ⊆ (𝑓‘𝑥) → ∩ ran
𝑓 ∈ ran 𝑓))) |
20 | | isfin3ds.f |
. 2
⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑m ω)(∀𝑏 ∈ ω (𝑎‘suc 𝑏) ⊆ (𝑎‘𝑏) → ∩ ran
𝑎 ∈ ran 𝑎)} |
21 | 19, 20 | elab2g 3594 |
1
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐹 ↔ ∀𝑓 ∈ (𝒫 𝐴 ↑m ω)(∀𝑥 ∈ ω (𝑓‘suc 𝑥) ⊆ (𝑓‘𝑥) → ∩ ran
𝑓 ∈ ran 𝑓))) |