Metamath Proof Explorer

Theorem bnj563

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

Ref Expression
Hypotheses bnj563.19 
|- ( et <-> ( m e. D /\ n = suc m /\ p e. _om /\ m = suc p ) )
bnj563.21 
|- ( rh <-> ( i e. _om /\ suc i e. n /\ m =/= suc i ) )
Assertion bnj563 
|- ( ( et /\ rh ) -> suc i e. m )

Proof

Step Hyp Ref Expression
1 bnj563.19 
 |-  ( et <-> ( m e. D /\ n = suc m /\ p e. _om /\ m = suc p ) )
2 bnj563.21 
 |-  ( rh <-> ( i e. _om /\ suc i e. n /\ m =/= suc i ) )
3 bnj312 
 |-  ( ( m e. D /\ n = suc m /\ p e. _om /\ m = suc p ) <-> ( n = suc m /\ m e. D /\ p e. _om /\ m = suc p ) )
4 bnj252 
 |-  ( ( n = suc m /\ m e. D /\ p e. _om /\ m = suc p ) <-> ( n = suc m /\ ( m e. D /\ p e. _om /\ m = suc p ) ) )
5 3 4 bitri 
 |-  ( ( m e. D /\ n = suc m /\ p e. _om /\ m = suc p ) <-> ( n = suc m /\ ( m e. D /\ p e. _om /\ m = suc p ) ) )
6 5 simplbi 
 |-  ( ( m e. D /\ n = suc m /\ p e. _om /\ m = suc p ) -> n = suc m )
7 1 6 sylbi 
 |-  ( et -> n = suc m )
8 2 simp2bi 
 |-  ( rh -> suc i e. n )
9 2 simp3bi 
 |-  ( rh -> m =/= suc i )
10 8 9 jca 
 |-  ( rh -> ( suc i e. n /\ m =/= suc i ) )
11 necom 
 |-  ( m =/= suc i <-> suc i =/= m )
12 eleq2 
 |-  ( n = suc m -> ( suc i e. n <-> suc i e. suc m ) )
13 12 biimpa 
 |-  ( ( n = suc m /\ suc i e. n ) -> suc i e. suc m )
14 elsuci 
 |-  ( suc i e. suc m -> ( suc i e. m \/ suc i = m ) )
15 orcom 
 |-  ( ( suc i = m \/ suc i e. m ) <-> ( suc i e. m \/ suc i = m ) )
16 neor 
 |-  ( ( suc i = m \/ suc i e. m ) <-> ( suc i =/= m -> suc i e. m ) )
17 15 16 bitr3i 
 |-  ( ( suc i e. m \/ suc i = m ) <-> ( suc i =/= m -> suc i e. m ) )
18 14 17 sylib 
 |-  ( suc i e. suc m -> ( suc i =/= m -> suc i e. m ) )
19 18 imp 
 |-  ( ( suc i e. suc m /\ suc i =/= m ) -> suc i e. m )
20 13 19 stoic3 
 |-  ( ( n = suc m /\ suc i e. n /\ suc i =/= m ) -> suc i e. m )
21 11 20 syl3an3b 
 |-  ( ( n = suc m /\ suc i e. n /\ m =/= suc i ) -> suc i e. m )
22 21 3expb 
 |-  ( ( n = suc m /\ ( suc i e. n /\ m =/= suc i ) ) -> suc i e. m )
23 7 10 22 syl2an 
 |-  ( ( et /\ rh ) -> suc i e. m )