Proof of Theorem isfin3ds
Step | Hyp | Ref
| Expression |
1 | | suceq 5707 |
. . . . . . . . 9
⊢ (𝑏 = 𝑥 → suc 𝑏 = suc 𝑥) |
2 | 1 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑏 = 𝑥 → (𝑎‘suc 𝑏) = (𝑎‘suc 𝑥)) |
3 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑏 = 𝑥 → (𝑎‘𝑏) = (𝑎‘𝑥)) |
4 | 2, 3 | sseq12d 3597 |
. . . . . . 7
⊢ (𝑏 = 𝑥 → ((𝑎‘suc 𝑏) ⊆ (𝑎‘𝑏) ↔ (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥))) |
5 | 4 | cbvralv 3147 |
. . . . . 6
⊢
(∀𝑏 ∈
ω (𝑎‘suc 𝑏) ⊆ (𝑎‘𝑏) ↔ ∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥)) |
6 | | fveq1 6102 |
. . . . . . . 8
⊢ (𝑎 = 𝑓 → (𝑎‘suc 𝑥) = (𝑓‘suc 𝑥)) |
7 | | fveq1 6102 |
. . . . . . . 8
⊢ (𝑎 = 𝑓 → (𝑎‘𝑥) = (𝑓‘𝑥)) |
8 | 6, 7 | sseq12d 3597 |
. . . . . . 7
⊢ (𝑎 = 𝑓 → ((𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) ↔ (𝑓‘suc 𝑥) ⊆ (𝑓‘𝑥))) |
9 | 8 | ralbidv 2969 |
. . . . . 6
⊢ (𝑎 = 𝑓 → (∀𝑥 ∈ ω (𝑎‘suc 𝑥) ⊆ (𝑎‘𝑥) ↔ ∀𝑥 ∈ ω (𝑓‘suc 𝑥) ⊆ (𝑓‘𝑥))) |
10 | 5, 9 | syl5bb 271 |
. . . . 5
⊢ (𝑎 = 𝑓 → (∀𝑏 ∈ ω (𝑎‘suc 𝑏) ⊆ (𝑎‘𝑏) ↔ ∀𝑥 ∈ ω (𝑓‘suc 𝑥) ⊆ (𝑓‘𝑥))) |
11 | | rneq 5272 |
. . . . . . 7
⊢ (𝑎 = 𝑓 → ran 𝑎 = ran 𝑓) |
12 | 11 | inteqd 4415 |
. . . . . 6
⊢ (𝑎 = 𝑓 → ∩ ran
𝑎 = ∩ ran 𝑓) |
13 | 12, 11 | eleq12d 2682 |
. . . . 5
⊢ (𝑎 = 𝑓 → (∩ ran
𝑎 ∈ ran 𝑎 ↔ ∩ ran 𝑓 ∈ ran 𝑓)) |
14 | 10, 13 | imbi12d 333 |
. . . 4
⊢ (𝑎 = 𝑓 → ((∀𝑏 ∈ ω (𝑎‘suc 𝑏) ⊆ (𝑎‘𝑏) → ∩ ran
𝑎 ∈ ran 𝑎) ↔ (∀𝑥 ∈ ω (𝑓‘suc 𝑥) ⊆ (𝑓‘𝑥) → ∩ ran
𝑓 ∈ ran 𝑓))) |
15 | 14 | cbvralv 3147 |
. . 3
⊢
(∀𝑎 ∈
(𝒫 𝑔
↑𝑚 ω)(∀𝑏 ∈ ω (𝑎‘suc 𝑏) ⊆ (𝑎‘𝑏) → ∩ ran
𝑎 ∈ ran 𝑎) ↔ ∀𝑓 ∈ (𝒫 𝑔 ↑𝑚
ω)(∀𝑥 ∈
ω (𝑓‘suc 𝑥) ⊆ (𝑓‘𝑥) → ∩ ran
𝑓 ∈ ran 𝑓)) |
16 | | pweq 4111 |
. . . . 5
⊢ (𝑔 = 𝐴 → 𝒫 𝑔 = 𝒫 𝐴) |
17 | 16 | oveq1d 6564 |
. . . 4
⊢ (𝑔 = 𝐴 → (𝒫 𝑔 ↑𝑚 ω) =
(𝒫 𝐴
↑𝑚 ω)) |
18 | 17 | raleqdv 3121 |
. . 3
⊢ (𝑔 = 𝐴 → (∀𝑓 ∈ (𝒫 𝑔 ↑𝑚
ω)(∀𝑥 ∈
ω (𝑓‘suc 𝑥) ⊆ (𝑓‘𝑥) → ∩ ran
𝑓 ∈ ran 𝑓) ↔ ∀𝑓 ∈ (𝒫 𝐴 ↑𝑚
ω)(∀𝑥 ∈
ω (𝑓‘suc 𝑥) ⊆ (𝑓‘𝑥) → ∩ ran
𝑓 ∈ ran 𝑓))) |
19 | 15, 18 | syl5bb 271 |
. 2
⊢ (𝑔 = 𝐴 → (∀𝑎 ∈ (𝒫 𝑔 ↑𝑚
ω)(∀𝑏 ∈
ω (𝑎‘suc 𝑏) ⊆ (𝑎‘𝑏) → ∩ ran
𝑎 ∈ ran 𝑎) ↔ ∀𝑓 ∈ (𝒫 𝐴 ↑𝑚
ω)(∀𝑥 ∈
ω (𝑓‘suc 𝑥) ⊆ (𝑓‘𝑥) → ∩ ran
𝑓 ∈ ran 𝑓))) |
20 | | isfin3ds.f |
. 2
⊢ 𝐹 = {𝑔 ∣ ∀𝑎 ∈ (𝒫 𝑔 ↑𝑚
ω)(∀𝑏 ∈
ω (𝑎‘suc 𝑏) ⊆ (𝑎‘𝑏) → ∩ ran
𝑎 ∈ ran 𝑎)} |
21 | 19, 20 | elab2g 3322 |
1
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐹 ↔ ∀𝑓 ∈ (𝒫 𝐴 ↑𝑚
ω)(∀𝑥 ∈
ω (𝑓‘suc 𝑥) ⊆ (𝑓‘𝑥) → ∩ ran
𝑓 ∈ ran 𝑓))) |