Step | Hyp | Ref
| Expression |
1 | | omex 9258 |
. . . . 5
⊢ ω
∈ V |
2 | 1 | mptex 7039 |
. . . 4
⊢ (𝑤 ∈ ω ↦ (𝐹‘𝑤)) ∈ V |
3 | 2 | rnex 7690 |
. . 3
⊢ ran
(𝑤 ∈ ω ↦
(𝐹‘𝑤)) ∈ V |
4 | | zfregfr 9220 |
. . 3
⊢ E Fr ran
(𝑤 ∈ ω ↦
(𝐹‘𝑤)) |
5 | | ssid 3923 |
. . 3
⊢ ran
(𝑤 ∈ ω ↦
(𝐹‘𝑤)) ⊆ ran (𝑤 ∈ ω ↦ (𝐹‘𝑤)) |
6 | | dmmptg 6105 |
. . . . . 6
⊢
(∀𝑤 ∈
ω (𝐹‘𝑤) ∈ V → dom (𝑤 ∈ ω ↦ (𝐹‘𝑤)) = ω) |
7 | | fvexd 6732 |
. . . . . 6
⊢ (𝑤 ∈ ω → (𝐹‘𝑤) ∈ V) |
8 | 6, 7 | mprg 3075 |
. . . . 5
⊢ dom
(𝑤 ∈ ω ↦
(𝐹‘𝑤)) = ω |
9 | | peano1 7667 |
. . . . . 6
⊢ ∅
∈ ω |
10 | 9 | ne0ii 4252 |
. . . . 5
⊢ ω
≠ ∅ |
11 | 8, 10 | eqnetri 3011 |
. . . 4
⊢ dom
(𝑤 ∈ ω ↦
(𝐹‘𝑤)) ≠ ∅ |
12 | | dm0rn0 5794 |
. . . . 5
⊢ (dom
(𝑤 ∈ ω ↦
(𝐹‘𝑤)) = ∅ ↔ ran (𝑤 ∈ ω ↦ (𝐹‘𝑤)) = ∅) |
13 | 12 | necon3bii 2993 |
. . . 4
⊢ (dom
(𝑤 ∈ ω ↦
(𝐹‘𝑤)) ≠ ∅ ↔ ran (𝑤 ∈ ω ↦ (𝐹‘𝑤)) ≠ ∅) |
14 | 11, 13 | mpbi 233 |
. . 3
⊢ ran
(𝑤 ∈ ω ↦
(𝐹‘𝑤)) ≠ ∅ |
15 | | fri 5512 |
. . 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 6730 |
. . . . . . 7
⊢ (𝐹‘𝑤) ∈ V |
18 | | eqid 2737 |
. . . . . . 7
⊢ (𝑤 ∈ ω ↦ (𝐹‘𝑤)) = (𝑤 ∈ ω ↦ (𝐹‘𝑤)) |
19 | 17, 18 | fnmpti 6521 |
. . . . . 6
⊢ (𝑤 ∈ ω ↦ (𝐹‘𝑤)) Fn ω |
20 | | fvelrnb 6773 |
. . . . . 6
⊢ ((𝑤 ∈ ω ↦ (𝐹‘𝑤)) Fn ω → (𝑦 ∈ ran (𝑤 ∈ ω ↦ (𝐹‘𝑤)) ↔ ∃𝑥 ∈ ω ((𝑤 ∈ ω ↦ (𝐹‘𝑤))‘𝑥) = 𝑦)) |
21 | 19, 20 | ax-mp 5 |
. . . . 5
⊢ (𝑦 ∈ ran (𝑤 ∈ ω ↦ (𝐹‘𝑤)) ↔ ∃𝑥 ∈ ω ((𝑤 ∈ ω ↦ (𝐹‘𝑤))‘𝑥) = 𝑦) |
22 | | peano2 7668 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ω → suc 𝑥 ∈
ω) |
23 | | fveq2 6717 |
. . . . . . . . . . 11
⊢ (𝑤 = suc 𝑥 → (𝐹‘𝑤) = (𝐹‘suc 𝑥)) |
24 | | fvex 6730 |
. . . . . . . . . . 11
⊢ (𝐹‘suc 𝑥) ∈ V |
25 | 23, 18, 24 | fvmpt 6818 |
. . . . . . . . . 10
⊢ (suc
𝑥 ∈ ω →
((𝑤 ∈ ω ↦
(𝐹‘𝑤))‘suc 𝑥) = (𝐹‘suc 𝑥)) |
26 | 22, 25 | syl 17 |
. . . . . . . . 9
⊢ (𝑥 ∈ ω → ((𝑤 ∈ ω ↦ (𝐹‘𝑤))‘suc 𝑥) = (𝐹‘suc 𝑥)) |
27 | | fnfvelrn 6901 |
. . . . . . . . . 10
⊢ (((𝑤 ∈ ω ↦ (𝐹‘𝑤)) Fn ω ∧ suc 𝑥 ∈ ω) → ((𝑤 ∈ ω ↦ (𝐹‘𝑤))‘suc 𝑥) ∈ ran (𝑤 ∈ ω ↦ (𝐹‘𝑤))) |
28 | 19, 22, 27 | sylancr 590 |
. . . . . . . . 9
⊢ (𝑥 ∈ ω → ((𝑤 ∈ ω ↦ (𝐹‘𝑤))‘suc 𝑥) ∈ ran (𝑤 ∈ ω ↦ (𝐹‘𝑤))) |
29 | 26, 28 | eqeltrrd 2839 |
. . . . . . . 8
⊢ (𝑥 ∈ ω → (𝐹‘suc 𝑥) ∈ ran (𝑤 ∈ ω ↦ (𝐹‘𝑤))) |
30 | | epel 5463 |
. . . . . . . . . . . 12
⊢ (𝑧 E 𝑦 ↔ 𝑧 ∈ 𝑦) |
31 | | eleq1 2825 |
. . . . . . . . . . . 12
⊢ (𝑧 = (𝐹‘suc 𝑥) → (𝑧 ∈ 𝑦 ↔ (𝐹‘suc 𝑥) ∈ 𝑦)) |
32 | 30, 31 | syl5bb 286 |
. . . . . . . . . . 11
⊢ (𝑧 = (𝐹‘suc 𝑥) → (𝑧 E 𝑦 ↔ (𝐹‘suc 𝑥) ∈ 𝑦)) |
33 | 32 | notbid 321 |
. . . . . . . . . 10
⊢ (𝑧 = (𝐹‘suc 𝑥) → (¬ 𝑧 E 𝑦 ↔ ¬ (𝐹‘suc 𝑥) ∈ 𝑦)) |
34 | | df-nel 3047 |
. . . . . . . . . 10
⊢ ((𝐹‘suc 𝑥) ∉ 𝑦 ↔ ¬ (𝐹‘suc 𝑥) ∈ 𝑦) |
35 | 33, 34 | bitr4di 292 |
. . . . . . . . 9
⊢ (𝑧 = (𝐹‘suc 𝑥) → (¬ 𝑧 E 𝑦 ↔ (𝐹‘suc 𝑥) ∉ 𝑦)) |
36 | 35 | rspccv 3534 |
. . . . . . . 8
⊢
(∀𝑧 ∈
ran (𝑤 ∈ ω
↦ (𝐹‘𝑤)) ¬ 𝑧 E 𝑦 → ((𝐹‘suc 𝑥) ∈ ran (𝑤 ∈ ω ↦ (𝐹‘𝑤)) → (𝐹‘suc 𝑥) ∉ 𝑦)) |
37 | 29, 36 | syl5com 31 |
. . . . . . 7
⊢ (𝑥 ∈ ω →
(∀𝑧 ∈ ran
(𝑤 ∈ ω ↦
(𝐹‘𝑤)) ¬ 𝑧 E 𝑦 → (𝐹‘suc 𝑥) ∉ 𝑦)) |
38 | | fveq2 6717 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑥 → (𝐹‘𝑤) = (𝐹‘𝑥)) |
39 | | fvex 6730 |
. . . . . . . . . . 11
⊢ (𝐹‘𝑥) ∈ V |
40 | 38, 18, 39 | fvmpt 6818 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ω → ((𝑤 ∈ ω ↦ (𝐹‘𝑤))‘𝑥) = (𝐹‘𝑥)) |
41 | | eqeq1 2741 |
. . . . . . . . . 10
⊢ (((𝑤 ∈ ω ↦ (𝐹‘𝑤))‘𝑥) = 𝑦 → (((𝑤 ∈ ω ↦ (𝐹‘𝑤))‘𝑥) = (𝐹‘𝑥) ↔ 𝑦 = (𝐹‘𝑥))) |
42 | 40, 41 | syl5ibcom 248 |
. . . . . . . . 9
⊢ (𝑥 ∈ ω → (((𝑤 ∈ ω ↦ (𝐹‘𝑤))‘𝑥) = 𝑦 → 𝑦 = (𝐹‘𝑥))) |
43 | | neleq2 3052 |
. . . . . . . . . 10
⊢ (𝑦 = (𝐹‘𝑥) → ((𝐹‘suc 𝑥) ∉ 𝑦 ↔ (𝐹‘suc 𝑥) ∉ (𝐹‘𝑥))) |
44 | 43 | biimpd 232 |
. . . . . . . . 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 3191 |
. . . . 5
⊢
(∀𝑧 ∈
ran (𝑤 ∈ ω
↦ (𝐹‘𝑤)) ¬ 𝑧 E 𝑦 → (∃𝑥 ∈ ω ((𝑤 ∈ ω ↦ (𝐹‘𝑤))‘𝑥) = 𝑦 → ∃𝑥 ∈ ω (𝐹‘suc 𝑥) ∉ (𝐹‘𝑥))) |
49 | 21, 48 | syl5bi 245 |
. . . 4
⊢
(∀𝑧 ∈
ran (𝑤 ∈ ω
↦ (𝐹‘𝑤)) ¬ 𝑧 E 𝑦 → (𝑦 ∈ ran (𝑤 ∈ ω ↦ (𝐹‘𝑤)) → ∃𝑥 ∈ ω (𝐹‘suc 𝑥) ∉ (𝐹‘𝑥))) |
50 | 49 | com12 32 |
. . 3
⊢ (𝑦 ∈ ran (𝑤 ∈ ω ↦ (𝐹‘𝑤)) → (∀𝑧 ∈ ran (𝑤 ∈ ω ↦ (𝐹‘𝑤)) ¬ 𝑧 E 𝑦 → ∃𝑥 ∈ ω (𝐹‘suc 𝑥) ∉ (𝐹‘𝑥))) |
51 | 50 | rexlimiv 3199 |
. 2
⊢
(∃𝑦 ∈ ran
(𝑤 ∈ ω ↦
(𝐹‘𝑤))∀𝑧 ∈ ran (𝑤 ∈ ω ↦ (𝐹‘𝑤)) ¬ 𝑧 E 𝑦 → ∃𝑥 ∈ ω (𝐹‘suc 𝑥) ∉ (𝐹‘𝑥)) |
52 | 16, 51 | ax-mp 5 |
1
⊢
∃𝑥 ∈
ω (𝐹‘suc 𝑥) ∉ (𝐹‘𝑥) |