Metamath Proof Explorer

Theorem bnj605

Description: Technical lemma. 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 bnj605.5 
|- ( th <-> A. m e. D ( m _E n -> [. m / n ]. ch ) )
bnj605.13 
|- ( ph" <-> [. f / f ]. ph )
bnj605.14 
|- ( ps" <-> [. f / f ]. ps )
bnj605.17 
|- ( ta <-> ( f Fn m /\ ph' /\ ps' ) )
bnj605.19 
|- ( et <-> ( m e. D /\ n = suc m /\ p e. _om /\ m = suc p ) )
bnj605.28 
|- f e. _V
bnj605.31 
|- ( ch' <-> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn m /\ ph' /\ ps' ) ) )
bnj605.32 
|- ( ph" <-> ( f ` (/) ) = _pred ( x , A , R ) )
bnj605.33 
|- ( ps" <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
bnj605.37 
|- ( ( n =/= 1o /\ n e. D ) -> E. m E. p et )
bnj605.38 
|- ( ( th /\ m e. D /\ m _E n ) -> ch' )
bnj605.41 
|- ( ( R _FrSe A /\ ta /\ et ) -> f Fn n )
bnj605.42 
|- ( ( R _FrSe A /\ ta /\ et ) -> ph" )
bnj605.43 
|- ( ( R _FrSe A /\ ta /\ et ) -> ps" )
Assertion bnj605 
|- ( ( n =/= 1o /\ n e. D /\ th ) -> ( ( R _FrSe A /\ x e. A ) -> E. f ( f Fn n /\ ph /\ ps ) ) )

Proof

Step Hyp Ref Expression
1 bnj605.5 
 |-  ( th <-> A. m e. D ( m _E n -> [. m / n ]. ch ) )
2 bnj605.13 
 |-  ( ph" <-> [. f / f ]. ph )
3 bnj605.14 
 |-  ( ps" <-> [. f / f ]. ps )
4 bnj605.17 
 |-  ( ta <-> ( f Fn m /\ ph' /\ ps' ) )
5 bnj605.19 
 |-  ( et <-> ( m e. D /\ n = suc m /\ p e. _om /\ m = suc p ) )
6 bnj605.28 
 |-  f e. _V
7 bnj605.31 
 |-  ( ch' <-> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn m /\ ph' /\ ps' ) ) )
8 bnj605.32 
 |-  ( ph" <-> ( f ` (/) ) = _pred ( x , A , R ) )
9 bnj605.33 
 |-  ( ps" <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
10 bnj605.37 
 |-  ( ( n =/= 1o /\ n e. D ) -> E. m E. p et )
11 bnj605.38 
 |-  ( ( th /\ m e. D /\ m _E n ) -> ch' )
12 bnj605.41 
 |-  ( ( R _FrSe A /\ ta /\ et ) -> f Fn n )
13 bnj605.42 
 |-  ( ( R _FrSe A /\ ta /\ et ) -> ph" )
14 bnj605.43 
 |-  ( ( R _FrSe A /\ ta /\ et ) -> ps" )
15 10 anim1i 
 |-  ( ( ( n =/= 1o /\ n e. D ) /\ th ) -> ( E. m E. p et /\ th ) )
16 nfv 
 |-  F/ p th
17 16 19.41 
 |-  ( E. p ( et /\ th ) <-> ( E. p et /\ th ) )
18 17 exbii 
 |-  ( E. m E. p ( et /\ th ) <-> E. m ( E. p et /\ th ) )
19 1 bnj1095 
 |-  ( th -> A. m th )
20 19 nf5i 
 |-  F/ m th
21 20 19.41 
 |-  ( E. m ( E. p et /\ th ) <-> ( E. m E. p et /\ th ) )
22 18 21 bitr2i 
 |-  ( ( E. m E. p et /\ th ) <-> E. m E. p ( et /\ th ) )
23 15 22 sylib 
 |-  ( ( ( n =/= 1o /\ n e. D ) /\ th ) -> E. m E. p ( et /\ th ) )
24 5 bnj1232 
 |-  ( et -> m e. D )
25 bnj219 
 |-  ( n = suc m -> m _E n )
26 5 25 bnj770 
 |-  ( et -> m _E n )
27 24 26 jca 
 |-  ( et -> ( m e. D /\ m _E n ) )
28 27 anim1i 
 |-  ( ( et /\ th ) -> ( ( m e. D /\ m _E n ) /\ th ) )
29 bnj170 
 |-  ( ( th /\ m e. D /\ m _E n ) <-> ( ( m e. D /\ m _E n ) /\ th ) )
30 28 29 sylibr 
 |-  ( ( et /\ th ) -> ( th /\ m e. D /\ m _E n ) )
31 30 11 syl 
 |-  ( ( et /\ th ) -> ch' )
32 simpl 
 |-  ( ( et /\ th ) -> et )
33 31 32 jca 
 |-  ( ( et /\ th ) -> ( ch' /\ et ) )
34 33 2eximi 
 |-  ( E. m E. p ( et /\ th ) -> E. m E. p ( ch' /\ et ) )
35 bnj248 
 |-  ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) <-> ( ( ( R _FrSe A /\ x e. A ) /\ ch' ) /\ et ) )
36 pm3.35 
 |-  ( ( ( R _FrSe A /\ x e. A ) /\ ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn m /\ ph' /\ ps' ) ) ) -> E! f ( f Fn m /\ ph' /\ ps' ) )
37 7 36 sylan2b 
 |-  ( ( ( R _FrSe A /\ x e. A ) /\ ch' ) -> E! f ( f Fn m /\ ph' /\ ps' ) )
38 euex 
 |-  ( E! f ( f Fn m /\ ph' /\ ps' ) -> E. f ( f Fn m /\ ph' /\ ps' ) )
39 37 38 syl 
 |-  ( ( ( R _FrSe A /\ x e. A ) /\ ch' ) -> E. f ( f Fn m /\ ph' /\ ps' ) )
40 39 4 bnj1198 
 |-  ( ( ( R _FrSe A /\ x e. A ) /\ ch' ) -> E. f ta )
41 35 40 bnj832 
 |-  ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) -> E. f ta )
42 12 13 14 3jca 
 |-  ( ( R _FrSe A /\ ta /\ et ) -> ( f Fn n /\ ph" /\ ps" ) )
43 42 3com23 
 |-  ( ( R _FrSe A /\ et /\ ta ) -> ( f Fn n /\ ph" /\ ps" ) )
44 43 3expia 
 |-  ( ( R _FrSe A /\ et ) -> ( ta -> ( f Fn n /\ ph" /\ ps" ) ) )
45 44 eximdv 
 |-  ( ( R _FrSe A /\ et ) -> ( E. f ta -> E. f ( f Fn n /\ ph" /\ ps" ) ) )
46 45 ad4ant14 
 |-  ( ( ( ( R _FrSe A /\ x e. A ) /\ ch' ) /\ et ) -> ( E. f ta -> E. f ( f Fn n /\ ph" /\ ps" ) ) )
47 35 46 sylbi 
 |-  ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) -> ( E. f ta -> E. f ( f Fn n /\ ph" /\ ps" ) ) )
48 41 47 mpd 
 |-  ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) -> E. f ( f Fn n /\ ph" /\ ps" ) )
49 bnj432 
 |-  ( ( R _FrSe A /\ x e. A /\ ch' /\ et ) <-> ( ( ch' /\ et ) /\ ( R _FrSe A /\ x e. A ) ) )
50 biid 
 |-  ( f Fn n <-> f Fn n )
51 sbcid 
 |-  ( [. f / f ]. ph <-> ph )
52 2 51 bitri 
 |-  ( ph" <-> ph )
53 sbcid 
 |-  ( [. f / f ]. ps <-> ps )
54 3 53 bitri 
 |-  ( ps" <-> ps )
55 50 52 54 3anbi123i 
 |-  ( ( f Fn n /\ ph" /\ ps" ) <-> ( f Fn n /\ ph /\ ps ) )
56 55 exbii 
 |-  ( E. f ( f Fn n /\ ph" /\ ps" ) <-> E. f ( f Fn n /\ ph /\ ps ) )
57 48 49 56 3imtr3i 
 |-  ( ( ( ch' /\ et ) /\ ( R _FrSe A /\ x e. A ) ) -> E. f ( f Fn n /\ ph /\ ps ) )
58 57 ex 
 |-  ( ( ch' /\ et ) -> ( ( R _FrSe A /\ x e. A ) -> E. f ( f Fn n /\ ph /\ ps ) ) )
59 58 exlimivv 
 |-  ( E. m E. p ( ch' /\ et ) -> ( ( R _FrSe A /\ x e. A ) -> E. f ( f Fn n /\ ph /\ ps ) ) )
60 23 34 59 3syl 
 |-  ( ( ( n =/= 1o /\ n e. D ) /\ th ) -> ( ( R _FrSe A /\ x e. A ) -> E. f ( f Fn n /\ ph /\ ps ) ) )
61 60 3impa 
 |-  ( ( n =/= 1o /\ n e. D /\ th ) -> ( ( R _FrSe A /\ x e. A ) -> E. f ( f Fn n /\ ph /\ ps ) ) )