Metamath Proof Explorer

Theorem bnj1098

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypothesis bnj1098.1 
|- D = ( _om \ { (/) } )
Assertion bnj1098 
|- E. j ( ( i =/= (/) /\ i e. n /\ n e. D ) -> ( j e. n /\ i = suc j ) )

Proof

Step Hyp Ref Expression
1 bnj1098.1 
 |-  D = ( _om \ { (/) } )
2 3anrev 
 |-  ( ( i =/= (/) /\ i e. n /\ n e. D ) <-> ( n e. D /\ i e. n /\ i =/= (/) ) )
3 df-3an 
 |-  ( ( n e. D /\ i e. n /\ i =/= (/) ) <-> ( ( n e. D /\ i e. n ) /\ i =/= (/) ) )
4 2 3 bitri 
 |-  ( ( i =/= (/) /\ i e. n /\ n e. D ) <-> ( ( n e. D /\ i e. n ) /\ i =/= (/) ) )
5 simpr 
 |-  ( ( n e. D /\ i e. n ) -> i e. n )
6 1 bnj923 
 |-  ( n e. D -> n e. _om )
7 6 adantr 
 |-  ( ( n e. D /\ i e. n ) -> n e. _om )
8 elnn 
 |-  ( ( i e. n /\ n e. _om ) -> i e. _om )
9 5 7 8 syl2anc 
 |-  ( ( n e. D /\ i e. n ) -> i e. _om )
10 9 anim1i 
 |-  ( ( ( n e. D /\ i e. n ) /\ i =/= (/) ) -> ( i e. _om /\ i =/= (/) ) )
11 4 10 sylbi 
 |-  ( ( i =/= (/) /\ i e. n /\ n e. D ) -> ( i e. _om /\ i =/= (/) ) )
12 nnsuc 
 |-  ( ( i e. _om /\ i =/= (/) ) -> E. j e. _om i = suc j )
13 11 12 syl 
 |-  ( ( i =/= (/) /\ i e. n /\ n e. D ) -> E. j e. _om i = suc j )
14 df-rex 
 |-  ( E. j e. _om i = suc j <-> E. j ( j e. _om /\ i = suc j ) )
15 14 imbi2i 
 |-  ( ( ( i =/= (/) /\ i e. n /\ n e. D ) -> E. j e. _om i = suc j ) <-> ( ( i =/= (/) /\ i e. n /\ n e. D ) -> E. j ( j e. _om /\ i = suc j ) ) )
16 19.37v 
 |-  ( E. j ( ( i =/= (/) /\ i e. n /\ n e. D ) -> ( j e. _om /\ i = suc j ) ) <-> ( ( i =/= (/) /\ i e. n /\ n e. D ) -> E. j ( j e. _om /\ i = suc j ) ) )
17 15 16 bitr4i 
 |-  ( ( ( i =/= (/) /\ i e. n /\ n e. D ) -> E. j e. _om i = suc j ) <-> E. j ( ( i =/= (/) /\ i e. n /\ n e. D ) -> ( j e. _om /\ i = suc j ) ) )
18 13 17 mpbi 
 |-  E. j ( ( i =/= (/) /\ i e. n /\ n e. D ) -> ( j e. _om /\ i = suc j ) )
19 ancr 
 |-  ( ( ( i =/= (/) /\ i e. n /\ n e. D ) -> ( j e. _om /\ i = suc j ) ) -> ( ( i =/= (/) /\ i e. n /\ n e. D ) -> ( ( j e. _om /\ i = suc j ) /\ ( i =/= (/) /\ i e. n /\ n e. D ) ) ) )
20 18 19 bnj101 
 |-  E. j ( ( i =/= (/) /\ i e. n /\ n e. D ) -> ( ( j e. _om /\ i = suc j ) /\ ( i =/= (/) /\ i e. n /\ n e. D ) ) )
21 vex 
 |-  j e. _V
22 21 bnj216 
 |-  ( i = suc j -> j e. i )
23 22 ad2antlr 
 |-  ( ( ( j e. _om /\ i = suc j ) /\ ( i =/= (/) /\ i e. n /\ n e. D ) ) -> j e. i )
24 simpr2 
 |-  ( ( ( j e. _om /\ i = suc j ) /\ ( i =/= (/) /\ i e. n /\ n e. D ) ) -> i e. n )
25 3simpc 
 |-  ( ( i =/= (/) /\ i e. n /\ n e. D ) -> ( i e. n /\ n e. D ) )
26 25 ancomd 
 |-  ( ( i =/= (/) /\ i e. n /\ n e. D ) -> ( n e. D /\ i e. n ) )
27 26 adantl 
 |-  ( ( ( j e. _om /\ i = suc j ) /\ ( i =/= (/) /\ i e. n /\ n e. D ) ) -> ( n e. D /\ i e. n ) )
28 nnord 
 |-  ( n e. _om -> Ord n )
29 ordtr1 
 |-  ( Ord n -> ( ( j e. i /\ i e. n ) -> j e. n ) )
30 27 7 28 29 4syl 
 |-  ( ( ( j e. _om /\ i = suc j ) /\ ( i =/= (/) /\ i e. n /\ n e. D ) ) -> ( ( j e. i /\ i e. n ) -> j e. n ) )
31 23 24 30 mp2and 
 |-  ( ( ( j e. _om /\ i = suc j ) /\ ( i =/= (/) /\ i e. n /\ n e. D ) ) -> j e. n )
32 simplr 
 |-  ( ( ( j e. _om /\ i = suc j ) /\ ( i =/= (/) /\ i e. n /\ n e. D ) ) -> i = suc j )
33 31 32 jca 
 |-  ( ( ( j e. _om /\ i = suc j ) /\ ( i =/= (/) /\ i e. n /\ n e. D ) ) -> ( j e. n /\ i = suc j ) )
34 20 33 bnj1023 
 |-  E. j ( ( i =/= (/) /\ i e. n /\ n e. D ) -> ( j e. n /\ i = suc j ) )