Step | Hyp | Ref
| Expression |
1 | | breq1 5056 |
. . . . . 6
⊢ (𝑥 = ∅ → (𝑥 ≈ 𝑧 ↔ ∅ ≈ 𝑧)) |
2 | | eqeq1 2741 |
. . . . . 6
⊢ (𝑥 = ∅ → (𝑥 = 𝑧 ↔ ∅ = 𝑧)) |
3 | 1, 2 | imbi12d 348 |
. . . . 5
⊢ (𝑥 = ∅ → ((𝑥 ≈ 𝑧 → 𝑥 = 𝑧) ↔ (∅ ≈ 𝑧 → ∅ = 𝑧))) |
4 | 3 | ralbidv 3118 |
. . . 4
⊢ (𝑥 = ∅ → (∀𝑧 ∈ ω (𝑥 ≈ 𝑧 → 𝑥 = 𝑧) ↔ ∀𝑧 ∈ ω (∅ ≈ 𝑧 → ∅ = 𝑧))) |
5 | | breq1 5056 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑥 ≈ 𝑧 ↔ 𝑦 ≈ 𝑧)) |
6 | | eqeq1 2741 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑧 ↔ 𝑦 = 𝑧)) |
7 | 5, 6 | imbi12d 348 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝑥 ≈ 𝑧 → 𝑥 = 𝑧) ↔ (𝑦 ≈ 𝑧 → 𝑦 = 𝑧))) |
8 | 7 | ralbidv 3118 |
. . . 4
⊢ (𝑥 = 𝑦 → (∀𝑧 ∈ ω (𝑥 ≈ 𝑧 → 𝑥 = 𝑧) ↔ ∀𝑧 ∈ ω (𝑦 ≈ 𝑧 → 𝑦 = 𝑧))) |
9 | | breq1 5056 |
. . . . . 6
⊢ (𝑥 = suc 𝑦 → (𝑥 ≈ 𝑧 ↔ suc 𝑦 ≈ 𝑧)) |
10 | | eqeq1 2741 |
. . . . . 6
⊢ (𝑥 = suc 𝑦 → (𝑥 = 𝑧 ↔ suc 𝑦 = 𝑧)) |
11 | 9, 10 | imbi12d 348 |
. . . . 5
⊢ (𝑥 = suc 𝑦 → ((𝑥 ≈ 𝑧 → 𝑥 = 𝑧) ↔ (suc 𝑦 ≈ 𝑧 → suc 𝑦 = 𝑧))) |
12 | 11 | ralbidv 3118 |
. . . 4
⊢ (𝑥 = suc 𝑦 → (∀𝑧 ∈ ω (𝑥 ≈ 𝑧 → 𝑥 = 𝑧) ↔ ∀𝑧 ∈ ω (suc 𝑦 ≈ 𝑧 → suc 𝑦 = 𝑧))) |
13 | | breq1 5056 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (𝑥 ≈ 𝑧 ↔ 𝐴 ≈ 𝑧)) |
14 | | eqeq1 2741 |
. . . . . 6
⊢ (𝑥 = 𝐴 → (𝑥 = 𝑧 ↔ 𝐴 = 𝑧)) |
15 | 13, 14 | imbi12d 348 |
. . . . 5
⊢ (𝑥 = 𝐴 → ((𝑥 ≈ 𝑧 → 𝑥 = 𝑧) ↔ (𝐴 ≈ 𝑧 → 𝐴 = 𝑧))) |
16 | 15 | ralbidv 3118 |
. . . 4
⊢ (𝑥 = 𝐴 → (∀𝑧 ∈ ω (𝑥 ≈ 𝑧 → 𝑥 = 𝑧) ↔ ∀𝑧 ∈ ω (𝐴 ≈ 𝑧 → 𝐴 = 𝑧))) |
17 | | ensym 8677 |
. . . . . 6
⊢ (∅
≈ 𝑧 → 𝑧 ≈
∅) |
18 | | en0 8691 |
. . . . . . 7
⊢ (𝑧 ≈ ∅ ↔ 𝑧 = ∅) |
19 | | eqcom 2744 |
. . . . . . 7
⊢ (𝑧 = ∅ ↔ ∅ =
𝑧) |
20 | 18, 19 | bitri 278 |
. . . . . 6
⊢ (𝑧 ≈ ∅ ↔ ∅
= 𝑧) |
21 | 17, 20 | sylib 221 |
. . . . 5
⊢ (∅
≈ 𝑧 → ∅ =
𝑧) |
22 | 21 | rgenw 3073 |
. . . 4
⊢
∀𝑧 ∈
ω (∅ ≈ 𝑧
→ ∅ = 𝑧) |
23 | | nn0suc 7673 |
. . . . . . 7
⊢ (𝑤 ∈ ω → (𝑤 = ∅ ∨ ∃𝑧 ∈ ω 𝑤 = suc 𝑧)) |
24 | | en0 8691 |
. . . . . . . . . . . 12
⊢ (suc
𝑦 ≈ ∅ ↔
suc 𝑦 =
∅) |
25 | | breq2 5057 |
. . . . . . . . . . . . 13
⊢ (𝑤 = ∅ → (suc 𝑦 ≈ 𝑤 ↔ suc 𝑦 ≈ ∅)) |
26 | | eqeq2 2749 |
. . . . . . . . . . . . 13
⊢ (𝑤 = ∅ → (suc 𝑦 = 𝑤 ↔ suc 𝑦 = ∅)) |
27 | 25, 26 | bibi12d 349 |
. . . . . . . . . . . 12
⊢ (𝑤 = ∅ → ((suc 𝑦 ≈ 𝑤 ↔ suc 𝑦 = 𝑤) ↔ (suc 𝑦 ≈ ∅ ↔ suc 𝑦 = ∅))) |
28 | 24, 27 | mpbiri 261 |
. . . . . . . . . . 11
⊢ (𝑤 = ∅ → (suc 𝑦 ≈ 𝑤 ↔ suc 𝑦 = 𝑤)) |
29 | 28 | biimpd 232 |
. . . . . . . . . 10
⊢ (𝑤 = ∅ → (suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤)) |
30 | 29 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ω ∧
∀𝑧 ∈ ω
(𝑦 ≈ 𝑧 → 𝑦 = 𝑧)) → (𝑤 = ∅ → (suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤))) |
31 | | nfv 1922 |
. . . . . . . . . . 11
⊢
Ⅎ𝑧 𝑦 ∈ ω |
32 | | nfra1 3140 |
. . . . . . . . . . 11
⊢
Ⅎ𝑧∀𝑧 ∈ ω (𝑦 ≈ 𝑧 → 𝑦 = 𝑧) |
33 | 31, 32 | nfan 1907 |
. . . . . . . . . 10
⊢
Ⅎ𝑧(𝑦 ∈ ω ∧
∀𝑧 ∈ ω
(𝑦 ≈ 𝑧 → 𝑦 = 𝑧)) |
34 | | nfv 1922 |
. . . . . . . . . 10
⊢
Ⅎ𝑧(suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤) |
35 | | vex 3412 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑦 ∈ V |
36 | | vex 3412 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑧 ∈ V |
37 | 35, 36 | phplem4 8828 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ω ∧ 𝑧 ∈ ω) → (suc
𝑦 ≈ suc 𝑧 → 𝑦 ≈ 𝑧)) |
38 | 37 | imim1d 82 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ω ∧ 𝑧 ∈ ω) → ((𝑦 ≈ 𝑧 → 𝑦 = 𝑧) → (suc 𝑦 ≈ suc 𝑧 → 𝑦 = 𝑧))) |
39 | 38 | ex 416 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ω → (𝑧 ∈ ω → ((𝑦 ≈ 𝑧 → 𝑦 = 𝑧) → (suc 𝑦 ≈ suc 𝑧 → 𝑦 = 𝑧)))) |
40 | 39 | a2d 29 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ω → ((𝑧 ∈ ω → (𝑦 ≈ 𝑧 → 𝑦 = 𝑧)) → (𝑧 ∈ ω → (suc 𝑦 ≈ suc 𝑧 → 𝑦 = 𝑧)))) |
41 | | rsp 3127 |
. . . . . . . . . . . . 13
⊢
(∀𝑧 ∈
ω (𝑦 ≈ 𝑧 → 𝑦 = 𝑧) → (𝑧 ∈ ω → (𝑦 ≈ 𝑧 → 𝑦 = 𝑧))) |
42 | 40, 41 | impel 509 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ω ∧
∀𝑧 ∈ ω
(𝑦 ≈ 𝑧 → 𝑦 = 𝑧)) → (𝑧 ∈ ω → (suc 𝑦 ≈ suc 𝑧 → 𝑦 = 𝑧))) |
43 | | suceq 6278 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑧 → suc 𝑦 = suc 𝑧) |
44 | 42, 43 | syl8 76 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ω ∧
∀𝑧 ∈ ω
(𝑦 ≈ 𝑧 → 𝑦 = 𝑧)) → (𝑧 ∈ ω → (suc 𝑦 ≈ suc 𝑧 → suc 𝑦 = suc 𝑧))) |
45 | | breq2 5057 |
. . . . . . . . . . . . 13
⊢ (𝑤 = suc 𝑧 → (suc 𝑦 ≈ 𝑤 ↔ suc 𝑦 ≈ suc 𝑧)) |
46 | | eqeq2 2749 |
. . . . . . . . . . . . 13
⊢ (𝑤 = suc 𝑧 → (suc 𝑦 = 𝑤 ↔ suc 𝑦 = suc 𝑧)) |
47 | 45, 46 | imbi12d 348 |
. . . . . . . . . . . 12
⊢ (𝑤 = suc 𝑧 → ((suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤) ↔ (suc 𝑦 ≈ suc 𝑧 → suc 𝑦 = suc 𝑧))) |
48 | 47 | biimprcd 253 |
. . . . . . . . . . 11
⊢ ((suc
𝑦 ≈ suc 𝑧 → suc 𝑦 = suc 𝑧) → (𝑤 = suc 𝑧 → (suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤))) |
49 | 44, 48 | syl6 35 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ω ∧
∀𝑧 ∈ ω
(𝑦 ≈ 𝑧 → 𝑦 = 𝑧)) → (𝑧 ∈ ω → (𝑤 = suc 𝑧 → (suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤)))) |
50 | 33, 34, 49 | rexlimd 3236 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ω ∧
∀𝑧 ∈ ω
(𝑦 ≈ 𝑧 → 𝑦 = 𝑧)) → (∃𝑧 ∈ ω 𝑤 = suc 𝑧 → (suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤))) |
51 | 30, 50 | jaod 859 |
. . . . . . . 8
⊢ ((𝑦 ∈ ω ∧
∀𝑧 ∈ ω
(𝑦 ≈ 𝑧 → 𝑦 = 𝑧)) → ((𝑤 = ∅ ∨ ∃𝑧 ∈ ω 𝑤 = suc 𝑧) → (suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤))) |
52 | 51 | ex 416 |
. . . . . . 7
⊢ (𝑦 ∈ ω →
(∀𝑧 ∈ ω
(𝑦 ≈ 𝑧 → 𝑦 = 𝑧) → ((𝑤 = ∅ ∨ ∃𝑧 ∈ ω 𝑤 = suc 𝑧) → (suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤)))) |
53 | 23, 52 | syl7 74 |
. . . . . 6
⊢ (𝑦 ∈ ω →
(∀𝑧 ∈ ω
(𝑦 ≈ 𝑧 → 𝑦 = 𝑧) → (𝑤 ∈ ω → (suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤)))) |
54 | 53 | ralrimdv 3109 |
. . . . 5
⊢ (𝑦 ∈ ω →
(∀𝑧 ∈ ω
(𝑦 ≈ 𝑧 → 𝑦 = 𝑧) → ∀𝑤 ∈ ω (suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤))) |
55 | | breq2 5057 |
. . . . . . 7
⊢ (𝑤 = 𝑧 → (suc 𝑦 ≈ 𝑤 ↔ suc 𝑦 ≈ 𝑧)) |
56 | | eqeq2 2749 |
. . . . . . 7
⊢ (𝑤 = 𝑧 → (suc 𝑦 = 𝑤 ↔ suc 𝑦 = 𝑧)) |
57 | 55, 56 | imbi12d 348 |
. . . . . 6
⊢ (𝑤 = 𝑧 → ((suc 𝑦 ≈ 𝑤 → suc 𝑦 = 𝑤) ↔ (suc 𝑦 ≈ 𝑧 → suc 𝑦 = 𝑧))) |
58 | 57 | cbvralvw 3358 |
. . . . 5
⊢
(∀𝑤 ∈
ω (suc 𝑦 ≈
𝑤 → suc 𝑦 = 𝑤) ↔ ∀𝑧 ∈ ω (suc 𝑦 ≈ 𝑧 → suc 𝑦 = 𝑧)) |
59 | 54, 58 | syl6ib 254 |
. . . 4
⊢ (𝑦 ∈ ω →
(∀𝑧 ∈ ω
(𝑦 ≈ 𝑧 → 𝑦 = 𝑧) → ∀𝑧 ∈ ω (suc 𝑦 ≈ 𝑧 → suc 𝑦 = 𝑧))) |
60 | 4, 8, 12, 16, 22, 59 | finds 7676 |
. . 3
⊢ (𝐴 ∈ ω →
∀𝑧 ∈ ω
(𝐴 ≈ 𝑧 → 𝐴 = 𝑧)) |
61 | | breq2 5057 |
. . . . 5
⊢ (𝑧 = 𝐵 → (𝐴 ≈ 𝑧 ↔ 𝐴 ≈ 𝐵)) |
62 | | eqeq2 2749 |
. . . . 5
⊢ (𝑧 = 𝐵 → (𝐴 = 𝑧 ↔ 𝐴 = 𝐵)) |
63 | 61, 62 | imbi12d 348 |
. . . 4
⊢ (𝑧 = 𝐵 → ((𝐴 ≈ 𝑧 → 𝐴 = 𝑧) ↔ (𝐴 ≈ 𝐵 → 𝐴 = 𝐵))) |
64 | 63 | rspcv 3532 |
. . 3
⊢ (𝐵 ∈ ω →
(∀𝑧 ∈ ω
(𝐴 ≈ 𝑧 → 𝐴 = 𝑧) → (𝐴 ≈ 𝐵 → 𝐴 = 𝐵))) |
65 | 60, 64 | mpan9 510 |
. 2
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ≈ 𝐵 → 𝐴 = 𝐵)) |
66 | | eqeng 8662 |
. . 3
⊢ (𝐴 ∈ ω → (𝐴 = 𝐵 → 𝐴 ≈ 𝐵)) |
67 | 66 | adantr 484 |
. 2
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 = 𝐵 → 𝐴 ≈ 𝐵)) |
68 | 65, 67 | impbid 215 |
1
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ ω) → (𝐴 ≈ 𝐵 ↔ 𝐴 = 𝐵)) |