Step | Hyp | Ref
| Expression |
1 | | epweon 6875 |
. . . . . 6
⊢ E We
On |
2 | 1 | a1i 11 |
. . . . 5
⊢ (((𝐹‘∅) ∈ On ∧
∀𝑥 ∈ ω
(𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) → E We On) |
3 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑦 = ∅ → (𝐹‘𝑦) = (𝐹‘∅)) |
4 | 3 | eleq1d 2672 |
. . . . . . . . . 10
⊢ (𝑦 = ∅ → ((𝐹‘𝑦) ∈ On ↔ (𝐹‘∅) ∈ On)) |
5 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑧 → (𝐹‘𝑦) = (𝐹‘𝑧)) |
6 | 5 | eleq1d 2672 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑧 → ((𝐹‘𝑦) ∈ On ↔ (𝐹‘𝑧) ∈ On)) |
7 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑦 = suc 𝑧 → (𝐹‘𝑦) = (𝐹‘suc 𝑧)) |
8 | 7 | eleq1d 2672 |
. . . . . . . . . 10
⊢ (𝑦 = suc 𝑧 → ((𝐹‘𝑦) ∈ On ↔ (𝐹‘suc 𝑧) ∈ On)) |
9 | | simpl 472 |
. . . . . . . . . 10
⊢ (((𝐹‘∅) ∈ On ∧
∀𝑥 ∈ ω
(𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) → (𝐹‘∅) ∈ On) |
10 | | suceq 5707 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑧 → suc 𝑥 = suc 𝑧) |
11 | 10 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑧 → (𝐹‘suc 𝑥) = (𝐹‘suc 𝑧)) |
12 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧)) |
13 | 11, 12 | eleq12d 2682 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑧 → ((𝐹‘suc 𝑥) ∈ (𝐹‘𝑥) ↔ (𝐹‘suc 𝑧) ∈ (𝐹‘𝑧))) |
14 | 13 | rspcv 3278 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ω →
(∀𝑥 ∈ ω
(𝐹‘suc 𝑥) ∈ (𝐹‘𝑥) → (𝐹‘suc 𝑧) ∈ (𝐹‘𝑧))) |
15 | | onelon 5665 |
. . . . . . . . . . . . 13
⊢ (((𝐹‘𝑧) ∈ On ∧ (𝐹‘suc 𝑧) ∈ (𝐹‘𝑧)) → (𝐹‘suc 𝑧) ∈ On) |
16 | 15 | expcom 450 |
. . . . . . . . . . . 12
⊢ ((𝐹‘suc 𝑧) ∈ (𝐹‘𝑧) → ((𝐹‘𝑧) ∈ On → (𝐹‘suc 𝑧) ∈ On)) |
17 | 14, 16 | syl6 34 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ω →
(∀𝑥 ∈ ω
(𝐹‘suc 𝑥) ∈ (𝐹‘𝑥) → ((𝐹‘𝑧) ∈ On → (𝐹‘suc 𝑧) ∈ On))) |
18 | 17 | adantld 482 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ω → (((𝐹‘∅) ∈ On ∧
∀𝑥 ∈ ω
(𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) → ((𝐹‘𝑧) ∈ On → (𝐹‘suc 𝑧) ∈ On))) |
19 | 4, 6, 8, 9, 18 | finds2 6986 |
. . . . . . . . 9
⊢ (𝑦 ∈ ω → (((𝐹‘∅) ∈ On ∧
∀𝑥 ∈ ω
(𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) → (𝐹‘𝑦) ∈ On)) |
20 | 19 | com12 32 |
. . . . . . . 8
⊢ (((𝐹‘∅) ∈ On ∧
∀𝑥 ∈ ω
(𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) → (𝑦 ∈ ω → (𝐹‘𝑦) ∈ On)) |
21 | 20 | ralrimiv 2948 |
. . . . . . 7
⊢ (((𝐹‘∅) ∈ On ∧
∀𝑥 ∈ ω
(𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) → ∀𝑦 ∈ ω (𝐹‘𝑦) ∈ On) |
22 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑦 ∈ ω ↦ (𝐹‘𝑦)) = (𝑦 ∈ ω ↦ (𝐹‘𝑦)) |
23 | 22 | fmpt 6289 |
. . . . . . 7
⊢
(∀𝑦 ∈
ω (𝐹‘𝑦) ∈ On ↔ (𝑦 ∈ ω ↦ (𝐹‘𝑦)):ω⟶On) |
24 | 21, 23 | sylib 207 |
. . . . . 6
⊢ (((𝐹‘∅) ∈ On ∧
∀𝑥 ∈ ω
(𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) → (𝑦 ∈ ω ↦ (𝐹‘𝑦)):ω⟶On) |
25 | | frn 5966 |
. . . . . 6
⊢ ((𝑦 ∈ ω ↦ (𝐹‘𝑦)):ω⟶On → ran (𝑦 ∈ ω ↦ (𝐹‘𝑦)) ⊆ On) |
26 | 24, 25 | syl 17 |
. . . . 5
⊢ (((𝐹‘∅) ∈ On ∧
∀𝑥 ∈ ω
(𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) → ran (𝑦 ∈ ω ↦ (𝐹‘𝑦)) ⊆ On) |
27 | | peano1 6977 |
. . . . . . . 8
⊢ ∅
∈ ω |
28 | | fdm 5964 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ω ↦ (𝐹‘𝑦)):ω⟶On → dom (𝑦 ∈ ω ↦ (𝐹‘𝑦)) = ω) |
29 | 24, 28 | syl 17 |
. . . . . . . 8
⊢ (((𝐹‘∅) ∈ On ∧
∀𝑥 ∈ ω
(𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) → dom (𝑦 ∈ ω ↦ (𝐹‘𝑦)) = ω) |
30 | 27, 29 | syl5eleqr 2695 |
. . . . . . 7
⊢ (((𝐹‘∅) ∈ On ∧
∀𝑥 ∈ ω
(𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) → ∅ ∈ dom (𝑦 ∈ ω ↦ (𝐹‘𝑦))) |
31 | | ne0i 3880 |
. . . . . . 7
⊢ (∅
∈ dom (𝑦 ∈
ω ↦ (𝐹‘𝑦)) → dom (𝑦 ∈ ω ↦ (𝐹‘𝑦)) ≠ ∅) |
32 | 30, 31 | syl 17 |
. . . . . 6
⊢ (((𝐹‘∅) ∈ On ∧
∀𝑥 ∈ ω
(𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) → dom (𝑦 ∈ ω ↦ (𝐹‘𝑦)) ≠ ∅) |
33 | | dm0rn0 5263 |
. . . . . . 7
⊢ (dom
(𝑦 ∈ ω ↦
(𝐹‘𝑦)) = ∅ ↔ ran (𝑦 ∈ ω ↦ (𝐹‘𝑦)) = ∅) |
34 | 33 | necon3bii 2834 |
. . . . . 6
⊢ (dom
(𝑦 ∈ ω ↦
(𝐹‘𝑦)) ≠ ∅ ↔ ran (𝑦 ∈ ω ↦ (𝐹‘𝑦)) ≠ ∅) |
35 | 32, 34 | sylib 207 |
. . . . 5
⊢ (((𝐹‘∅) ∈ On ∧
∀𝑥 ∈ ω
(𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) → ran (𝑦 ∈ ω ↦ (𝐹‘𝑦)) ≠ ∅) |
36 | | wefrc 5032 |
. . . . 5
⊢ (( E We
On ∧ ran (𝑦 ∈
ω ↦ (𝐹‘𝑦)) ⊆ On ∧ ran (𝑦 ∈ ω ↦ (𝐹‘𝑦)) ≠ ∅) → ∃𝑧 ∈ ran (𝑦 ∈ ω ↦ (𝐹‘𝑦))(ran (𝑦 ∈ ω ↦ (𝐹‘𝑦)) ∩ 𝑧) = ∅) |
37 | 2, 26, 35, 36 | syl3anc 1318 |
. . . 4
⊢ (((𝐹‘∅) ∈ On ∧
∀𝑥 ∈ ω
(𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) → ∃𝑧 ∈ ran (𝑦 ∈ ω ↦ (𝐹‘𝑦))(ran (𝑦 ∈ ω ↦ (𝐹‘𝑦)) ∩ 𝑧) = ∅) |
38 | | fvex 6113 |
. . . . . 6
⊢ (𝐹‘𝑤) ∈ V |
39 | 38 | rgenw 2908 |
. . . . 5
⊢
∀𝑤 ∈
ω (𝐹‘𝑤) ∈ V |
40 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑦 = 𝑤 → (𝐹‘𝑦) = (𝐹‘𝑤)) |
41 | 40 | cbvmptv 4678 |
. . . . . 6
⊢ (𝑦 ∈ ω ↦ (𝐹‘𝑦)) = (𝑤 ∈ ω ↦ (𝐹‘𝑤)) |
42 | | ineq2 3770 |
. . . . . . 7
⊢ (𝑧 = (𝐹‘𝑤) → (ran (𝑦 ∈ ω ↦ (𝐹‘𝑦)) ∩ 𝑧) = (ran (𝑦 ∈ ω ↦ (𝐹‘𝑦)) ∩ (𝐹‘𝑤))) |
43 | 42 | eqeq1d 2612 |
. . . . . 6
⊢ (𝑧 = (𝐹‘𝑤) → ((ran (𝑦 ∈ ω ↦ (𝐹‘𝑦)) ∩ 𝑧) = ∅ ↔ (ran (𝑦 ∈ ω ↦ (𝐹‘𝑦)) ∩ (𝐹‘𝑤)) = ∅)) |
44 | 41, 43 | rexrnmpt 6277 |
. . . . 5
⊢
(∀𝑤 ∈
ω (𝐹‘𝑤) ∈ V → (∃𝑧 ∈ ran (𝑦 ∈ ω ↦ (𝐹‘𝑦))(ran (𝑦 ∈ ω ↦ (𝐹‘𝑦)) ∩ 𝑧) = ∅ ↔ ∃𝑤 ∈ ω (ran (𝑦 ∈ ω ↦ (𝐹‘𝑦)) ∩ (𝐹‘𝑤)) = ∅)) |
45 | 39, 44 | ax-mp 5 |
. . . 4
⊢
(∃𝑧 ∈ ran
(𝑦 ∈ ω ↦
(𝐹‘𝑦))(ran (𝑦 ∈ ω ↦ (𝐹‘𝑦)) ∩ 𝑧) = ∅ ↔ ∃𝑤 ∈ ω (ran (𝑦 ∈ ω ↦ (𝐹‘𝑦)) ∩ (𝐹‘𝑤)) = ∅) |
46 | 37, 45 | sylib 207 |
. . 3
⊢ (((𝐹‘∅) ∈ On ∧
∀𝑥 ∈ ω
(𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) → ∃𝑤 ∈ ω (ran (𝑦 ∈ ω ↦ (𝐹‘𝑦)) ∩ (𝐹‘𝑤)) = ∅) |
47 | | peano2 6978 |
. . . . . . . . 9
⊢ (𝑤 ∈ ω → suc 𝑤 ∈
ω) |
48 | 47 | adantl 481 |
. . . . . . . 8
⊢ ((((𝐹‘∅) ∈ On ∧
∀𝑥 ∈ ω
(𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) ∧ 𝑤 ∈ ω) → suc 𝑤 ∈
ω) |
49 | | eqid 2610 |
. . . . . . . 8
⊢ (𝐹‘suc 𝑤) = (𝐹‘suc 𝑤) |
50 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑦 = suc 𝑤 → (𝐹‘𝑦) = (𝐹‘suc 𝑤)) |
51 | 50 | eqeq2d 2620 |
. . . . . . . . 9
⊢ (𝑦 = suc 𝑤 → ((𝐹‘suc 𝑤) = (𝐹‘𝑦) ↔ (𝐹‘suc 𝑤) = (𝐹‘suc 𝑤))) |
52 | 51 | rspcev 3282 |
. . . . . . . 8
⊢ ((suc
𝑤 ∈ ω ∧
(𝐹‘suc 𝑤) = (𝐹‘suc 𝑤)) → ∃𝑦 ∈ ω (𝐹‘suc 𝑤) = (𝐹‘𝑦)) |
53 | 48, 49, 52 | sylancl 693 |
. . . . . . 7
⊢ ((((𝐹‘∅) ∈ On ∧
∀𝑥 ∈ ω
(𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) ∧ 𝑤 ∈ ω) → ∃𝑦 ∈ ω (𝐹‘suc 𝑤) = (𝐹‘𝑦)) |
54 | | fvex 6113 |
. . . . . . . 8
⊢ (𝐹‘suc 𝑤) ∈ V |
55 | 22 | elrnmpt 5293 |
. . . . . . . 8
⊢ ((𝐹‘suc 𝑤) ∈ V → ((𝐹‘suc 𝑤) ∈ ran (𝑦 ∈ ω ↦ (𝐹‘𝑦)) ↔ ∃𝑦 ∈ ω (𝐹‘suc 𝑤) = (𝐹‘𝑦))) |
56 | 54, 55 | ax-mp 5 |
. . . . . . 7
⊢ ((𝐹‘suc 𝑤) ∈ ran (𝑦 ∈ ω ↦ (𝐹‘𝑦)) ↔ ∃𝑦 ∈ ω (𝐹‘suc 𝑤) = (𝐹‘𝑦)) |
57 | 53, 56 | sylibr 223 |
. . . . . 6
⊢ ((((𝐹‘∅) ∈ On ∧
∀𝑥 ∈ ω
(𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) ∧ 𝑤 ∈ ω) → (𝐹‘suc 𝑤) ∈ ran (𝑦 ∈ ω ↦ (𝐹‘𝑦))) |
58 | | suceq 5707 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑤 → suc 𝑥 = suc 𝑤) |
59 | 58 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑥 = 𝑤 → (𝐹‘suc 𝑥) = (𝐹‘suc 𝑤)) |
60 | | fveq2 6103 |
. . . . . . . . 9
⊢ (𝑥 = 𝑤 → (𝐹‘𝑥) = (𝐹‘𝑤)) |
61 | 59, 60 | eleq12d 2682 |
. . . . . . . 8
⊢ (𝑥 = 𝑤 → ((𝐹‘suc 𝑥) ∈ (𝐹‘𝑥) ↔ (𝐹‘suc 𝑤) ∈ (𝐹‘𝑤))) |
62 | 61 | rspccva 3281 |
. . . . . . 7
⊢
((∀𝑥 ∈
ω (𝐹‘suc 𝑥) ∈ (𝐹‘𝑥) ∧ 𝑤 ∈ ω) → (𝐹‘suc 𝑤) ∈ (𝐹‘𝑤)) |
63 | 62 | adantll 746 |
. . . . . 6
⊢ ((((𝐹‘∅) ∈ On ∧
∀𝑥 ∈ ω
(𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) ∧ 𝑤 ∈ ω) → (𝐹‘suc 𝑤) ∈ (𝐹‘𝑤)) |
64 | | inelcm 3984 |
. . . . . 6
⊢ (((𝐹‘suc 𝑤) ∈ ran (𝑦 ∈ ω ↦ (𝐹‘𝑦)) ∧ (𝐹‘suc 𝑤) ∈ (𝐹‘𝑤)) → (ran (𝑦 ∈ ω ↦ (𝐹‘𝑦)) ∩ (𝐹‘𝑤)) ≠ ∅) |
65 | 57, 63, 64 | syl2anc 691 |
. . . . 5
⊢ ((((𝐹‘∅) ∈ On ∧
∀𝑥 ∈ ω
(𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) ∧ 𝑤 ∈ ω) → (ran (𝑦 ∈ ω ↦ (𝐹‘𝑦)) ∩ (𝐹‘𝑤)) ≠ ∅) |
66 | 65 | neneqd 2787 |
. . . 4
⊢ ((((𝐹‘∅) ∈ On ∧
∀𝑥 ∈ ω
(𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) ∧ 𝑤 ∈ ω) → ¬ (ran (𝑦 ∈ ω ↦ (𝐹‘𝑦)) ∩ (𝐹‘𝑤)) = ∅) |
67 | 66 | nrexdv 2984 |
. . 3
⊢ (((𝐹‘∅) ∈ On ∧
∀𝑥 ∈ ω
(𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) → ¬ ∃𝑤 ∈ ω (ran (𝑦 ∈ ω ↦ (𝐹‘𝑦)) ∩ (𝐹‘𝑤)) = ∅) |
68 | 46, 67 | pm2.65da 598 |
. 2
⊢ ((𝐹‘∅) ∈ On →
¬ ∀𝑥 ∈
ω (𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) |
69 | | rexnal 2978 |
. 2
⊢
(∃𝑥 ∈
ω ¬ (𝐹‘suc
𝑥) ∈ (𝐹‘𝑥) ↔ ¬ ∀𝑥 ∈ ω (𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) |
70 | 68, 69 | sylibr 223 |
1
⊢ ((𝐹‘∅) ∈ On →
∃𝑥 ∈ ω
¬ (𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) |