Metamath Proof Explorer


Theorem bnj168

Description: First-order logic and set theory. Revised to remove dependence on ax-reg . (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (Revised by NM, 21-Dec-2016) (New usage is discouraged.)

Ref Expression
Hypothesis bnj168.1 D = ω
Assertion bnj168 n 1 𝑜 n D m D n = suc m

Proof

Step Hyp Ref Expression
1 bnj168.1 D = ω
2 1 bnj158 n D m ω n = suc m
3 2 anim2i n 1 𝑜 n D n 1 𝑜 m ω n = suc m
4 r19.42v m ω n 1 𝑜 n = suc m n 1 𝑜 m ω n = suc m
5 3 4 sylibr n 1 𝑜 n D m ω n 1 𝑜 n = suc m
6 neeq1 n = suc m n 1 𝑜 suc m 1 𝑜
7 6 biimpac n 1 𝑜 n = suc m suc m 1 𝑜
8 df-1o 1 𝑜 = suc
9 8 eqeq2i suc m = 1 𝑜 suc m = suc
10 nnon m ω m On
11 0elon On
12 suc11 m On On suc m = suc m =
13 10 11 12 sylancl m ω suc m = suc m =
14 9 13 bitr2id m ω m = suc m = 1 𝑜
15 14 necon3bid m ω m suc m 1 𝑜
16 7 15 syl5ibr m ω n 1 𝑜 n = suc m m
17 16 ancld m ω n 1 𝑜 n = suc m n 1 𝑜 n = suc m m
18 17 reximia m ω n 1 𝑜 n = suc m m ω n 1 𝑜 n = suc m m
19 5 18 syl n 1 𝑜 n D m ω n 1 𝑜 n = suc m m
20 anass n 1 𝑜 n = suc m m n 1 𝑜 n = suc m m
21 20 rexbii m ω n 1 𝑜 n = suc m m m ω n 1 𝑜 n = suc m m
22 19 21 sylib n 1 𝑜 n D m ω n 1 𝑜 n = suc m m
23 simpr n 1 𝑜 n = suc m m n = suc m m
24 22 23 bnj31 n 1 𝑜 n D m ω n = suc m m
25 df-rex m ω n = suc m m m m ω n = suc m m
26 24 25 sylib n 1 𝑜 n D m m ω n = suc m m
27 simpr n = suc m m m
28 27 anim2i m ω n = suc m m m ω m
29 1 eleq2i m D m ω
30 eldifsn m ω m ω m
31 29 30 bitr2i m ω m m D
32 28 31 sylib m ω n = suc m m m D
33 simprl m ω n = suc m m n = suc m
34 32 33 jca m ω n = suc m m m D n = suc m
35 34 eximi m m ω n = suc m m m m D n = suc m
36 26 35 syl n 1 𝑜 n D m m D n = suc m
37 df-rex m D n = suc m m m D n = suc m
38 36 37 sylibr n 1 𝑜 n D m D n = suc m