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 )