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

Metamath Proof Explorer

Theorem bnj996

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 bnj996.1 
|- ( ph <-> ( f ` (/) ) = _pred ( X , A , R ) )
bnj996.2 
|- ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
bnj996.3 
|- ( ch <-> ( n e. D /\ f Fn n /\ ph /\ ps ) )
bnj996.4 
|- ( th <-> ( R _FrSe A /\ X e. A /\ y e. _trCl ( X , A , R ) /\ z e. _pred ( y , A , R ) ) )
bnj996.5 
|- ( ta <-> ( m e. _om /\ n = suc m /\ p = suc n ) )
bnj996.6 
|- ( et <-> ( i e. n /\ y e. ( f ` i ) ) )
bnj996.13 
|- D = ( _om \ { (/) } )
bnj996.14 
|- B = { f | E. n e. D ( f Fn n /\ ph /\ ps ) }
Assertion bnj996 
|- E. f E. n E. i E. m E. p ( th -> ( ch /\ ta /\ et ) )

Proof

Step Hyp Ref Expression
1 bnj996.1 
 |-  ( ph <-> ( f ` (/) ) = _pred ( X , A , R ) )
2 bnj996.2 
 |-  ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
3 bnj996.3 
 |-  ( ch <-> ( n e. D /\ f Fn n /\ ph /\ ps ) )
4 bnj996.4 
 |-  ( th <-> ( R _FrSe A /\ X e. A /\ y e. _trCl ( X , A , R ) /\ z e. _pred ( y , A , R ) ) )
5 bnj996.5 
 |-  ( ta <-> ( m e. _om /\ n = suc m /\ p = suc n ) )
6 bnj996.6 
 |-  ( et <-> ( i e. n /\ y e. ( f ` i ) ) )
7 bnj996.13 
 |-  D = ( _om \ { (/) } )
8 bnj996.14 
 |-  B = { f | E. n e. D ( f Fn n /\ ph /\ ps ) }
9 1 2 7 8 3 bnj917 
 |-  ( y e. _trCl ( X , A , R ) -> E. f E. n E. i ( ch /\ i e. n /\ y e. ( f ` i ) ) )
10 4 9 bnj771 
 |-  ( th -> E. f E. n E. i ( ch /\ i e. n /\ y e. ( f ` i ) ) )
11 3anass 
 |-  ( ( ch /\ i e. n /\ y e. ( f ` i ) ) <-> ( ch /\ ( i e. n /\ y e. ( f ` i ) ) ) )
12 6 anbi2i 
 |-  ( ( ch /\ et ) <-> ( ch /\ ( i e. n /\ y e. ( f ` i ) ) ) )
13 11 12 bitr4i 
 |-  ( ( ch /\ i e. n /\ y e. ( f ` i ) ) <-> ( ch /\ et ) )
14 13 3exbii 
 |-  ( E. f E. n E. i ( ch /\ i e. n /\ y e. ( f ` i ) ) <-> E. f E. n E. i ( ch /\ et ) )
15 10 14 sylib 
 |-  ( th -> E. f E. n E. i ( ch /\ et ) )
16 3 7 5 bnj986 
 |-  ( ch -> E. m E. p ta )
17 16 ancli 
 |-  ( ch -> ( ch /\ E. m E. p ta ) )
18 19.42vv 
 |-  ( E. m E. p ( ch /\ ta ) <-> ( ch /\ E. m E. p ta ) )
19 17 18 sylibr 
 |-  ( ch -> E. m E. p ( ch /\ ta ) )
20 19 anim1i 
 |-  ( ( ch /\ et ) -> ( E. m E. p ( ch /\ ta ) /\ et ) )
21 19.41vv 
 |-  ( E. m E. p ( ( ch /\ ta ) /\ et ) <-> ( E. m E. p ( ch /\ ta ) /\ et ) )
22 20 21 sylibr 
 |-  ( ( ch /\ et ) -> E. m E. p ( ( ch /\ ta ) /\ et ) )
23 df-3an 
 |-  ( ( ch /\ ta /\ et ) <-> ( ( ch /\ ta ) /\ et ) )
24 23 2exbii 
 |-  ( E. m E. p ( ch /\ ta /\ et ) <-> E. m E. p ( ( ch /\ ta ) /\ et ) )
25 22 24 sylibr 
 |-  ( ( ch /\ et ) -> E. m E. p ( ch /\ ta /\ et ) )
26 25 2eximi 
 |-  ( E. n E. i ( ch /\ et ) -> E. n E. i E. m E. p ( ch /\ ta /\ et ) )
27 15 26 bnj593 
 |-  ( th -> E. f E. n E. i E. m E. p ( ch /\ ta /\ et ) )
28 19.37v 
 |-  ( E. p ( th -> ( ch /\ ta /\ et ) ) <-> ( th -> E. p ( ch /\ ta /\ et ) ) )
29 28 exbii 
 |-  ( E. m E. p ( th -> ( ch /\ ta /\ et ) ) <-> E. m ( th -> E. p ( ch /\ ta /\ et ) ) )
30 29 bnj132 
 |-  ( E. m E. p ( th -> ( ch /\ ta /\ et ) ) <-> ( th -> E. m E. p ( ch /\ ta /\ et ) ) )
31 30 exbii 
 |-  ( E. i E. m E. p ( th -> ( ch /\ ta /\ et ) ) <-> E. i ( th -> E. m E. p ( ch /\ ta /\ et ) ) )
32 31 bnj132 
 |-  ( E. i E. m E. p ( th -> ( ch /\ ta /\ et ) ) <-> ( th -> E. i E. m E. p ( ch /\ ta /\ et ) ) )
33 32 exbii 
 |-  ( E. n E. i E. m E. p ( th -> ( ch /\ ta /\ et ) ) <-> E. n ( th -> E. i E. m E. p ( ch /\ ta /\ et ) ) )
34 33 bnj132 
 |-  ( E. n E. i E. m E. p ( th -> ( ch /\ ta /\ et ) ) <-> ( th -> E. n E. i E. m E. p ( ch /\ ta /\ et ) ) )
35 34 exbii 
 |-  ( E. f E. n E. i E. m E. p ( th -> ( ch /\ ta /\ et ) ) <-> E. f ( th -> E. n E. i E. m E. p ( ch /\ ta /\ et ) ) )
36 35 bnj132 
 |-  ( E. f E. n E. i E. m E. p ( th -> ( ch /\ ta /\ et ) ) <-> ( th -> E. f E. n E. i E. m E. p ( ch /\ ta /\ et ) ) )
37 27 36 mpbir 
 |-  E. f E. n E. i E. m E. p ( th -> ( ch /\ ta /\ et ) )