Metamath Proof Explorer

Theorem nneneqOLD

Description: Obsolete version of nneneq as of 11-Nov-2024. (Contributed by NM, 28-May-1998) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion nneneqOLD ⊢ A ∈ ω ∧ B ∈ ω → A ≈ B ↔ A = B

Proof

Step Hyp Ref Expression
1 breq1 ⊢ x = ∅ → x ≈ z ↔ ∅ ≈ z
2 eqeq1 ⊢ x = ∅ → x = z ↔ ∅ = z
3 1 2 imbi12d ⊢ x = ∅ → x ≈ z → x = z ↔ ∅ ≈ z → ∅ = z
4 3 ralbidv ⊢ x = ∅ → ∀ z ∈ ω x ≈ z → x = z ↔ ∀ z ∈ ω ∅ ≈ z → ∅ = z
5 breq1 ⊢ x = y → x ≈ z ↔ y ≈ z
6 eqeq1 ⊢ x = y → x = z ↔ y = z
7 5 6 imbi12d ⊢ x = y → x ≈ z → x = z ↔ y ≈ z → y = z
8 7 ralbidv ⊢ x = y → ∀ z ∈ ω x ≈ z → x = z ↔ ∀ z ∈ ω y ≈ z → y = z
9 breq1 ⊢ x = suc ⁡ y → x ≈ z ↔ suc ⁡ y ≈ z
10 eqeq1 ⊢ x = suc ⁡ y → x = z ↔ suc ⁡ y = z
11 9 10 imbi12d ⊢ x = suc ⁡ y → x ≈ z → x = z ↔ suc ⁡ y ≈ z → suc ⁡ y = z
12 11 ralbidv ⊢ x = suc ⁡ y → ∀ z ∈ ω x ≈ z → x = z ↔ ∀ z ∈ ω suc ⁡ y ≈ z → suc ⁡ y = z
13 breq1 ⊢ x = A → x ≈ z ↔ A ≈ z
14 eqeq1 ⊢ x = A → x = z ↔ A = z
15 13 14 imbi12d ⊢ x = A → x ≈ z → x = z ↔ A ≈ z → A = z
16 15 ralbidv ⊢ x = A → ∀ z ∈ ω x ≈ z → x = z ↔ ∀ z ∈ ω A ≈ z → A = z
17 ensym ⊢ ∅ ≈ z → z ≈ ∅
18 en0 ⊢ z ≈ ∅ ↔ z = ∅
19 eqcom ⊢ z = ∅ ↔ ∅ = z
20 18 19 bitri ⊢ z ≈ ∅ ↔ ∅ = z
21 17 20 sylib ⊢ ∅ ≈ z → ∅ = z
22 21 rgenw ⊢ ∀ z ∈ ω ∅ ≈ z → ∅ = z
23 nn0suc ⊢ w ∈ ω → w = ∅ ∨ ∃ z ∈ ω w = suc ⁡ z
24 en0 ⊢ suc ⁡ y ≈ ∅ ↔ suc ⁡ y = ∅
25 breq2 ⊢ w = ∅ → suc ⁡ y ≈ w ↔ suc ⁡ y ≈ ∅
26 eqeq2 ⊢ w = ∅ → suc ⁡ y = w ↔ suc ⁡ y = ∅
27 25 26 bibi12d ⊢ w = ∅ → suc ⁡ y ≈ w ↔ suc ⁡ y = w ↔ suc ⁡ y ≈ ∅ ↔ suc ⁡ y = ∅
28 24 27 mpbiri ⊢ w = ∅ → suc ⁡ y ≈ w ↔ suc ⁡ y = w
29 28 biimpd ⊢ w = ∅ → suc ⁡ y ≈ w → suc ⁡ y = w
30 29 a1i ⊢ y ∈ ω ∧ ∀ z ∈ ω y ≈ z → y = z → w = ∅ → suc ⁡ y ≈ w → suc ⁡ y = w
31 nfv ⊢ Ⅎ z y ∈ ω
32 nfra1 ⊢ Ⅎ z ∀ z ∈ ω y ≈ z → y = z
33 31 32 nfan ⊢ Ⅎ z y ∈ ω ∧ ∀ z ∈ ω y ≈ z → y = z
34 nfv ⊢ Ⅎ z suc ⁡ y ≈ w → suc ⁡ y = w
35 vex ⊢ y ∈ V
36 vex ⊢ z ∈ V
37 35 36 phplem4OLD ⊢ y ∈ ω ∧ z ∈ ω → suc ⁡ y ≈ suc ⁡ z → y ≈ z
38 37 imim1d ⊢ y ∈ ω ∧ z ∈ ω → y ≈ z → y = z → suc ⁡ y ≈ suc ⁡ z → y = z
39 38 ex ⊢ y ∈ ω → z ∈ ω → y ≈ z → y = z → suc ⁡ y ≈ suc ⁡ z → y = z
40 39 a2d ⊢ y ∈ ω → z ∈ ω → y ≈ z → y = z → z ∈ ω → suc ⁡ y ≈ suc ⁡ z → y = z
41 rsp ⊢ ∀ z ∈ ω y ≈ z → y = z → z ∈ ω → y ≈ z → y = z
42 40 41 impel ⊢ y ∈ ω ∧ ∀ z ∈ ω y ≈ z → y = z → z ∈ ω → suc ⁡ y ≈ suc ⁡ z → y = z
43 suceq ⊢ y = z → suc ⁡ y = suc ⁡ z
44 42 43 syl8 ⊢ y ∈ ω ∧ ∀ z ∈ ω y ≈ z → y = z → z ∈ ω → suc ⁡ y ≈ suc ⁡ z → suc ⁡ y = suc ⁡ z
45 breq2 ⊢ w = suc ⁡ z → suc ⁡ y ≈ w ↔ suc ⁡ y ≈ suc ⁡ z
46 eqeq2 ⊢ w = suc ⁡ z → suc ⁡ y = w ↔ suc ⁡ y = suc ⁡ z
47 45 46 imbi12d ⊢ w = suc ⁡ z → suc ⁡ y ≈ w → suc ⁡ y = w ↔ suc ⁡ y ≈ suc ⁡ z → suc ⁡ y = suc ⁡ z
48 47 biimprcd ⊢ suc ⁡ y ≈ suc ⁡ z → suc ⁡ y = suc ⁡ z → w = suc ⁡ z → suc ⁡ y ≈ w → suc ⁡ y = w
49 44 48 syl6 ⊢ y ∈ ω ∧ ∀ z ∈ ω y ≈ z → y = z → z ∈ ω → w = suc ⁡ z → suc ⁡ y ≈ w → suc ⁡ y = w
50 33 34 49 rexlimd ⊢ y ∈ ω ∧ ∀ z ∈ ω y ≈ z → y = z → ∃ z ∈ ω w = suc ⁡ z → suc ⁡ y ≈ w → suc ⁡ y = w
51 30 50 jaod ⊢ y ∈ ω ∧ ∀ z ∈ ω y ≈ z → y = z → w = ∅ ∨ ∃ z ∈ ω w = suc ⁡ z → suc ⁡ y ≈ w → suc ⁡ y = w
52 51 ex ⊢ y ∈ ω → ∀ z ∈ ω y ≈ z → y = z → w = ∅ ∨ ∃ z ∈ ω w = suc ⁡ z → suc ⁡ y ≈ w → suc ⁡ y = w
53 23 52 syl7 ⊢ y ∈ ω → ∀ z ∈ ω y ≈ z → y = z → w ∈ ω → suc ⁡ y ≈ w → suc ⁡ y = w
54 53 ralrimdv ⊢ y ∈ ω → ∀ z ∈ ω y ≈ z → y = z → ∀ w ∈ ω suc ⁡ y ≈ w → suc ⁡ y = w
55 breq2 ⊢ w = z → suc ⁡ y ≈ w ↔ suc ⁡ y ≈ z
56 eqeq2 ⊢ w = z → suc ⁡ y = w ↔ suc ⁡ y = z
57 55 56 imbi12d ⊢ w = z → suc ⁡ y ≈ w → suc ⁡ y = w ↔ suc ⁡ y ≈ z → suc ⁡ y = z
58 57 cbvralvw ⊢ ∀ w ∈ ω suc ⁡ y ≈ w → suc ⁡ y = w ↔ ∀ z ∈ ω suc ⁡ y ≈ z → suc ⁡ y = z
59 54 58 imbitrdi ⊢ y ∈ ω → ∀ z ∈ ω y ≈ z → y = z → ∀ z ∈ ω suc ⁡ y ≈ z → suc ⁡ y = z
60 4 8 12 16 22 59 finds ⊢ A ∈ ω → ∀ z ∈ ω A ≈ z → A = z
61 breq2 ⊢ z = B → A ≈ z ↔ A ≈ B
62 eqeq2 ⊢ z = B → A = z ↔ A = B
63 61 62 imbi12d ⊢ z = B → A ≈ z → A = z ↔ A ≈ B → A = B
64 63 rspcv ⊢ B ∈ ω → ∀ z ∈ ω A ≈ z → A = z → A ≈ B → A = B
65 60 64 mpan9 ⊢ A ∈ ω ∧ B ∈ ω → A ≈ B → A = B
66 eqeng ⊢ A ∈ ω → A = B → A ≈ B
67 66 adantr ⊢ A ∈ ω ∧ B ∈ ω → A = B → A ≈ B
68 65 67 impbid ⊢ A ∈ ω ∧ B ∈ ω → A ≈ B ↔ A = B