Metamath Proof Explorer

Theorem bnj970

Description: Technical lemma for bnj69 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj970.3 
|- ( ch <-> ( n e. D /\ f Fn n /\ ph /\ ps ) )
bnj970.10 
|- D = ( _om \ { (/) } )
Assertion bnj970 
|- ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> p e. D )

Proof

Step Hyp Ref Expression
1 bnj970.3 
 |-  ( ch <-> ( n e. D /\ f Fn n /\ ph /\ ps ) )
2 bnj970.10 
 |-  D = ( _om \ { (/) } )
3 1 bnj1232 
 |-  ( ch -> n e. D )
4 3 3ad2ant1 
 |-  ( ( ch /\ n = suc m /\ p = suc n ) -> n e. D )
5 4 adantl 
 |-  ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> n e. D )
6 simpr3 
 |-  ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> p = suc n )
7 2 bnj923 
 |-  ( n e. D -> n e. _om )
8 peano2 
 |-  ( n e. _om -> suc n e. _om )
9 eleq1 
 |-  ( p = suc n -> ( p e. _om <-> suc n e. _om ) )
10 bianir 
 |-  ( ( suc n e. _om /\ ( p e. _om <-> suc n e. _om ) ) -> p e. _om )
11 8 9 10 syl2an 
 |-  ( ( n e. _om /\ p = suc n ) -> p e. _om )
12 7 11 sylan 
 |-  ( ( n e. D /\ p = suc n ) -> p e. _om )
13 df-suc 
 |-  suc n = ( n u. { n } )
14 13 eqeq2i 
 |-  ( p = suc n <-> p = ( n u. { n } ) )
15 ssun2 
 |-  { n } C_ ( n u. { n } )
16 vex 
 |-  n e. _V
17 16 snnz 
 |-  { n } =/= (/)
18 ssn0 
 |-  ( ( { n } C_ ( n u. { n } ) /\ { n } =/= (/) ) -> ( n u. { n } ) =/= (/) )
19 15 17 18 mp2an 
 |-  ( n u. { n } ) =/= (/)
20 neeq1 
 |-  ( p = ( n u. { n } ) -> ( p =/= (/) <-> ( n u. { n } ) =/= (/) ) )
21 19 20 mpbiri 
 |-  ( p = ( n u. { n } ) -> p =/= (/) )
22 14 21 sylbi 
 |-  ( p = suc n -> p =/= (/) )
23 22 adantl 
 |-  ( ( n e. D /\ p = suc n ) -> p =/= (/) )
24 2 eleq2i 
 |-  ( p e. D <-> p e. ( _om \ { (/) } ) )
25 eldifsn 
 |-  ( p e. ( _om \ { (/) } ) <-> ( p e. _om /\ p =/= (/) ) )
26 24 25 bitri 
 |-  ( p e. D <-> ( p e. _om /\ p =/= (/) ) )
27 12 23 26 sylanbrc 
 |-  ( ( n e. D /\ p = suc n ) -> p e. D )
28 5 6 27 syl2anc 
 |-  ( ( ( R _FrSe A /\ X e. A ) /\ ( ch /\ n = suc m /\ p = suc n ) ) -> p e. D )