| Step | Hyp | Ref
| Expression |
| 1 | | epweon 7795 |
. . . . 5
⊢ E We
On |
| 2 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑦 = ∅ → (𝐹‘𝑦) = (𝐹‘∅)) |
| 3 | 2 | eleq1d 2826 |
. . . . . . . . . 10
⊢ (𝑦 = ∅ → ((𝐹‘𝑦) ∈ On ↔ (𝐹‘∅) ∈ On)) |
| 4 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑧 → (𝐹‘𝑦) = (𝐹‘𝑧)) |
| 5 | 4 | eleq1d 2826 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑧 → ((𝐹‘𝑦) ∈ On ↔ (𝐹‘𝑧) ∈ On)) |
| 6 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑦 = suc 𝑧 → (𝐹‘𝑦) = (𝐹‘suc 𝑧)) |
| 7 | 6 | eleq1d 2826 |
. . . . . . . . . 10
⊢ (𝑦 = suc 𝑧 → ((𝐹‘𝑦) ∈ On ↔ (𝐹‘suc 𝑧) ∈ On)) |
| 8 | | simpl 482 |
. . . . . . . . . 10
⊢ (((𝐹‘∅) ∈ On ∧
∀𝑥 ∈ ω
(𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) → (𝐹‘∅) ∈ On) |
| 9 | | suceq 6450 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑧 → suc 𝑥 = suc 𝑧) |
| 10 | 9 | fveq2d 6910 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑧 → (𝐹‘suc 𝑥) = (𝐹‘suc 𝑧)) |
| 11 | | fveq2 6906 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧)) |
| 12 | 10, 11 | eleq12d 2835 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑧 → ((𝐹‘suc 𝑥) ∈ (𝐹‘𝑥) ↔ (𝐹‘suc 𝑧) ∈ (𝐹‘𝑧))) |
| 13 | 12 | rspcv 3618 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ω →
(∀𝑥 ∈ ω
(𝐹‘suc 𝑥) ∈ (𝐹‘𝑥) → (𝐹‘suc 𝑧) ∈ (𝐹‘𝑧))) |
| 14 | | onelon 6409 |
. . . . . . . . . . . . 13
⊢ (((𝐹‘𝑧) ∈ On ∧ (𝐹‘suc 𝑧) ∈ (𝐹‘𝑧)) → (𝐹‘suc 𝑧) ∈ On) |
| 15 | 14 | expcom 413 |
. . . . . . . . . . . 12
⊢ ((𝐹‘suc 𝑧) ∈ (𝐹‘𝑧) → ((𝐹‘𝑧) ∈ On → (𝐹‘suc 𝑧) ∈ On)) |
| 16 | 13, 15 | syl6 35 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ω →
(∀𝑥 ∈ ω
(𝐹‘suc 𝑥) ∈ (𝐹‘𝑥) → ((𝐹‘𝑧) ∈ On → (𝐹‘suc 𝑧) ∈ On))) |
| 17 | 16 | adantld 490 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ω → (((𝐹‘∅) ∈ On ∧
∀𝑥 ∈ ω
(𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) → ((𝐹‘𝑧) ∈ On → (𝐹‘suc 𝑧) ∈ On))) |
| 18 | 3, 5, 7, 8, 17 | finds2 7920 |
. . . . . . . . 9
⊢ (𝑦 ∈ ω → (((𝐹‘∅) ∈ On ∧
∀𝑥 ∈ ω
(𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) → (𝐹‘𝑦) ∈ On)) |
| 19 | 18 | com12 32 |
. . . . . . . 8
⊢ (((𝐹‘∅) ∈ On ∧
∀𝑥 ∈ ω
(𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) → (𝑦 ∈ ω → (𝐹‘𝑦) ∈ On)) |
| 20 | 19 | ralrimiv 3145 |
. . . . . . 7
⊢ (((𝐹‘∅) ∈ On ∧
∀𝑥 ∈ ω
(𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) → ∀𝑦 ∈ ω (𝐹‘𝑦) ∈ On) |
| 21 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑦 ∈ ω ↦ (𝐹‘𝑦)) = (𝑦 ∈ ω ↦ (𝐹‘𝑦)) |
| 22 | 21 | fmpt 7130 |
. . . . . . 7
⊢
(∀𝑦 ∈
ω (𝐹‘𝑦) ∈ On ↔ (𝑦 ∈ ω ↦ (𝐹‘𝑦)):ω⟶On) |
| 23 | 20, 22 | sylib 218 |
. . . . . 6
⊢ (((𝐹‘∅) ∈ On ∧
∀𝑥 ∈ ω
(𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) → (𝑦 ∈ ω ↦ (𝐹‘𝑦)):ω⟶On) |
| 24 | 23 | frnd 6744 |
. . . . 5
⊢ (((𝐹‘∅) ∈ On ∧
∀𝑥 ∈ ω
(𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) → ran (𝑦 ∈ ω ↦ (𝐹‘𝑦)) ⊆ On) |
| 25 | | peano1 7910 |
. . . . . . . 8
⊢ ∅
∈ ω |
| 26 | 23 | fdmd 6746 |
. . . . . . . 8
⊢ (((𝐹‘∅) ∈ On ∧
∀𝑥 ∈ ω
(𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) → dom (𝑦 ∈ ω ↦ (𝐹‘𝑦)) = ω) |
| 27 | 25, 26 | eleqtrrid 2848 |
. . . . . . 7
⊢ (((𝐹‘∅) ∈ On ∧
∀𝑥 ∈ ω
(𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) → ∅ ∈ dom (𝑦 ∈ ω ↦ (𝐹‘𝑦))) |
| 28 | 27 | ne0d 4342 |
. . . . . 6
⊢ (((𝐹‘∅) ∈ On ∧
∀𝑥 ∈ ω
(𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) → dom (𝑦 ∈ ω ↦ (𝐹‘𝑦)) ≠ ∅) |
| 29 | | dm0rn0 5935 |
. . . . . . 7
⊢ (dom
(𝑦 ∈ ω ↦
(𝐹‘𝑦)) = ∅ ↔ ran (𝑦 ∈ ω ↦ (𝐹‘𝑦)) = ∅) |
| 30 | 29 | necon3bii 2993 |
. . . . . 6
⊢ (dom
(𝑦 ∈ ω ↦
(𝐹‘𝑦)) ≠ ∅ ↔ ran (𝑦 ∈ ω ↦ (𝐹‘𝑦)) ≠ ∅) |
| 31 | 28, 30 | sylib 218 |
. . . . 5
⊢ (((𝐹‘∅) ∈ On ∧
∀𝑥 ∈ ω
(𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) → ran (𝑦 ∈ ω ↦ (𝐹‘𝑦)) ≠ ∅) |
| 32 | | wefrc 5679 |
. . . . 5
⊢ (( E We
On ∧ ran (𝑦 ∈
ω ↦ (𝐹‘𝑦)) ⊆ On ∧ ran (𝑦 ∈ ω ↦ (𝐹‘𝑦)) ≠ ∅) → ∃𝑧 ∈ ran (𝑦 ∈ ω ↦ (𝐹‘𝑦))(ran (𝑦 ∈ ω ↦ (𝐹‘𝑦)) ∩ 𝑧) = ∅) |
| 33 | 1, 24, 31, 32 | mp3an2i 1468 |
. . . 4
⊢ (((𝐹‘∅) ∈ On ∧
∀𝑥 ∈ ω
(𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) → ∃𝑧 ∈ ran (𝑦 ∈ ω ↦ (𝐹‘𝑦))(ran (𝑦 ∈ ω ↦ (𝐹‘𝑦)) ∩ 𝑧) = ∅) |
| 34 | | fvex 6919 |
. . . . . 6
⊢ (𝐹‘𝑤) ∈ V |
| 35 | 34 | rgenw 3065 |
. . . . 5
⊢
∀𝑤 ∈
ω (𝐹‘𝑤) ∈ V |
| 36 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑦 = 𝑤 → (𝐹‘𝑦) = (𝐹‘𝑤)) |
| 37 | 36 | cbvmptv 5255 |
. . . . . 6
⊢ (𝑦 ∈ ω ↦ (𝐹‘𝑦)) = (𝑤 ∈ ω ↦ (𝐹‘𝑤)) |
| 38 | | ineq2 4214 |
. . . . . . 7
⊢ (𝑧 = (𝐹‘𝑤) → (ran (𝑦 ∈ ω ↦ (𝐹‘𝑦)) ∩ 𝑧) = (ran (𝑦 ∈ ω ↦ (𝐹‘𝑦)) ∩ (𝐹‘𝑤))) |
| 39 | 38 | eqeq1d 2739 |
. . . . . 6
⊢ (𝑧 = (𝐹‘𝑤) → ((ran (𝑦 ∈ ω ↦ (𝐹‘𝑦)) ∩ 𝑧) = ∅ ↔ (ran (𝑦 ∈ ω ↦ (𝐹‘𝑦)) ∩ (𝐹‘𝑤)) = ∅)) |
| 40 | 37, 39 | rexrnmptw 7115 |
. . . . 5
⊢
(∀𝑤 ∈
ω (𝐹‘𝑤) ∈ V → (∃𝑧 ∈ ran (𝑦 ∈ ω ↦ (𝐹‘𝑦))(ran (𝑦 ∈ ω ↦ (𝐹‘𝑦)) ∩ 𝑧) = ∅ ↔ ∃𝑤 ∈ ω (ran (𝑦 ∈ ω ↦ (𝐹‘𝑦)) ∩ (𝐹‘𝑤)) = ∅)) |
| 41 | 35, 40 | ax-mp 5 |
. . . 4
⊢
(∃𝑧 ∈ ran
(𝑦 ∈ ω ↦
(𝐹‘𝑦))(ran (𝑦 ∈ ω ↦ (𝐹‘𝑦)) ∩ 𝑧) = ∅ ↔ ∃𝑤 ∈ ω (ran (𝑦 ∈ ω ↦ (𝐹‘𝑦)) ∩ (𝐹‘𝑤)) = ∅) |
| 42 | 33, 41 | sylib 218 |
. . 3
⊢ (((𝐹‘∅) ∈ On ∧
∀𝑥 ∈ ω
(𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) → ∃𝑤 ∈ ω (ran (𝑦 ∈ ω ↦ (𝐹‘𝑦)) ∩ (𝐹‘𝑤)) = ∅) |
| 43 | | peano2 7912 |
. . . . . . . . 9
⊢ (𝑤 ∈ ω → suc 𝑤 ∈
ω) |
| 44 | 43 | adantl 481 |
. . . . . . . 8
⊢ ((((𝐹‘∅) ∈ On ∧
∀𝑥 ∈ ω
(𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) ∧ 𝑤 ∈ ω) → suc 𝑤 ∈
ω) |
| 45 | | eqid 2737 |
. . . . . . . 8
⊢ (𝐹‘suc 𝑤) = (𝐹‘suc 𝑤) |
| 46 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑦 = suc 𝑤 → (𝐹‘𝑦) = (𝐹‘suc 𝑤)) |
| 47 | 46 | rspceeqv 3645 |
. . . . . . . 8
⊢ ((suc
𝑤 ∈ ω ∧
(𝐹‘suc 𝑤) = (𝐹‘suc 𝑤)) → ∃𝑦 ∈ ω (𝐹‘suc 𝑤) = (𝐹‘𝑦)) |
| 48 | 44, 45, 47 | sylancl 586 |
. . . . . . 7
⊢ ((((𝐹‘∅) ∈ On ∧
∀𝑥 ∈ ω
(𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) ∧ 𝑤 ∈ ω) → ∃𝑦 ∈ ω (𝐹‘suc 𝑤) = (𝐹‘𝑦)) |
| 49 | | fvex 6919 |
. . . . . . . 8
⊢ (𝐹‘suc 𝑤) ∈ V |
| 50 | 21 | elrnmpt 5969 |
. . . . . . . 8
⊢ ((𝐹‘suc 𝑤) ∈ V → ((𝐹‘suc 𝑤) ∈ ran (𝑦 ∈ ω ↦ (𝐹‘𝑦)) ↔ ∃𝑦 ∈ ω (𝐹‘suc 𝑤) = (𝐹‘𝑦))) |
| 51 | 49, 50 | ax-mp 5 |
. . . . . . 7
⊢ ((𝐹‘suc 𝑤) ∈ ran (𝑦 ∈ ω ↦ (𝐹‘𝑦)) ↔ ∃𝑦 ∈ ω (𝐹‘suc 𝑤) = (𝐹‘𝑦)) |
| 52 | 48, 51 | sylibr 234 |
. . . . . 6
⊢ ((((𝐹‘∅) ∈ On ∧
∀𝑥 ∈ ω
(𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) ∧ 𝑤 ∈ ω) → (𝐹‘suc 𝑤) ∈ ran (𝑦 ∈ ω ↦ (𝐹‘𝑦))) |
| 53 | | suceq 6450 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑤 → suc 𝑥 = suc 𝑤) |
| 54 | 53 | fveq2d 6910 |
. . . . . . . . 9
⊢ (𝑥 = 𝑤 → (𝐹‘suc 𝑥) = (𝐹‘suc 𝑤)) |
| 55 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑥 = 𝑤 → (𝐹‘𝑥) = (𝐹‘𝑤)) |
| 56 | 54, 55 | eleq12d 2835 |
. . . . . . . 8
⊢ (𝑥 = 𝑤 → ((𝐹‘suc 𝑥) ∈ (𝐹‘𝑥) ↔ (𝐹‘suc 𝑤) ∈ (𝐹‘𝑤))) |
| 57 | 56 | rspccva 3621 |
. . . . . . 7
⊢
((∀𝑥 ∈
ω (𝐹‘suc 𝑥) ∈ (𝐹‘𝑥) ∧ 𝑤 ∈ ω) → (𝐹‘suc 𝑤) ∈ (𝐹‘𝑤)) |
| 58 | 57 | adantll 714 |
. . . . . 6
⊢ ((((𝐹‘∅) ∈ On ∧
∀𝑥 ∈ ω
(𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) ∧ 𝑤 ∈ ω) → (𝐹‘suc 𝑤) ∈ (𝐹‘𝑤)) |
| 59 | | inelcm 4465 |
. . . . . 6
⊢ (((𝐹‘suc 𝑤) ∈ ran (𝑦 ∈ ω ↦ (𝐹‘𝑦)) ∧ (𝐹‘suc 𝑤) ∈ (𝐹‘𝑤)) → (ran (𝑦 ∈ ω ↦ (𝐹‘𝑦)) ∩ (𝐹‘𝑤)) ≠ ∅) |
| 60 | 52, 58, 59 | syl2anc 584 |
. . . . 5
⊢ ((((𝐹‘∅) ∈ On ∧
∀𝑥 ∈ ω
(𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) ∧ 𝑤 ∈ ω) → (ran (𝑦 ∈ ω ↦ (𝐹‘𝑦)) ∩ (𝐹‘𝑤)) ≠ ∅) |
| 61 | 60 | neneqd 2945 |
. . . 4
⊢ ((((𝐹‘∅) ∈ On ∧
∀𝑥 ∈ ω
(𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) ∧ 𝑤 ∈ ω) → ¬ (ran (𝑦 ∈ ω ↦ (𝐹‘𝑦)) ∩ (𝐹‘𝑤)) = ∅) |
| 62 | 61 | nrexdv 3149 |
. . 3
⊢ (((𝐹‘∅) ∈ On ∧
∀𝑥 ∈ ω
(𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) → ¬ ∃𝑤 ∈ ω (ran (𝑦 ∈ ω ↦ (𝐹‘𝑦)) ∩ (𝐹‘𝑤)) = ∅) |
| 63 | 42, 62 | pm2.65da 817 |
. 2
⊢ ((𝐹‘∅) ∈ On →
¬ ∀𝑥 ∈
ω (𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) |
| 64 | | rexnal 3100 |
. 2
⊢
(∃𝑥 ∈
ω ¬ (𝐹‘suc
𝑥) ∈ (𝐹‘𝑥) ↔ ¬ ∀𝑥 ∈ ω (𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) |
| 65 | 63, 64 | sylibr 234 |
1
⊢ ((𝐹‘∅) ∈ On →
∃𝑥 ∈ ω
¬ (𝐹‘suc 𝑥) ∈ (𝐹‘𝑥)) |