Proof of Theorem axcc4
| Step | Hyp | Ref
| Expression |
| 1 | | axcc4.1 |
. . . 4
⊢ 𝐴 ∈ V |
| 2 | 1 | rabex 5339 |
. . 3
⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} ∈ V |
| 3 | | axcc4.2 |
. . 3
⊢ 𝑁 ≈
ω |
| 4 | 2, 3 | axcc3 10478 |
. 2
⊢
∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 ({𝑥 ∈ 𝐴 ∣ 𝜑} ≠ ∅ → (𝑓‘𝑛) ∈ {𝑥 ∈ 𝐴 ∣ 𝜑})) |
| 5 | | rabn0 4389 |
. . . . . . . . . 10
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ≠ ∅ ↔ ∃𝑥 ∈ 𝐴 𝜑) |
| 6 | | pm2.27 42 |
. . . . . . . . . 10
⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ≠ ∅ → (({𝑥 ∈ 𝐴 ∣ 𝜑} ≠ ∅ → (𝑓‘𝑛) ∈ {𝑥 ∈ 𝐴 ∣ 𝜑}) → (𝑓‘𝑛) ∈ {𝑥 ∈ 𝐴 ∣ 𝜑})) |
| 7 | 5, 6 | sylbir 235 |
. . . . . . . . 9
⊢
(∃𝑥 ∈
𝐴 𝜑 → (({𝑥 ∈ 𝐴 ∣ 𝜑} ≠ ∅ → (𝑓‘𝑛) ∈ {𝑥 ∈ 𝐴 ∣ 𝜑}) → (𝑓‘𝑛) ∈ {𝑥 ∈ 𝐴 ∣ 𝜑})) |
| 8 | | axcc4.3 |
. . . . . . . . . 10
⊢ (𝑥 = (𝑓‘𝑛) → (𝜑 ↔ 𝜓)) |
| 9 | 8 | elrab 3692 |
. . . . . . . . 9
⊢ ((𝑓‘𝑛) ∈ {𝑥 ∈ 𝐴 ∣ 𝜑} ↔ ((𝑓‘𝑛) ∈ 𝐴 ∧ 𝜓)) |
| 10 | 7, 9 | imbitrdi 251 |
. . . . . . . 8
⊢
(∃𝑥 ∈
𝐴 𝜑 → (({𝑥 ∈ 𝐴 ∣ 𝜑} ≠ ∅ → (𝑓‘𝑛) ∈ {𝑥 ∈ 𝐴 ∣ 𝜑}) → ((𝑓‘𝑛) ∈ 𝐴 ∧ 𝜓))) |
| 11 | 10 | ral2imi 3085 |
. . . . . . 7
⊢
(∀𝑛 ∈
𝑁 ∃𝑥 ∈ 𝐴 𝜑 → (∀𝑛 ∈ 𝑁 ({𝑥 ∈ 𝐴 ∣ 𝜑} ≠ ∅ → (𝑓‘𝑛) ∈ {𝑥 ∈ 𝐴 ∣ 𝜑}) → ∀𝑛 ∈ 𝑁 ((𝑓‘𝑛) ∈ 𝐴 ∧ 𝜓))) |
| 12 | | simpl 482 |
. . . . . . . 8
⊢ (((𝑓‘𝑛) ∈ 𝐴 ∧ 𝜓) → (𝑓‘𝑛) ∈ 𝐴) |
| 13 | 12 | ralimi 3083 |
. . . . . . 7
⊢
(∀𝑛 ∈
𝑁 ((𝑓‘𝑛) ∈ 𝐴 ∧ 𝜓) → ∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ 𝐴) |
| 14 | 11, 13 | syl6 35 |
. . . . . 6
⊢
(∀𝑛 ∈
𝑁 ∃𝑥 ∈ 𝐴 𝜑 → (∀𝑛 ∈ 𝑁 ({𝑥 ∈ 𝐴 ∣ 𝜑} ≠ ∅ → (𝑓‘𝑛) ∈ {𝑥 ∈ 𝐴 ∣ 𝜑}) → ∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ 𝐴)) |
| 15 | 14 | anim2d 612 |
. . . . 5
⊢
(∀𝑛 ∈
𝑁 ∃𝑥 ∈ 𝐴 𝜑 → ((𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 ({𝑥 ∈ 𝐴 ∣ 𝜑} ≠ ∅ → (𝑓‘𝑛) ∈ {𝑥 ∈ 𝐴 ∣ 𝜑})) → (𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ 𝐴))) |
| 16 | | ffnfv 7139 |
. . . . 5
⊢ (𝑓:𝑁⟶𝐴 ↔ (𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑓‘𝑛) ∈ 𝐴)) |
| 17 | 15, 16 | imbitrrdi 252 |
. . . 4
⊢
(∀𝑛 ∈
𝑁 ∃𝑥 ∈ 𝐴 𝜑 → ((𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 ({𝑥 ∈ 𝐴 ∣ 𝜑} ≠ ∅ → (𝑓‘𝑛) ∈ {𝑥 ∈ 𝐴 ∣ 𝜑})) → 𝑓:𝑁⟶𝐴)) |
| 18 | | simpr 484 |
. . . . . . 7
⊢ (((𝑓‘𝑛) ∈ 𝐴 ∧ 𝜓) → 𝜓) |
| 19 | 18 | ralimi 3083 |
. . . . . 6
⊢
(∀𝑛 ∈
𝑁 ((𝑓‘𝑛) ∈ 𝐴 ∧ 𝜓) → ∀𝑛 ∈ 𝑁 𝜓) |
| 20 | 11, 19 | syl6 35 |
. . . . 5
⊢
(∀𝑛 ∈
𝑁 ∃𝑥 ∈ 𝐴 𝜑 → (∀𝑛 ∈ 𝑁 ({𝑥 ∈ 𝐴 ∣ 𝜑} ≠ ∅ → (𝑓‘𝑛) ∈ {𝑥 ∈ 𝐴 ∣ 𝜑}) → ∀𝑛 ∈ 𝑁 𝜓)) |
| 21 | 20 | adantld 490 |
. . . 4
⊢
(∀𝑛 ∈
𝑁 ∃𝑥 ∈ 𝐴 𝜑 → ((𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 ({𝑥 ∈ 𝐴 ∣ 𝜑} ≠ ∅ → (𝑓‘𝑛) ∈ {𝑥 ∈ 𝐴 ∣ 𝜑})) → ∀𝑛 ∈ 𝑁 𝜓)) |
| 22 | 17, 21 | jcad 512 |
. . 3
⊢
(∀𝑛 ∈
𝑁 ∃𝑥 ∈ 𝐴 𝜑 → ((𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 ({𝑥 ∈ 𝐴 ∣ 𝜑} ≠ ∅ → (𝑓‘𝑛) ∈ {𝑥 ∈ 𝐴 ∣ 𝜑})) → (𝑓:𝑁⟶𝐴 ∧ ∀𝑛 ∈ 𝑁 𝜓))) |
| 23 | 22 | eximdv 1917 |
. 2
⊢
(∀𝑛 ∈
𝑁 ∃𝑥 ∈ 𝐴 𝜑 → (∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛 ∈ 𝑁 ({𝑥 ∈ 𝐴 ∣ 𝜑} ≠ ∅ → (𝑓‘𝑛) ∈ {𝑥 ∈ 𝐴 ∣ 𝜑})) → ∃𝑓(𝑓:𝑁⟶𝐴 ∧ ∀𝑛 ∈ 𝑁 𝜓))) |
| 24 | 4, 23 | mpi 20 |
1
⊢
(∀𝑛 ∈
𝑁 ∃𝑥 ∈ 𝐴 𝜑 → ∃𝑓(𝑓:𝑁⟶𝐴 ∧ ∀𝑛 ∈ 𝑁 𝜓)) |