| Step | Hyp | Ref
| Expression |
| 1 | | omex 9683 |
. . . . 5
⊢ ω
∈ V |
| 2 | 1 | mptex 7243 |
. . . 4
⊢ (𝑤 ∈ ω ↦ (𝐹‘𝑤)) ∈ V |
| 3 | 2 | rnex 7932 |
. . 3
⊢ ran
(𝑤 ∈ ω ↦
(𝐹‘𝑤)) ∈ V |
| 4 | | zfregfr 9645 |
. . 3
⊢ E Fr ran
(𝑤 ∈ ω ↦
(𝐹‘𝑤)) |
| 5 | | ssid 4006 |
. . 3
⊢ ran
(𝑤 ∈ ω ↦
(𝐹‘𝑤)) ⊆ ran (𝑤 ∈ ω ↦ (𝐹‘𝑤)) |
| 6 | | dmmptg 6262 |
. . . . . 6
⊢
(∀𝑤 ∈
ω (𝐹‘𝑤) ∈ V → dom (𝑤 ∈ ω ↦ (𝐹‘𝑤)) = ω) |
| 7 | | fvexd 6921 |
. . . . . 6
⊢ (𝑤 ∈ ω → (𝐹‘𝑤) ∈ V) |
| 8 | 6, 7 | mprg 3067 |
. . . . 5
⊢ dom
(𝑤 ∈ ω ↦
(𝐹‘𝑤)) = ω |
| 9 | | peano1 7910 |
. . . . . 6
⊢ ∅
∈ ω |
| 10 | 9 | ne0ii 4344 |
. . . . 5
⊢ ω
≠ ∅ |
| 11 | 8, 10 | eqnetri 3011 |
. . . 4
⊢ dom
(𝑤 ∈ ω ↦
(𝐹‘𝑤)) ≠ ∅ |
| 12 | | dm0rn0 5935 |
. . . . 5
⊢ (dom
(𝑤 ∈ ω ↦
(𝐹‘𝑤)) = ∅ ↔ ran (𝑤 ∈ ω ↦ (𝐹‘𝑤)) = ∅) |
| 13 | 12 | necon3bii 2993 |
. . . 4
⊢ (dom
(𝑤 ∈ ω ↦
(𝐹‘𝑤)) ≠ ∅ ↔ ran (𝑤 ∈ ω ↦ (𝐹‘𝑤)) ≠ ∅) |
| 14 | 11, 13 | mpbi 230 |
. . 3
⊢ ran
(𝑤 ∈ ω ↦
(𝐹‘𝑤)) ≠ ∅ |
| 15 | | fri 5642 |
. . 3
⊢ (((ran
(𝑤 ∈ ω ↦
(𝐹‘𝑤)) ∈ V ∧ E Fr ran (𝑤 ∈ ω ↦ (𝐹‘𝑤))) ∧ (ran (𝑤 ∈ ω ↦ (𝐹‘𝑤)) ⊆ ran (𝑤 ∈ ω ↦ (𝐹‘𝑤)) ∧ ran (𝑤 ∈ ω ↦ (𝐹‘𝑤)) ≠ ∅)) → ∃𝑦 ∈ ran (𝑤 ∈ ω ↦ (𝐹‘𝑤))∀𝑧 ∈ ran (𝑤 ∈ ω ↦ (𝐹‘𝑤)) ¬ 𝑧 E 𝑦) |
| 16 | 3, 4, 5, 14, 15 | mp4an 693 |
. 2
⊢
∃𝑦 ∈ ran
(𝑤 ∈ ω ↦
(𝐹‘𝑤))∀𝑧 ∈ ran (𝑤 ∈ ω ↦ (𝐹‘𝑤)) ¬ 𝑧 E 𝑦 |
| 17 | | fvex 6919 |
. . . . . . 7
⊢ (𝐹‘𝑤) ∈ V |
| 18 | | eqid 2737 |
. . . . . . 7
⊢ (𝑤 ∈ ω ↦ (𝐹‘𝑤)) = (𝑤 ∈ ω ↦ (𝐹‘𝑤)) |
| 19 | 17, 18 | fnmpti 6711 |
. . . . . 6
⊢ (𝑤 ∈ ω ↦ (𝐹‘𝑤)) Fn ω |
| 20 | | fvelrnb 6969 |
. . . . . 6
⊢ ((𝑤 ∈ ω ↦ (𝐹‘𝑤)) Fn ω → (𝑦 ∈ ran (𝑤 ∈ ω ↦ (𝐹‘𝑤)) ↔ ∃𝑥 ∈ ω ((𝑤 ∈ ω ↦ (𝐹‘𝑤))‘𝑥) = 𝑦)) |
| 21 | 19, 20 | ax-mp 5 |
. . . . 5
⊢ (𝑦 ∈ ran (𝑤 ∈ ω ↦ (𝐹‘𝑤)) ↔ ∃𝑥 ∈ ω ((𝑤 ∈ ω ↦ (𝐹‘𝑤))‘𝑥) = 𝑦) |
| 22 | | peano2 7912 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ω → suc 𝑥 ∈
ω) |
| 23 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑤 = suc 𝑥 → (𝐹‘𝑤) = (𝐹‘suc 𝑥)) |
| 24 | | fvex 6919 |
. . . . . . . . . . 11
⊢ (𝐹‘suc 𝑥) ∈ V |
| 25 | 23, 18, 24 | fvmpt 7016 |
. . . . . . . . . 10
⊢ (suc
𝑥 ∈ ω →
((𝑤 ∈ ω ↦
(𝐹‘𝑤))‘suc 𝑥) = (𝐹‘suc 𝑥)) |
| 26 | 22, 25 | syl 17 |
. . . . . . . . 9
⊢ (𝑥 ∈ ω → ((𝑤 ∈ ω ↦ (𝐹‘𝑤))‘suc 𝑥) = (𝐹‘suc 𝑥)) |
| 27 | | fnfvelrn 7100 |
. . . . . . . . . 10
⊢ (((𝑤 ∈ ω ↦ (𝐹‘𝑤)) Fn ω ∧ suc 𝑥 ∈ ω) → ((𝑤 ∈ ω ↦ (𝐹‘𝑤))‘suc 𝑥) ∈ ran (𝑤 ∈ ω ↦ (𝐹‘𝑤))) |
| 28 | 19, 22, 27 | sylancr 587 |
. . . . . . . . 9
⊢ (𝑥 ∈ ω → ((𝑤 ∈ ω ↦ (𝐹‘𝑤))‘suc 𝑥) ∈ ran (𝑤 ∈ ω ↦ (𝐹‘𝑤))) |
| 29 | 26, 28 | eqeltrrd 2842 |
. . . . . . . 8
⊢ (𝑥 ∈ ω → (𝐹‘suc 𝑥) ∈ ran (𝑤 ∈ ω ↦ (𝐹‘𝑤))) |
| 30 | | epel 5587 |
. . . . . . . . . . . 12
⊢ (𝑧 E 𝑦 ↔ 𝑧 ∈ 𝑦) |
| 31 | | eleq1 2829 |
. . . . . . . . . . . 12
⊢ (𝑧 = (𝐹‘suc 𝑥) → (𝑧 ∈ 𝑦 ↔ (𝐹‘suc 𝑥) ∈ 𝑦)) |
| 32 | 30, 31 | bitrid 283 |
. . . . . . . . . . 11
⊢ (𝑧 = (𝐹‘suc 𝑥) → (𝑧 E 𝑦 ↔ (𝐹‘suc 𝑥) ∈ 𝑦)) |
| 33 | 32 | notbid 318 |
. . . . . . . . . 10
⊢ (𝑧 = (𝐹‘suc 𝑥) → (¬ 𝑧 E 𝑦 ↔ ¬ (𝐹‘suc 𝑥) ∈ 𝑦)) |
| 34 | | df-nel 3047 |
. . . . . . . . . 10
⊢ ((𝐹‘suc 𝑥) ∉ 𝑦 ↔ ¬ (𝐹‘suc 𝑥) ∈ 𝑦) |
| 35 | 33, 34 | bitr4di 289 |
. . . . . . . . 9
⊢ (𝑧 = (𝐹‘suc 𝑥) → (¬ 𝑧 E 𝑦 ↔ (𝐹‘suc 𝑥) ∉ 𝑦)) |
| 36 | 35 | rspccv 3619 |
. . . . . . . 8
⊢
(∀𝑧 ∈
ran (𝑤 ∈ ω
↦ (𝐹‘𝑤)) ¬ 𝑧 E 𝑦 → ((𝐹‘suc 𝑥) ∈ ran (𝑤 ∈ ω ↦ (𝐹‘𝑤)) → (𝐹‘suc 𝑥) ∉ 𝑦)) |
| 37 | 29, 36 | syl5com 31 |
. . . . . . 7
⊢ (𝑥 ∈ ω →
(∀𝑧 ∈ ran
(𝑤 ∈ ω ↦
(𝐹‘𝑤)) ¬ 𝑧 E 𝑦 → (𝐹‘suc 𝑥) ∉ 𝑦)) |
| 38 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑥 → (𝐹‘𝑤) = (𝐹‘𝑥)) |
| 39 | | fvex 6919 |
. . . . . . . . . . 11
⊢ (𝐹‘𝑥) ∈ V |
| 40 | 38, 18, 39 | fvmpt 7016 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ω → ((𝑤 ∈ ω ↦ (𝐹‘𝑤))‘𝑥) = (𝐹‘𝑥)) |
| 41 | | eqeq1 2741 |
. . . . . . . . . 10
⊢ (((𝑤 ∈ ω ↦ (𝐹‘𝑤))‘𝑥) = 𝑦 → (((𝑤 ∈ ω ↦ (𝐹‘𝑤))‘𝑥) = (𝐹‘𝑥) ↔ 𝑦 = (𝐹‘𝑥))) |
| 42 | 40, 41 | syl5ibcom 245 |
. . . . . . . . 9
⊢ (𝑥 ∈ ω → (((𝑤 ∈ ω ↦ (𝐹‘𝑤))‘𝑥) = 𝑦 → 𝑦 = (𝐹‘𝑥))) |
| 43 | | neleq2 3053 |
. . . . . . . . . 10
⊢ (𝑦 = (𝐹‘𝑥) → ((𝐹‘suc 𝑥) ∉ 𝑦 ↔ (𝐹‘suc 𝑥) ∉ (𝐹‘𝑥))) |
| 44 | 43 | biimpd 229 |
. . . . . . . . 9
⊢ (𝑦 = (𝐹‘𝑥) → ((𝐹‘suc 𝑥) ∉ 𝑦 → (𝐹‘suc 𝑥) ∉ (𝐹‘𝑥))) |
| 45 | 42, 44 | syl6 35 |
. . . . . . . 8
⊢ (𝑥 ∈ ω → (((𝑤 ∈ ω ↦ (𝐹‘𝑤))‘𝑥) = 𝑦 → ((𝐹‘suc 𝑥) ∉ 𝑦 → (𝐹‘suc 𝑥) ∉ (𝐹‘𝑥)))) |
| 46 | 45 | com23 86 |
. . . . . . 7
⊢ (𝑥 ∈ ω → ((𝐹‘suc 𝑥) ∉ 𝑦 → (((𝑤 ∈ ω ↦ (𝐹‘𝑤))‘𝑥) = 𝑦 → (𝐹‘suc 𝑥) ∉ (𝐹‘𝑥)))) |
| 47 | 37, 46 | syldc 48 |
. . . . . 6
⊢
(∀𝑧 ∈
ran (𝑤 ∈ ω
↦ (𝐹‘𝑤)) ¬ 𝑧 E 𝑦 → (𝑥 ∈ ω → (((𝑤 ∈ ω ↦ (𝐹‘𝑤))‘𝑥) = 𝑦 → (𝐹‘suc 𝑥) ∉ (𝐹‘𝑥)))) |
| 48 | 47 | reximdvai 3165 |
. . . . 5
⊢
(∀𝑧 ∈
ran (𝑤 ∈ ω
↦ (𝐹‘𝑤)) ¬ 𝑧 E 𝑦 → (∃𝑥 ∈ ω ((𝑤 ∈ ω ↦ (𝐹‘𝑤))‘𝑥) = 𝑦 → ∃𝑥 ∈ ω (𝐹‘suc 𝑥) ∉ (𝐹‘𝑥))) |
| 49 | 21, 48 | biimtrid 242 |
. . . 4
⊢
(∀𝑧 ∈
ran (𝑤 ∈ ω
↦ (𝐹‘𝑤)) ¬ 𝑧 E 𝑦 → (𝑦 ∈ ran (𝑤 ∈ ω ↦ (𝐹‘𝑤)) → ∃𝑥 ∈ ω (𝐹‘suc 𝑥) ∉ (𝐹‘𝑥))) |
| 50 | 49 | com12 32 |
. . 3
⊢ (𝑦 ∈ ran (𝑤 ∈ ω ↦ (𝐹‘𝑤)) → (∀𝑧 ∈ ran (𝑤 ∈ ω ↦ (𝐹‘𝑤)) ¬ 𝑧 E 𝑦 → ∃𝑥 ∈ ω (𝐹‘suc 𝑥) ∉ (𝐹‘𝑥))) |
| 51 | 50 | rexlimiv 3148 |
. 2
⊢
(∃𝑦 ∈ ran
(𝑤 ∈ ω ↦
(𝐹‘𝑤))∀𝑧 ∈ ran (𝑤 ∈ ω ↦ (𝐹‘𝑤)) ¬ 𝑧 E 𝑦 → ∃𝑥 ∈ ω (𝐹‘suc 𝑥) ∉ (𝐹‘𝑥)) |
| 52 | 16, 51 | ax-mp 5 |
1
⊢
∃𝑥 ∈
ω (𝐹‘suc 𝑥) ∉ (𝐹‘𝑥) |