Metamath Proof Explorer

Theorem bnj607

Description: Technical lemma for bnj852 . 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 bnj607.5 
|- ( th <-> A. m e. D ( m _E n -> [. m / n ]. ch ) )
bnj607.13 
|- ( ph" <-> [. G / f ]. ph )
bnj607.14 
|- ( ps" <-> [. G / f ]. ps )
bnj607.17 
|- ( ta <-> ( f Fn m /\ ph' /\ ps' ) )
bnj607.19 
|- ( et <-> ( m e. D /\ n = suc m /\ p e. _om /\ m = suc p ) )
bnj607.28 
|- G e. _V
bnj607.31 
|- ( ch' <-> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn m /\ ph' /\ ps' ) ) )
bnj607.32 
|- ( ph" <-> ( G ` (/) ) = _pred ( x , A , R ) )
bnj607.33 
|- ( ps" <-> A. i e. _om ( suc i e. n -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) )
bnj607.37 
|- ( ( n =/= 1o /\ n e. D ) -> E. m E. p et )
bnj607.38 
|- ( ( th /\ m e. D /\ m _E n ) -> ch' )
bnj607.41 
|- ( ( R _FrSe A /\ ta /\ et ) -> G Fn n )
bnj607.42 
|- ( ( R _FrSe A /\ ta /\ et ) -> ph" )
bnj607.43 
|- ( ( R _FrSe A /\ ta /\ et ) -> ps" )
bnj607.1 
|- ( ph <-> ( f ` (/) ) = _pred ( x , A , R ) )
bnj607.2 
|- ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
bnj607.400 
|- ( ph0 <-> [. h / f ]. ph )
bnj607.401 
|- ( ps0 <-> [. h / f ]. ps )
bnj607.300 
|- ( ph1 <-> [. G / h ]. ph0 )
bnj607.301 
|- ( ps1 <-> [. G / h ]. ps0 )
Assertion bnj607 
|- ( ( 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 bnj607.5 
 |-  ( th <-> A. m e. D ( m _E n -> [. m / n ]. ch ) )
2 bnj607.13 
 |-  ( ph" <-> [. G / f ]. ph )
3 bnj607.14 
 |-  ( ps" <-> [. G / f ]. ps )
4 bnj607.17 
 |-  ( ta <-> ( f Fn m /\ ph' /\ ps' ) )
5 bnj607.19 
 |-  ( et <-> ( m e. D /\ n = suc m /\ p e. _om /\ m = suc p ) )
6 bnj607.28 
 |-  G e. _V
7 bnj607.31 
 |-  ( ch' <-> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn m /\ ph' /\ ps' ) ) )
8 bnj607.32 
 |-  ( ph" <-> ( G ` (/) ) = _pred ( x , A , R ) )
9 bnj607.33 
 |-  ( ps" <-> A. i e. _om ( suc i e. n -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) )
10 bnj607.37 
 |-  ( ( n =/= 1o /\ n e. D ) -> E. m E. p et )
11 bnj607.38 
 |-  ( ( th /\ m e. D /\ m _E n ) -> ch' )
12 bnj607.41 
 |-  ( ( R _FrSe A /\ ta /\ et ) -> G Fn n )
13 bnj607.42 
 |-  ( ( R _FrSe A /\ ta /\ et ) -> ph" )
14 bnj607.43 
 |-  ( ( R _FrSe A /\ ta /\ et ) -> ps" )
15 bnj607.1 
 |-  ( ph <-> ( f ` (/) ) = _pred ( x , A , R ) )
16 bnj607.2 
 |-  ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
17 bnj607.400 
 |-  ( ph0 <-> [. h / f ]. ph )
18 bnj607.401 
 |-  ( ps0 <-> [. h / f ]. ps )
19 bnj607.300 
 |-  ( ph1 <-> [. G / h ]. ph0 )
20 bnj607.301 
 |-  ( ps1 <-> [. G / h ]. ps0 )
21 10 anim1i 
 |-  ( ( ( n =/= 1o /\ n e. D ) /\ th ) -> ( E. m E. p et /\ th ) )
22 nfv 
 |-  F/ p th
23 22 19.41 
 |-  ( E. p ( et /\ th ) <-> ( E. p et /\ th ) )
24 23 exbii 
 |-  ( E. m E. p ( et /\ th ) <-> E. m ( E. p et /\ th ) )
25 1 bnj1095 
 |-  ( th -> A. m th )
26 25 nf5i 
 |-  F/ m th
27 26 19.41 
 |-  ( E. m ( E. p et /\ th ) <-> ( E. m E. p et /\ th ) )
28 24 27 bitr2i 
 |-  ( ( E. m E. p et /\ th ) <-> E. m E. p ( et /\ th ) )
29 21 28 sylib 
 |-  ( ( ( n =/= 1o /\ n e. D ) /\ th ) -> E. m E. p ( et /\ th ) )
30 5 bnj1232 
 |-  ( et -> m e. D )
31 bnj219 
 |-  ( n = suc m -> m _E n )
32 5 31 bnj770 
 |-  ( et -> m _E n )
33 30 32 jca 
 |-  ( et -> ( m e. D /\ m _E n ) )
34 33 anim1i 
 |-  ( ( et /\ th ) -> ( ( m e. D /\ m _E n ) /\ th ) )
35 bnj170 
 |-  ( ( th /\ m e. D /\ m _E n ) <-> ( ( m e. D /\ m _E n ) /\ th ) )
36 34 35 sylibr 
 |-  ( ( et /\ th ) -> ( th /\ m e. D /\ m _E n ) )
37 36 11 syl 
 |-  ( ( et /\ th ) -> ch' )
38 simpl 
 |-  ( ( et /\ th ) -> et )
39 37 38 jca 
 |-  ( ( et /\ th ) -> ( ch' /\ et ) )
40 39 2eximi 
 |-  ( E. m E. p ( et /\ th ) -> E. m E. p ( ch' /\ et ) )
41 7 biimpi 
 |-  ( ch' -> ( ( R _FrSe A /\ x e. A ) -> E! f ( f Fn m /\ ph' /\ ps' ) ) )
42 euex 
 |-  ( E! f ( f Fn m /\ ph' /\ ps' ) -> E. f ( f Fn m /\ ph' /\ ps' ) )
43 41 42 syl6 
 |-  ( ch' -> ( ( R _FrSe A /\ x e. A ) -> E. f ( f Fn m /\ ph' /\ ps' ) ) )
44 43 impcom 
 |-  ( ( ( R _FrSe A /\ x e. A ) /\ ch' ) -> E. f ( f Fn m /\ ph' /\ ps' ) )
45 44 4 bnj1198 
 |-  ( ( ( R _FrSe A /\ x e. A ) /\ ch' ) -> E. f ta )
46 45 adantrr 
 |-  ( ( ( R _FrSe A /\ x e. A ) /\ ( ch' /\ et ) ) -> E. f ta )
47 id 
 |-  ( ( R _FrSe A /\ ta /\ et ) -> ( R _FrSe A /\ ta /\ et ) )
48 47 3com23 
 |-  ( ( R _FrSe A /\ et /\ ta ) -> ( R _FrSe A /\ ta /\ et ) )
49 48 3expia 
 |-  ( ( R _FrSe A /\ et ) -> ( ta -> ( R _FrSe A /\ ta /\ et ) ) )
50 49 eximdv 
 |-  ( ( R _FrSe A /\ et ) -> ( E. f ta -> E. f ( R _FrSe A /\ ta /\ et ) ) )
51 50 ad2ant2rl 
 |-  ( ( ( R _FrSe A /\ x e. A ) /\ ( ch' /\ et ) ) -> ( E. f ta -> E. f ( R _FrSe A /\ ta /\ et ) ) )
52 46 51 mpd 
 |-  ( ( ( R _FrSe A /\ x e. A ) /\ ( ch' /\ et ) ) -> E. f ( R _FrSe A /\ ta /\ et ) )
53 12 13 14 3jca 
 |-  ( ( R _FrSe A /\ ta /\ et ) -> ( G Fn n /\ ph" /\ ps" ) )
54 53 eximi 
 |-  ( E. f ( R _FrSe A /\ ta /\ et ) -> E. f ( G Fn n /\ ph" /\ ps" ) )
55 nfe1 
 |-  F/ f E. f ( f Fn n /\ ph /\ ps )
56 nfcv 
 |-  F/_ h G
57 nfv 
 |-  F/ h G Fn n
58 nfsbc1v 
 |-  F/ h [. G / h ]. ph0
59 19 58 nfxfr 
 |-  F/ h ph1
60 nfsbc1v 
 |-  F/ h [. G / h ]. ps0
61 20 60 nfxfr 
 |-  F/ h ps1
62 57 59 61 nf3an 
 |-  F/ h ( G Fn n /\ ph1 /\ ps1 )
63 fneq1 
 |-  ( h = G -> ( h Fn n <-> G Fn n ) )
64 sbceq1a 
 |-  ( h = G -> ( ph0 <-> [. G / h ]. ph0 ) )
65 64 19 bitr4di 
 |-  ( h = G -> ( ph0 <-> ph1 ) )
66 sbceq1a 
 |-  ( h = G -> ( ps0 <-> [. G / h ]. ps0 ) )
67 66 20 bitr4di 
 |-  ( h = G -> ( ps0 <-> ps1 ) )
68 63 65 67 3anbi123d 
 |-  ( h = G -> ( ( h Fn n /\ ph0 /\ ps0 ) <-> ( G Fn n /\ ph1 /\ ps1 ) ) )
69 56 62 68 spcegf 
 |-  ( G e. _V -> ( ( G Fn n /\ ph1 /\ ps1 ) -> E. h ( h Fn n /\ ph0 /\ ps0 ) ) )
70 6 69 ax-mp 
 |-  ( ( G Fn n /\ ph1 /\ ps1 ) -> E. h ( h Fn n /\ ph0 /\ ps0 ) )
71 17 15 bnj154 
 |-  ( ph0 <-> ( h ` (/) ) = _pred ( x , A , R ) )
72 71 19 6 bnj526 
 |-  ( ph1 <-> ( G ` (/) ) = _pred ( x , A , R ) )
73 8 72 bitr4i 
 |-  ( ph" <-> ph1 )
74 vex 
 |-  h e. _V
75 16 18 74 bnj540 
 |-  ( ps0 <-> A. i e. _om ( suc i e. n -> ( h ` suc i ) = U_ y e. ( h ` i ) _pred ( y , A , R ) ) )
76 75 20 6 bnj540 
 |-  ( ps1 <-> A. i e. _om ( suc i e. n -> ( G ` suc i ) = U_ y e. ( G ` i ) _pred ( y , A , R ) ) )
77 9 76 bitr4i 
 |-  ( ps" <-> ps1 )
78 73 77 anbi12i 
 |-  ( ( ph" /\ ps" ) <-> ( ph1 /\ ps1 ) )
79 78 anbi2i 
 |-  ( ( G Fn n /\ ( ph" /\ ps" ) ) <-> ( G Fn n /\ ( ph1 /\ ps1 ) ) )
80 3anass 
 |-  ( ( G Fn n /\ ph" /\ ps" ) <-> ( G Fn n /\ ( ph" /\ ps" ) ) )
81 3anass 
 |-  ( ( G Fn n /\ ph1 /\ ps1 ) <-> ( G Fn n /\ ( ph1 /\ ps1 ) ) )
82 79 80 81 3bitr4i 
 |-  ( ( G Fn n /\ ph" /\ ps" ) <-> ( G Fn n /\ ph1 /\ ps1 ) )
83 nfv 
 |-  F/ h ( f Fn n /\ ph /\ ps )
84 nfv 
 |-  F/ f h Fn n
85 nfsbc1v 
 |-  F/ f [. h / f ]. ph
86 17 85 nfxfr 
 |-  F/ f ph0
87 nfsbc1v 
 |-  F/ f [. h / f ]. ps
88 18 87 nfxfr 
 |-  F/ f ps0
89 84 86 88 nf3an 
 |-  F/ f ( h Fn n /\ ph0 /\ ps0 )
90 fneq1 
 |-  ( f = h -> ( f Fn n <-> h Fn n ) )
91 sbceq1a 
 |-  ( f = h -> ( ph <-> [. h / f ]. ph ) )
92 91 17 bitr4di 
 |-  ( f = h -> ( ph <-> ph0 ) )
93 sbceq1a 
 |-  ( f = h -> ( ps <-> [. h / f ]. ps ) )
94 93 18 bitr4di 
 |-  ( f = h -> ( ps <-> ps0 ) )
95 90 92 94 3anbi123d 
 |-  ( f = h -> ( ( f Fn n /\ ph /\ ps ) <-> ( h Fn n /\ ph0 /\ ps0 ) ) )
96 83 89 95 cbvexv1 
 |-  ( E. f ( f Fn n /\ ph /\ ps ) <-> E. h ( h Fn n /\ ph0 /\ ps0 ) )
97 70 82 96 3imtr4i 
 |-  ( ( G Fn n /\ ph" /\ ps" ) -> E. f ( f Fn n /\ ph /\ ps ) )
98 55 97 exlimi 
 |-  ( E. f ( G Fn n /\ ph" /\ ps" ) -> E. f ( f Fn n /\ ph /\ ps ) )
99 52 54 98 3syl 
 |-  ( ( ( R _FrSe A /\ x e. A ) /\ ( ch' /\ et ) ) -> E. f ( f Fn n /\ ph /\ ps ) )
100 99 expcom 
 |-  ( ( ch' /\ et ) -> ( ( R _FrSe A /\ x e. A ) -> E. f ( f Fn n /\ ph /\ ps ) ) )
101 100 exlimivv 
 |-  ( E. m E. p ( ch' /\ et ) -> ( ( R _FrSe A /\ x e. A ) -> E. f ( f Fn n /\ ph /\ ps ) ) )
102 29 40 101 3syl 
 |-  ( ( ( n =/= 1o /\ n e. D ) /\ th ) -> ( ( R _FrSe A /\ x e. A ) -> E. f ( f Fn n /\ ph /\ ps ) ) )
103 102 3impa 
 |-  ( ( n =/= 1o /\ n e. D /\ th ) -> ( ( R _FrSe A /\ x e. A ) -> E. f ( f Fn n /\ ph /\ ps ) ) )