Step | Hyp | Ref
| Expression |
1 | | breq1 3968 |
. . . . . 6
⊢ (𝑥 = ∅ → (𝑥 ≈ 𝑧 ↔ ∅ ≈ 𝑧)) |
2 | | eqeq1 2164 |
. . . . . 6
⊢ (𝑥 = ∅ → (𝑥 = 𝑧 ↔ ∅ = 𝑧)) |
3 | 1, 2 | imbi12d 233 |
. . . . 5
⊢ (𝑥 = ∅ → ((𝑥 ≈ 𝑧 → 𝑥 = 𝑧) ↔ (∅ ≈ 𝑧 → ∅ = 𝑧))) |
4 | 3 | ralbidv 2457 |
. . . 4
⊢ (𝑥 = ∅ → (∀𝑧 ∈ ω (𝑥 ≈ 𝑧 → 𝑥 = 𝑧) ↔ ∀𝑧 ∈ ω (∅ ≈ 𝑧 → ∅ = 𝑧))) |
5 | | breq1 3968 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑥 ≈ 𝑧 ↔ 𝑦 ≈ 𝑧)) |
6 | | eqeq1 2164 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 ↔ 𝑦 = 𝑧)) |
7 | 5, 6 | imbi12d 233 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝑥 ≈ 𝑧 → 𝑥 = 𝑧) ↔ (𝑦 ≈ 𝑧 → 𝑦 = 𝑧))) |
8 | 7 | ralbidv 2457 |
. . . 4
⊢ (𝑥 = 𝑦 → (∀𝑧 ∈ ω (𝑥 ≈ 𝑧 → 𝑥 = 𝑧) ↔ ∀𝑧 ∈ ω (𝑦 ≈ 𝑧 → 𝑦 = 𝑧))) |
9 | | breq1 3968 |
. . . . . 6
⊢ (𝑥 = suc 𝑦 → (𝑥 ≈ 𝑧 ↔ suc 𝑦 ≈ 𝑧)) |
10 | | eqeq1 2164 |
. . . . . 6
⊢ (𝑥 = suc 𝑦 → (𝑥 = 𝑧 ↔ suc 𝑦 = 𝑧)) |
11 | 9, 10 | imbi12d 233 |
. . . . 5
⊢ (𝑥 = suc 𝑦 → ((𝑥 ≈ 𝑧 → 𝑥 = 𝑧) ↔ (suc 𝑦 ≈ 𝑧 → suc 𝑦 = 𝑧))) |
12 | 11 | ralbidv 2457 |
. . . 4
⊢ (𝑥 = suc 𝑦 → (∀𝑧 ∈ ω (𝑥 ≈ 𝑧 → 𝑥 = 𝑧) ↔ ∀𝑧 ∈ ω (suc 𝑦 ≈ 𝑧 → suc 𝑦 = 𝑧))) |
13 | | breq1 3968 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (𝑥 ≈ 𝑧 ↔ 𝐴 ≈ 𝑧)) |
14 | | eqeq1 2164 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (𝑥 = 𝑧 ↔ 𝐴 = 𝑧)) |
15 | 13, 14 | imbi12d 233 |
. . . . 5
⊢ (𝑥 = 𝐴 → ((𝑥 ≈ 𝑧 → 𝑥 = 𝑧) ↔ (𝐴 ≈ 𝑧 → 𝐴 = 𝑧))) |
16 | 15 | ralbidv 2457 |
. . . 4
⊢ (𝑥 = 𝐴 → (∀𝑧 ∈ ω (𝑥 ≈ 𝑧 → 𝑥 = 𝑧) ↔ ∀𝑧 ∈ ω (𝐴 ≈ 𝑧 → 𝐴 = 𝑧))) |
17 | | ensym 6723 |
. . . . . 6
⊢ (∅
≈ 𝑧 → 𝑧 ≈
∅) |
18 | | en0 6737 |
. . . . . . 7
⊢ (𝑧 ≈ ∅ ↔ 𝑧 = ∅) |
19 | | eqcom 2159 |
. . . . . . 7
⊢ (𝑧 = ∅ ↔ ∅ =
𝑧) |
20 | 18, 19 | bitri 183 |
. . . . . 6
⊢ (𝑧 ≈ ∅ ↔ ∅
= 𝑧) |
21 | 17, 20 | sylib 121 |
. . . . 5
⊢ (∅
≈ 𝑧 → ∅ =
𝑧) |
22 | 21 | rgenw 2512 |
. . . 4
⊢
∀𝑧 ∈
ω (∅ ≈ 𝑧
→ ∅ = 𝑧) |
23 | | nn0suc 4562 |
. . . . . . 7
⊢ (𝑤 ∈ ω → (𝑤 = ∅ ∨ ∃𝑧 ∈ ω 𝑤 = suc 𝑧)) |
24 | | en0 6737 |
. . . . . . . . . . . 12
⊢ (suc
𝑦 ≈ ∅ ↔
suc 𝑦 =
∅) |
25 | | breq2 3969 |
. . . . . . . . . . . . 13
⊢ (𝑤 = ∅ → (suc 𝑦 ≈ 𝑤 ↔ suc 𝑦 ≈ ∅)) |
26 | | eqeq2 2167 |
. . . . . . . . . . . . 13
⊢ (𝑤 = ∅ → (suc 𝑦 = 𝑤 ↔ suc 𝑦 = ∅)) |
27 | 25, 26 | bibi12d 234 |
. . . . . . . . . . . 12
⊢ (𝑤 = ∅ → ((suc 𝑦 ≈ 𝑤 ↔ suc 𝑦 = 𝑤) ↔ (suc 𝑦 ≈ ∅ ↔ suc 𝑦 = ∅))) |
28 | 24, 27 | mpbiri 167 |
. . . . . . . . . . 11
⊢ (𝑤 = ∅ → (suc 𝑦 ≈ 𝑤 ↔ suc 𝑦 = 𝑤)) |
29 | 28 | biimpd 143 |
. . . . . . . . . 10
⊢ (𝑤 = ∅ → (suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤)) |
30 | 29 | a1i 9 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ω ∧
∀𝑧 ∈ ω
(𝑦 ≈ 𝑧 → 𝑦 = 𝑧)) → (𝑤 = ∅ → (suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤))) |
31 | | nfv 1508 |
. . . . . . . . . . 11
⊢
Ⅎ𝑧 𝑦 ∈ ω |
32 | | nfra1 2488 |
. . . . . . . . . . 11
⊢
Ⅎ𝑧∀𝑧 ∈ ω (𝑦 ≈ 𝑧 → 𝑦 = 𝑧) |
33 | 31, 32 | nfan 1545 |
. . . . . . . . . 10
⊢
Ⅎ𝑧(𝑦 ∈ ω ∧
∀𝑧 ∈ ω
(𝑦 ≈ 𝑧 → 𝑦 = 𝑧)) |
34 | | nfv 1508 |
. . . . . . . . . 10
⊢
Ⅎ𝑧(suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤) |
35 | | rsp 2504 |
. . . . . . . . . . . . . 14
⊢
(∀𝑧 ∈
ω (𝑦 ≈ 𝑧 → 𝑦 = 𝑧) → (𝑧 ∈ ω → (𝑦 ≈ 𝑧 → 𝑦 = 𝑧))) |
36 | | vex 2715 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑦 ∈ V |
37 | | vex 2715 |
. . . . . . . . . . . . . . . . . 18
⊢ 𝑧 ∈ V |
38 | 36, 37 | phplem4 6797 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ω ∧ 𝑧 ∈ ω) → (suc
𝑦 ≈ suc 𝑧 → 𝑦 ≈ 𝑧)) |
39 | 38 | imim1d 75 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ω ∧ 𝑧 ∈ ω) → ((𝑦 ≈ 𝑧 → 𝑦 = 𝑧) → (suc 𝑦 ≈ suc 𝑧 → 𝑦 = 𝑧))) |
40 | 39 | ex 114 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ω → (𝑧 ∈ ω → ((𝑦 ≈ 𝑧 → 𝑦 = 𝑧) → (suc 𝑦 ≈ suc 𝑧 → 𝑦 = 𝑧)))) |
41 | 40 | a2d 26 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ω → ((𝑧 ∈ ω → (𝑦 ≈ 𝑧 → 𝑦 = 𝑧)) → (𝑧 ∈ ω → (suc 𝑦 ≈ suc 𝑧 → 𝑦 = 𝑧)))) |
42 | 35, 41 | syl5 32 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ω →
(∀𝑧 ∈ ω
(𝑦 ≈ 𝑧 → 𝑦 = 𝑧) → (𝑧 ∈ ω → (suc 𝑦 ≈ suc 𝑧 → 𝑦 = 𝑧)))) |
43 | 42 | imp 123 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ω ∧
∀𝑧 ∈ ω
(𝑦 ≈ 𝑧 → 𝑦 = 𝑧)) → (𝑧 ∈ ω → (suc 𝑦 ≈ suc 𝑧 → 𝑦 = 𝑧))) |
44 | | suceq 4362 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑧 → suc 𝑦 = suc 𝑧) |
45 | 43, 44 | syl8 71 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ω ∧
∀𝑧 ∈ ω
(𝑦 ≈ 𝑧 → 𝑦 = 𝑧)) → (𝑧 ∈ ω → (suc 𝑦 ≈ suc 𝑧 → suc 𝑦 = suc 𝑧))) |
46 | | breq2 3969 |
. . . . . . . . . . . . 13
⊢ (𝑤 = suc 𝑧 → (suc 𝑦 ≈ 𝑤 ↔ suc 𝑦 ≈ suc 𝑧)) |
47 | | eqeq2 2167 |
. . . . . . . . . . . . 13
⊢ (𝑤 = suc 𝑧 → (suc 𝑦 = 𝑤 ↔ suc 𝑦 = suc 𝑧)) |
48 | 46, 47 | imbi12d 233 |
. . . . . . . . . . . 12
⊢ (𝑤 = suc 𝑧 → ((suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤) ↔ (suc 𝑦 ≈ suc 𝑧 → suc 𝑦 = suc 𝑧))) |
49 | 48 | biimprcd 159 |
. . . . . . . . . . 11
⊢ ((suc
𝑦 ≈ suc 𝑧 → suc 𝑦 = suc 𝑧) → (𝑤 = suc 𝑧 → (suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤))) |
50 | 45, 49 | syl6 33 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ω ∧
∀𝑧 ∈ ω
(𝑦 ≈ 𝑧 → 𝑦 = 𝑧)) → (𝑧 ∈ ω → (𝑤 = suc 𝑧 → (suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤)))) |
51 | 33, 34, 50 | rexlimd 2571 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ω ∧
∀𝑧 ∈ ω
(𝑦 ≈ 𝑧 → 𝑦 = 𝑧)) → (∃𝑧 ∈ ω 𝑤 = suc 𝑧 → (suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤))) |
52 | 30, 51 | jaod 707 |
. . . . . . . 8
⊢ ((𝑦 ∈ ω ∧
∀𝑧 ∈ ω
(𝑦 ≈ 𝑧 → 𝑦 = 𝑧)) → ((𝑤 = ∅ ∨ ∃𝑧 ∈ ω 𝑤 = suc 𝑧) → (suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤))) |
53 | 52 | ex 114 |
. . . . . . 7
⊢ (𝑦 ∈ ω →
(∀𝑧 ∈ ω
(𝑦 ≈ 𝑧 → 𝑦 = 𝑧) → ((𝑤 = ∅ ∨ ∃𝑧 ∈ ω 𝑤 = suc 𝑧) → (suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤)))) |
54 | 23, 53 | syl7 69 |
. . . . . 6
⊢ (𝑦 ∈ ω →
(∀𝑧 ∈ ω
(𝑦 ≈ 𝑧 → 𝑦 = 𝑧) → (𝑤 ∈ ω → (suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤)))) |
55 | 54 | ralrimdv 2536 |
. . . . 5
⊢ (𝑦 ∈ ω →
(∀𝑧 ∈ ω
(𝑦 ≈ 𝑧 → 𝑦 = 𝑧) → ∀𝑤 ∈ ω (suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤))) |
56 | | breq2 3969 |
. . . . . . 7
⊢ (𝑤 = 𝑧 → (suc 𝑦 ≈ 𝑤 ↔ suc 𝑦 ≈ 𝑧)) |
57 | | eqeq2 2167 |
. . . . . . 7
⊢ (𝑤 = 𝑧 → (suc 𝑦 = 𝑤 ↔ suc 𝑦 = 𝑧)) |
58 | 56, 57 | imbi12d 233 |
. . . . . 6
⊢ (𝑤 = 𝑧 → ((suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤) ↔ (suc 𝑦 ≈ 𝑧 → suc 𝑦 = 𝑧))) |
59 | 58 | cbvralv 2680 |
. . . . 5
⊢
(∀𝑤 ∈
ω (suc 𝑦 ≈
𝑤 → suc 𝑦 = 𝑤) ↔ ∀𝑧 ∈ ω (suc 𝑦 ≈ 𝑧 → suc 𝑦 = 𝑧)) |
60 | 55, 59 | syl6ib 160 |
. . . 4
⊢ (𝑦 ∈ ω →
(∀𝑧 ∈ ω
(𝑦 ≈ 𝑧 → 𝑦 = 𝑧) → ∀𝑧 ∈ ω (suc 𝑦 ≈ 𝑧 → suc 𝑦 = 𝑧))) |
61 | 4, 8, 12, 16, 22, 60 | finds 4558 |
. . 3
⊢ (𝐴 ∈ ω →
∀𝑧 ∈ ω
(𝐴 ≈ 𝑧 → 𝐴 = 𝑧)) |
62 | | breq2 3969 |
. . . . 5
⊢ (𝑧 = 𝐵 → (𝐴 ≈ 𝑧 ↔ 𝐴 ≈ 𝐵)) |
63 | | eqeq2 2167 |
. . . . 5
⊢ (𝑧 = 𝐵 → (𝐴 = 𝑧 ↔ 𝐴 = 𝐵)) |
64 | 62, 63 | imbi12d 233 |
. . . 4
⊢ (𝑧 = 𝐵 → ((𝐴 ≈ 𝑧 → 𝐴 = 𝑧) ↔ (𝐴 ≈ 𝐵 → 𝐴 = 𝐵))) |
65 | 64 | rspcv 2812 |
. . 3
⊢ (𝐵 ∈ ω →
(∀𝑧 ∈ ω
(𝐴 ≈ 𝑧 → 𝐴 = 𝑧) → (𝐴 ≈ 𝐵 → 𝐴 = 𝐵))) |
66 | 61, 65 | mpan9 279 |
. 2
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ≈ 𝐵 → 𝐴 = 𝐵)) |
67 | | eqeng 6708 |
. . 3
⊢ (𝐴 ∈ ω → (𝐴 = 𝐵 → 𝐴 ≈ 𝐵)) |
68 | 67 | adantr 274 |
. 2
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 = 𝐵 → 𝐴 ≈ 𝐵)) |
69 | 66, 68 | impbid 128 |
1
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ≈ 𝐵 ↔ 𝐴 = 𝐵)) |