Theorem bnj1098 29603

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

Hypothesis

Ref	Expression
bnj1098.1	|- D = ( om \ { (/) } )

Assertion

Ref	Expression
bnj1098	|- E. j ( ( i =/= (/) /\ i e. n /\ n e. D ) -> ( j e. n /\ i = suc j ) )

Distinct variable groups:   D, j   i, j   j, n

Allowed substitution hints:   D( i, n)

Proof of Theorem bnj1098

Step	Hyp	Ref	Expression
1		3anrev 993	. . . . . . 7 |- ( ( i =/= (/) /\ i e. n /\ n e. D ) <-> ( n e. D /\ i e. n /\ i =/= (/) ) )
2		df-3an 984	. . . . . . 7 |- ( ( n e. D /\ i e. n /\ i =/= (/) ) <-> ( ( n e. D /\ i e. n ) /\ i =/= (/) ) )
3	1, 2	bitri 252	. . . . . 6 |- ( ( i =/= (/) /\ i e. n /\ n e. D ) <-> ( ( n e. D /\ i e. n ) /\ i =/= (/) ) )
4		simpr 462	. . . . . . . 8 |- ( ( n e. D /\ i e. n ) -> i e. n )
5		bnj1098.1	. . . . . . . . . 10 |- D = ( om \ { (/) } )
6	5	bnj923 29587	. . . . . . . . 9 |- ( n e. D -> n e. om )
7	6	adantr 466	. . . . . . . 8 |- ( ( n e. D /\ i e. n ) -> n e. om )
8		elnn 6716	. . . . . . . 8 |- ( ( i e. n /\ n e. om ) -> i e. om )
9	4, 7, 8	syl2anc 665	. . . . . . 7 |- ( ( n e. D /\ i e. n ) -> i e. om )
10	9	anim1i 570	. . . . . 6 |- ( ( ( n e. D /\ i e. n ) /\ i =/= (/) ) -> ( i e. om /\ i =/= (/) ) )
11	3, 10	sylbi 198	. . . . 5 |- ( ( i =/= (/) /\ i e. n /\ n e. D ) -> ( i e. om /\ i =/= (/) ) )
12		nnsuc 6723	. . . . 5 |- ( ( i e. om /\ i =/= (/) ) -> E. j e. om i = suc j )
13	11, 12	syl 17	. . . 4 |- ( ( i =/= (/) /\ i e. n /\ n e. D ) -> E. j e. om i = suc j )
14		df-rex 2777	. . . . . 6 |- ( E. j e. om i = suc j <-> E. j ( j e. om /\ i = suc j ) )
15	14	imbi2i 313	. . . . 5 |- ( ( ( 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 1819	. . . . 5 |- ( 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 255	. . . 4 |- ( ( ( 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 211	. . 3 |- E. j ( ( i =/= (/) /\ i e. n /\ n e. D ) -> ( j e. om /\ i = suc j ) )
19		ancr 551	. . 3 |- ( ( ( 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 29537	. 2 |- E. j ( ( i =/= (/) /\ i e. n /\ n e. D ) -> ( ( j e. om /\ i = suc j ) /\ ( i =/= (/) /\ i e. n /\ n e. D ) ) )
21		vex 3083	. . . . . 6 |- j e. _V
22	21	bnj216 29548	. . . . 5 |- ( i = suc j -> j e. i )
23	22	ad2antlr 731	. . . 4 |- ( ( ( j e. om /\ i = suc j ) /\ ( i =/= (/) /\ i e. n /\ n e. D ) ) -> j e. i )
24		simpr2 1012	. . . 4 |- ( ( ( j e. om /\ i = suc j ) /\ ( i =/= (/) /\ i e. n /\ n e. D ) ) -> i e. n )
25		3simpc 1004	. . . . . . 7 |- ( ( i =/= (/) /\ i e. n /\ n e. D ) -> ( i e. n /\ n e. D ) )
26	25	ancomd 452	. . . . . 6 |- ( ( i =/= (/) /\ i e. n /\ n e. D ) -> ( n e. D /\ i e. n ) )
27	26	adantl 467	. . . . 5 |- ( ( ( j e. om /\ i = suc j ) /\ ( i =/= (/) /\ i e. n /\ n e. D ) ) -> ( n e. D /\ i e. n ) )
28		nnord 6714	. . . . 5 |- ( n e. om -> Ord n )
29		ordtr1 5485	. . . . 5 |- ( Ord n -> ( ( j e. i /\ i e. n ) -> j e. n ) )
30	27, 7, 28, 29	4syl 19	. . . 4 |- ( ( ( 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 683	. . 3 |- ( ( ( j e. om /\ i = suc j ) /\ ( i =/= (/) /\ i e. n /\ n e. D ) ) -> j e. n )
32		simplr 760	. . 3 |- ( ( ( j e. om /\ i = suc j ) /\ ( i =/= (/) /\ i e. n /\ n e. D ) ) -> i = suc j )
33	31, 32	jca 534	. 2 |- ( ( ( j e. om /\ i = suc j ) /\ ( i =/= (/) /\ i e. n /\ n e. D ) ) -> ( j e. n /\ i = suc j ) )
34	20, 33	bnj1023 29600	1 |- E. j ( ( i =/= (/) /\ i e. n /\ n e. D ) -> ( j e. n /\ i = suc j ) )

Syntax hints:   -> wi 4   /\ wa 370   /\ w3a 982   = wceq 1437   E.wex 1657   e. wcel 1872   =/= wne 2614   E.wrex 2772   \ cdif 3433   (/)c0 3761   {csn 3998   Ord word 5441   suc csuc 5444   omcom 6706

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pr 4660  ax-un 6597

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-rab 2780  df-v 3082  df-sbc 3300  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-tp 4003  df-op 4005  df-uni 4220  df-br 4424  df-opab 4483  df-tr 4519  df-eprel 4764  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-om 6707

This theorem is referenced by:  bnj1110  29799  bnj1128  29807  bnj1145  29810