This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bnj986

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 bnj986.3 
|- ( ch <-> ( n e. D /\ f Fn n /\ ph /\ ps ) )
bnj986.10 
|- D = ( _om \ { (/) } )
bnj986.15 
|- ( ta <-> ( m e. _om /\ n = suc m /\ p = suc n ) )
Assertion bnj986 
|- ( ch -> E. m E. p ta )

Proof

Step Hyp Ref Expression
1 bnj986.3 
 |-  ( ch <-> ( n e. D /\ f Fn n /\ ph /\ ps ) )
2 bnj986.10 
 |-  D = ( _om \ { (/) } )
3 bnj986.15 
 |-  ( ta <-> ( m e. _om /\ n = suc m /\ p = suc n ) )
4 2 bnj158 
 |-  ( n e. D -> E. m e. _om n = suc m )
5 1 4 bnj769 
 |-  ( ch -> E. m e. _om n = suc m )
6 5 bnj1196 
 |-  ( ch -> E. m ( m e. _om /\ n = suc m ) )
7 vex 
 |-  n e. _V
8 7 sucex 
 |-  suc n e. _V
9 8 isseti 
 |-  E. p p = suc n
10 6 9 jctir 
 |-  ( ch -> ( E. m ( m e. _om /\ n = suc m ) /\ E. p p = suc n ) )
11 exdistr 
 |-  ( E. m E. p ( ( m e. _om /\ n = suc m ) /\ p = suc n ) <-> E. m ( ( m e. _om /\ n = suc m ) /\ E. p p = suc n ) )
12 19.41v 
 |-  ( E. m ( ( m e. _om /\ n = suc m ) /\ E. p p = suc n ) <-> ( E. m ( m e. _om /\ n = suc m ) /\ E. p p = suc n ) )
13 11 12 bitr2i 
 |-  ( ( E. m ( m e. _om /\ n = suc m ) /\ E. p p = suc n ) <-> E. m E. p ( ( m e. _om /\ n = suc m ) /\ p = suc n ) )
14 10 13 sylib 
 |-  ( ch -> E. m E. p ( ( m e. _om /\ n = suc m ) /\ p = suc n ) )
15 df-3an 
 |-  ( ( m e. _om /\ n = suc m /\ p = suc n ) <-> ( ( m e. _om /\ n = suc m ) /\ p = suc n ) )
16 3 15 bitri 
 |-  ( ta <-> ( ( m e. _om /\ n = suc m ) /\ p = suc n ) )
17 16 2exbii 
 |-  ( E. m E. p ta <-> E. m E. p ( ( m e. _om /\ n = suc m ) /\ p = suc n ) )
18 14 17 sylibr 
 |-  ( ch -> E. m E. p ta )