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 = ( _om \ { (/) } )
Assertion bnj168 
|- ( ( n =/= 1o /\ n e. D ) -> E. m e. D n = suc m )

Proof

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