Theorem bnj1098 29601

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 997	. . . . . . 7 |- ( ( i =/= (/) /\ i e. n /\ n e. D ) <-> ( n e. D /\ i e. n /\ i =/= (/) ) )
2		df-3an 988	. . . . . . 7 |- ( ( n e. D /\ i e. n /\ i =/= (/) ) <-> ( ( n e. D /\ i e. n ) /\ i =/= (/) ) )
3	1, 2	bitri 257	. . . . . 6 |- ( ( i =/= (/) /\ i e. n /\ n e. D ) <-> ( ( n e. D /\ i e. n ) /\ i =/= (/) ) )
4		simpr 467	. . . . . . . 8 |- ( ( n e. D /\ i e. n ) -> i e. n )
5		bnj1098.1	. . . . . . . . . 10 |- D = ( om \ { (/) } )
6	5	bnj923 29585	. . . . . . . . 9 |- ( n e. D -> n e. om )
7	6	adantr 471	. . . . . . . 8 |- ( ( n e. D /\ i e. n ) -> n e. om )
8		elnn 6690	. . . . . . . 8 |- ( ( i e. n /\ n e. om ) -> i e. om )
9	4, 7, 8	syl2anc 671	. . . . . . 7 |- ( ( n e. D /\ i e. n ) -> i e. om )
10	9	anim1i 576	. . . . . 6 |- ( ( ( n e. D /\ i e. n ) /\ i =/= (/) ) -> ( i e. om /\ i =/= (/) ) )
11	3, 10	sylbi 200	. . . . 5 |- ( ( i =/= (/) /\ i e. n /\ n e. D ) -> ( i e. om /\ i =/= (/) ) )
12		nnsuc 6697	. . . . 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 2743	. . . . . 6 |- ( E. j e. om i = suc j <-> E. j ( j e. om /\ i = suc j ) )
15	14	imbi2i 318	. . . . 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 1830	. . . . 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 260	. . . 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 213	. . 3 |- E. j ( ( i =/= (/) /\ i e. n /\ n e. D ) -> ( j e. om /\ i = suc j ) )
19		ancr 556	. . 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 29535	. 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 3016	. . . . . 6 |- j e. _V
22	21	bnj216 29546	. . . . 5 |- ( i = suc j -> j e. i )
23	22	ad2antlr 738	. . . 4 |- ( ( ( j e. om /\ i = suc j ) /\ ( i =/= (/) /\ i e. n /\ n e. D ) ) -> j e. i )
24		simpr2 1016	. . . 4 |- ( ( ( j e. om /\ i = suc j ) /\ ( i =/= (/) /\ i e. n /\ n e. D ) ) -> i e. n )
25		3simpc 1008	. . . . . . 7 |- ( ( i =/= (/) /\ i e. n /\ n e. D ) -> ( i e. n /\ n e. D ) )
26	25	ancomd 457	. . . . . 6 |- ( ( i =/= (/) /\ i e. n /\ n e. D ) -> ( n e. D /\ i e. n ) )
27	26	adantl 472	. . . . 5 |- ( ( ( j e. om /\ i = suc j ) /\ ( i =/= (/) /\ i e. n /\ n e. D ) ) -> ( n e. D /\ i e. n ) )
28		nnord 6688	. . . . 5 |- ( n e. om -> Ord n )
29		ordtr1 5445	. . . . 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 690	. . 3 |- ( ( ( j e. om /\ i = suc j ) /\ ( i =/= (/) /\ i e. n /\ n e. D ) ) -> j e. n )
32		simplr 767	. . 3 |- ( ( ( j e. om /\ i = suc j ) /\ ( i =/= (/) /\ i e. n /\ n e. D ) ) -> i = suc j )
33	31, 32	jca 539	. 2 |- ( ( ( j e. om /\ i = suc j ) /\ ( i =/= (/) /\ i e. n /\ n e. D ) ) -> ( j e. n /\ i = suc j ) )
34	20, 33	bnj1023 29598	1 |- E. j ( ( i =/= (/) /\ i e. n /\ n e. D ) -> ( j e. n /\ i = suc j ) )

Syntax hints:   -> wi 4   /\ wa 375   /\ w3a 986   = wceq 1448   E.wex 1667   e. wcel 1891   =/= wne 2622   E.wrex 2738   \ cdif 3369   (/)c0 3699   {csn 3936   Ord word 5401   suc csuc 5404   omcom 6680

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-8 1893  ax-9 1900  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432  ax-sep 4497  ax-nul 4506  ax-pr 4612  ax-un 6571

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 987  df-3an 988  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-eu 2304  df-mo 2305  df-clab 2439  df-cleq 2445  df-clel 2448  df-nfc 2582  df-ne 2624  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3015  df-sbc 3236  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-pss 3388  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-tp 3941  df-op 3943  df-uni 4169  df-br 4375  df-opab 4434  df-tr 4470  df-eprel 4723  df-po 4733  df-so 4734  df-fr 4771  df-we 4773  df-ord 5405  df-on 5406  df-lim 5407  df-suc 5408  df-om 6681

This theorem is referenced by:  bnj1110  29797  bnj1128  29805  bnj1145  29808