Metamath Proof Explorer

Theorem cvmlift3lem2

Description: Lemma for cvmlift2 . (Contributed by Mario Carneiro, 6-Jul-2015)

Ref Expression
Hypotheses cvmlift3.b 
|- B = U. C
cvmlift3.y 
|- Y = U. K
cvmlift3.f 
|- ( ph -> F e. ( C CovMap J ) )
cvmlift3.k 
|- ( ph -> K e. SConn )
cvmlift3.l 
|- ( ph -> K e. N-Locally PConn )
cvmlift3.o 
|- ( ph -> O e. Y )
cvmlift3.g 
|- ( ph -> G e. ( K Cn J ) )
cvmlift3.p 
|- ( ph -> P e. B )
cvmlift3.e 
|- ( ph -> ( F ` P ) = ( G ` O ) )
Assertion cvmlift3lem2 
|- ( ( ph /\ X e. Y ) -> E! z e. B E. f e. ( II Cn K ) ( ( f ` 0 ) = O /\ ( f ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = z ) )

Proof

Step Hyp Ref Expression
1 cvmlift3.b 
 |-  B = U. C
2 cvmlift3.y 
 |-  Y = U. K
3 cvmlift3.f 
 |-  ( ph -> F e. ( C CovMap J ) )
4 cvmlift3.k 
 |-  ( ph -> K e. SConn )
5 cvmlift3.l 
 |-  ( ph -> K e. N-Locally PConn )
6 cvmlift3.o 
 |-  ( ph -> O e. Y )
7 cvmlift3.g 
 |-  ( ph -> G e. ( K Cn J ) )
8 cvmlift3.p 
 |-  ( ph -> P e. B )
9 cvmlift3.e 
 |-  ( ph -> ( F ` P ) = ( G ` O ) )
10 4 adantr 
 |-  ( ( ph /\ X e. Y ) -> K e. SConn )
11 sconnpconn 
 |-  ( K e. SConn -> K e. PConn )
12 10 11 syl 
 |-  ( ( ph /\ X e. Y ) -> K e. PConn )
13 6 adantr 
 |-  ( ( ph /\ X e. Y ) -> O e. Y )
14 simpr 
 |-  ( ( ph /\ X e. Y ) -> X e. Y )
15 2 pconncn 
 |-  ( ( K e. PConn /\ O e. Y /\ X e. Y ) -> E. a e. ( II Cn K ) ( ( a ` 0 ) = O /\ ( a ` 1 ) = X ) )
16 12 13 14 15 syl3anc 
 |-  ( ( ph /\ X e. Y ) -> E. a e. ( II Cn K ) ( ( a ` 0 ) = O /\ ( a ` 1 ) = X ) )
17 eqid 
 |-  ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. a ) /\ ( g ` 0 ) = P ) ) = ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. a ) /\ ( g ` 0 ) = P ) )
18 3 ad2antrr 
 |-  ( ( ( ph /\ X e. Y ) /\ ( a e. ( II Cn K ) /\ ( ( a ` 0 ) = O /\ ( a ` 1 ) = X ) ) ) -> F e. ( C CovMap J ) )
19 simprl 
 |-  ( ( ( ph /\ X e. Y ) /\ ( a e. ( II Cn K ) /\ ( ( a ` 0 ) = O /\ ( a ` 1 ) = X ) ) ) -> a e. ( II Cn K ) )
20 7 ad2antrr 
 |-  ( ( ( ph /\ X e. Y ) /\ ( a e. ( II Cn K ) /\ ( ( a ` 0 ) = O /\ ( a ` 1 ) = X ) ) ) -> G e. ( K Cn J ) )
21 cnco 
 |-  ( ( a e. ( II Cn K ) /\ G e. ( K Cn J ) ) -> ( G o. a ) e. ( II Cn J ) )
22 19 20 21 syl2anc 
 |-  ( ( ( ph /\ X e. Y ) /\ ( a e. ( II Cn K ) /\ ( ( a ` 0 ) = O /\ ( a ` 1 ) = X ) ) ) -> ( G o. a ) e. ( II Cn J ) )
23 8 ad2antrr 
 |-  ( ( ( ph /\ X e. Y ) /\ ( a e. ( II Cn K ) /\ ( ( a ` 0 ) = O /\ ( a ` 1 ) = X ) ) ) -> P e. B )
24 simprrl 
 |-  ( ( ( ph /\ X e. Y ) /\ ( a e. ( II Cn K ) /\ ( ( a ` 0 ) = O /\ ( a ` 1 ) = X ) ) ) -> ( a ` 0 ) = O )
25 24 fveq2d 
 |-  ( ( ( ph /\ X e. Y ) /\ ( a e. ( II Cn K ) /\ ( ( a ` 0 ) = O /\ ( a ` 1 ) = X ) ) ) -> ( G ` ( a ` 0 ) ) = ( G ` O ) )
26 iiuni 
 |-  ( 0 [,] 1 ) = U. II
27 26 2 cnf 
 |-  ( a e. ( II Cn K ) -> a : ( 0 [,] 1 ) --> Y )
28 19 27 syl 
 |-  ( ( ( ph /\ X e. Y ) /\ ( a e. ( II Cn K ) /\ ( ( a ` 0 ) = O /\ ( a ` 1 ) = X ) ) ) -> a : ( 0 [,] 1 ) --> Y )
29 0elunit 
 |-  0 e. ( 0 [,] 1 )
30 fvco3 
 |-  ( ( a : ( 0 [,] 1 ) --> Y /\ 0 e. ( 0 [,] 1 ) ) -> ( ( G o. a ) ` 0 ) = ( G ` ( a ` 0 ) ) )
31 28 29 30 sylancl 
 |-  ( ( ( ph /\ X e. Y ) /\ ( a e. ( II Cn K ) /\ ( ( a ` 0 ) = O /\ ( a ` 1 ) = X ) ) ) -> ( ( G o. a ) ` 0 ) = ( G ` ( a ` 0 ) ) )
32 9 ad2antrr 
 |-  ( ( ( ph /\ X e. Y ) /\ ( a e. ( II Cn K ) /\ ( ( a ` 0 ) = O /\ ( a ` 1 ) = X ) ) ) -> ( F ` P ) = ( G ` O ) )
33 25 31 32 3eqtr4rd 
 |-  ( ( ( ph /\ X e. Y ) /\ ( a e. ( II Cn K ) /\ ( ( a ` 0 ) = O /\ ( a ` 1 ) = X ) ) ) -> ( F ` P ) = ( ( G o. a ) ` 0 ) )
34 1 17 18 22 23 33 cvmliftiota 
 |-  ( ( ( ph /\ X e. Y ) /\ ( a e. ( II Cn K ) /\ ( ( a ` 0 ) = O /\ ( a ` 1 ) = X ) ) ) -> ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. a ) /\ ( g ` 0 ) = P ) ) e. ( II Cn C ) /\ ( F o. ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. a ) /\ ( g ` 0 ) = P ) ) ) = ( G o. a ) /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. a ) /\ ( g ` 0 ) = P ) ) ` 0 ) = P ) )
35 34 simp1d 
 |-  ( ( ( ph /\ X e. Y ) /\ ( a e. ( II Cn K ) /\ ( ( a ` 0 ) = O /\ ( a ` 1 ) = X ) ) ) -> ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. a ) /\ ( g ` 0 ) = P ) ) e. ( II Cn C ) )
36 26 1 cnf 
 |-  ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. a ) /\ ( g ` 0 ) = P ) ) e. ( II Cn C ) -> ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. a ) /\ ( g ` 0 ) = P ) ) : ( 0 [,] 1 ) --> B )
37 35 36 syl 
 |-  ( ( ( ph /\ X e. Y ) /\ ( a e. ( II Cn K ) /\ ( ( a ` 0 ) = O /\ ( a ` 1 ) = X ) ) ) -> ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. a ) /\ ( g ` 0 ) = P ) ) : ( 0 [,] 1 ) --> B )
38 1elunit 
 |-  1 e. ( 0 [,] 1 )
39 ffvelcdm 
 |-  ( ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. a ) /\ ( g ` 0 ) = P ) ) : ( 0 [,] 1 ) --> B /\ 1 e. ( 0 [,] 1 ) ) -> ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. a ) /\ ( g ` 0 ) = P ) ) ` 1 ) e. B )
40 37 38 39 sylancl 
 |-  ( ( ( ph /\ X e. Y ) /\ ( a e. ( II Cn K ) /\ ( ( a ` 0 ) = O /\ ( a ` 1 ) = X ) ) ) -> ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. a ) /\ ( g ` 0 ) = P ) ) ` 1 ) e. B )
41 simprrr 
 |-  ( ( ( ph /\ X e. Y ) /\ ( a e. ( II Cn K ) /\ ( ( a ` 0 ) = O /\ ( a ` 1 ) = X ) ) ) -> ( a ` 1 ) = X )
42 eqidd 
 |-  ( ( ( ph /\ X e. Y ) /\ ( a e. ( II Cn K ) /\ ( ( a ` 0 ) = O /\ ( a ` 1 ) = X ) ) ) -> ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. a ) /\ ( g ` 0 ) = P ) ) ` 1 ) = ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. a ) /\ ( g ` 0 ) = P ) ) ` 1 ) )
43 fveq1 
 |-  ( f = a -> ( f ` 0 ) = ( a ` 0 ) )
44 43 eqeq1d 
 |-  ( f = a -> ( ( f ` 0 ) = O <-> ( a ` 0 ) = O ) )
45 fveq1 
 |-  ( f = a -> ( f ` 1 ) = ( a ` 1 ) )
46 45 eqeq1d 
 |-  ( f = a -> ( ( f ` 1 ) = X <-> ( a ` 1 ) = X ) )
47 coeq2 
 |-  ( f = a -> ( G o. f ) = ( G o. a ) )
48 47 eqeq2d 
 |-  ( f = a -> ( ( F o. g ) = ( G o. f ) <-> ( F o. g ) = ( G o. a ) ) )
49 48 anbi1d 
 |-  ( f = a -> ( ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) <-> ( ( F o. g ) = ( G o. a ) /\ ( g ` 0 ) = P ) ) )
50 49 riotabidv 
 |-  ( f = a -> ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) = ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. a ) /\ ( g ` 0 ) = P ) ) )
51 50 fveq1d 
 |-  ( f = a -> ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. a ) /\ ( g ` 0 ) = P ) ) ` 1 ) )
52 51 eqeq1d 
 |-  ( f = a -> ( ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. a ) /\ ( g ` 0 ) = P ) ) ` 1 ) <-> ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. a ) /\ ( g ` 0 ) = P ) ) ` 1 ) = ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. a ) /\ ( g ` 0 ) = P ) ) ` 1 ) ) )
53 44 46 52 3anbi123d 
 |-  ( f = a -> ( ( ( f ` 0 ) = O /\ ( f ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. a ) /\ ( g ` 0 ) = P ) ) ` 1 ) ) <-> ( ( a ` 0 ) = O /\ ( a ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. a ) /\ ( g ` 0 ) = P ) ) ` 1 ) = ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. a ) /\ ( g ` 0 ) = P ) ) ` 1 ) ) ) )
54 53 rspcev 
 |-  ( ( a e. ( II Cn K ) /\ ( ( a ` 0 ) = O /\ ( a ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. a ) /\ ( g ` 0 ) = P ) ) ` 1 ) = ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. a ) /\ ( g ` 0 ) = P ) ) ` 1 ) ) ) -> E. f e. ( II Cn K ) ( ( f ` 0 ) = O /\ ( f ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. a ) /\ ( g ` 0 ) = P ) ) ` 1 ) ) )
55 19 24 41 42 54 syl13anc 
 |-  ( ( ( ph /\ X e. Y ) /\ ( a e. ( II Cn K ) /\ ( ( a ` 0 ) = O /\ ( a ` 1 ) = X ) ) ) -> E. f e. ( II Cn K ) ( ( f ` 0 ) = O /\ ( f ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. a ) /\ ( g ` 0 ) = P ) ) ` 1 ) ) )
56 3 ad4antr 
 |-  ( ( ( ( ( ph /\ X e. Y ) /\ ( a e. ( II Cn K ) /\ ( ( a ` 0 ) = O /\ ( a ` 1 ) = X ) ) ) /\ w e. B ) /\ ( h e. ( II Cn K ) /\ ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. h ) /\ ( g ` 0 ) = P ) ) ` 1 ) = w ) ) ) -> F e. ( C CovMap J ) )
57 4 ad4antr 
 |-  ( ( ( ( ( ph /\ X e. Y ) /\ ( a e. ( II Cn K ) /\ ( ( a ` 0 ) = O /\ ( a ` 1 ) = X ) ) ) /\ w e. B ) /\ ( h e. ( II Cn K ) /\ ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. h ) /\ ( g ` 0 ) = P ) ) ` 1 ) = w ) ) ) -> K e. SConn )
58 5 ad4antr 
 |-  ( ( ( ( ( ph /\ X e. Y ) /\ ( a e. ( II Cn K ) /\ ( ( a ` 0 ) = O /\ ( a ` 1 ) = X ) ) ) /\ w e. B ) /\ ( h e. ( II Cn K ) /\ ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. h ) /\ ( g ` 0 ) = P ) ) ` 1 ) = w ) ) ) -> K e. N-Locally PConn )
59 6 ad4antr 
 |-  ( ( ( ( ( ph /\ X e. Y ) /\ ( a e. ( II Cn K ) /\ ( ( a ` 0 ) = O /\ ( a ` 1 ) = X ) ) ) /\ w e. B ) /\ ( h e. ( II Cn K ) /\ ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. h ) /\ ( g ` 0 ) = P ) ) ` 1 ) = w ) ) ) -> O e. Y )
60 7 ad4antr 
 |-  ( ( ( ( ( ph /\ X e. Y ) /\ ( a e. ( II Cn K ) /\ ( ( a ` 0 ) = O /\ ( a ` 1 ) = X ) ) ) /\ w e. B ) /\ ( h e. ( II Cn K ) /\ ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. h ) /\ ( g ` 0 ) = P ) ) ` 1 ) = w ) ) ) -> G e. ( K Cn J ) )
61 8 ad4antr 
 |-  ( ( ( ( ( ph /\ X e. Y ) /\ ( a e. ( II Cn K ) /\ ( ( a ` 0 ) = O /\ ( a ` 1 ) = X ) ) ) /\ w e. B ) /\ ( h e. ( II Cn K ) /\ ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. h ) /\ ( g ` 0 ) = P ) ) ` 1 ) = w ) ) ) -> P e. B )
62 9 ad4antr 
 |-  ( ( ( ( ( ph /\ X e. Y ) /\ ( a e. ( II Cn K ) /\ ( ( a ` 0 ) = O /\ ( a ` 1 ) = X ) ) ) /\ w e. B ) /\ ( h e. ( II Cn K ) /\ ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. h ) /\ ( g ` 0 ) = P ) ) ` 1 ) = w ) ) ) -> ( F ` P ) = ( G ` O ) )
63 19 ad2antrr 
 |-  ( ( ( ( ( ph /\ X e. Y ) /\ ( a e. ( II Cn K ) /\ ( ( a ` 0 ) = O /\ ( a ` 1 ) = X ) ) ) /\ w e. B ) /\ ( h e. ( II Cn K ) /\ ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. h ) /\ ( g ` 0 ) = P ) ) ` 1 ) = w ) ) ) -> a e. ( II Cn K ) )
64 24 ad2antrr 
 |-  ( ( ( ( ( ph /\ X e. Y ) /\ ( a e. ( II Cn K ) /\ ( ( a ` 0 ) = O /\ ( a ` 1 ) = X ) ) ) /\ w e. B ) /\ ( h e. ( II Cn K ) /\ ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. h ) /\ ( g ` 0 ) = P ) ) ` 1 ) = w ) ) ) -> ( a ` 0 ) = O )
65 simprl 
 |-  ( ( ( ( ( ph /\ X e. Y ) /\ ( a e. ( II Cn K ) /\ ( ( a ` 0 ) = O /\ ( a ` 1 ) = X ) ) ) /\ w e. B ) /\ ( h e. ( II Cn K ) /\ ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. h ) /\ ( g ` 0 ) = P ) ) ` 1 ) = w ) ) ) -> h e. ( II Cn K ) )
66 simprr1 
 |-  ( ( ( ( ( ph /\ X e. Y ) /\ ( a e. ( II Cn K ) /\ ( ( a ` 0 ) = O /\ ( a ` 1 ) = X ) ) ) /\ w e. B ) /\ ( h e. ( II Cn K ) /\ ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. h ) /\ ( g ` 0 ) = P ) ) ` 1 ) = w ) ) ) -> ( h ` 0 ) = O )
67 41 ad2antrr 
 |-  ( ( ( ( ( ph /\ X e. Y ) /\ ( a e. ( II Cn K ) /\ ( ( a ` 0 ) = O /\ ( a ` 1 ) = X ) ) ) /\ w e. B ) /\ ( h e. ( II Cn K ) /\ ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. h ) /\ ( g ` 0 ) = P ) ) ` 1 ) = w ) ) ) -> ( a ` 1 ) = X )
68 simprr2 
 |-  ( ( ( ( ( ph /\ X e. Y ) /\ ( a e. ( II Cn K ) /\ ( ( a ` 0 ) = O /\ ( a ` 1 ) = X ) ) ) /\ w e. B ) /\ ( h e. ( II Cn K ) /\ ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. h ) /\ ( g ` 0 ) = P ) ) ` 1 ) = w ) ) ) -> ( h ` 1 ) = X )
69 67 68 eqtr4d 
 |-  ( ( ( ( ( ph /\ X e. Y ) /\ ( a e. ( II Cn K ) /\ ( ( a ` 0 ) = O /\ ( a ` 1 ) = X ) ) ) /\ w e. B ) /\ ( h e. ( II Cn K ) /\ ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. h ) /\ ( g ` 0 ) = P ) ) ` 1 ) = w ) ) ) -> ( a ` 1 ) = ( h ` 1 ) )
70 1 2 56 57 58 59 60 61 62 63 64 65 66 69 cvmlift3lem1 
 |-  ( ( ( ( ( ph /\ X e. Y ) /\ ( a e. ( II Cn K ) /\ ( ( a ` 0 ) = O /\ ( a ` 1 ) = X ) ) ) /\ w e. B ) /\ ( h e. ( II Cn K ) /\ ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. h ) /\ ( g ` 0 ) = P ) ) ` 1 ) = w ) ) ) -> ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. a ) /\ ( g ` 0 ) = P ) ) ` 1 ) = ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. h ) /\ ( g ` 0 ) = P ) ) ` 1 ) )
71 simprr3 
 |-  ( ( ( ( ( ph /\ X e. Y ) /\ ( a e. ( II Cn K ) /\ ( ( a ` 0 ) = O /\ ( a ` 1 ) = X ) ) ) /\ w e. B ) /\ ( h e. ( II Cn K ) /\ ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. h ) /\ ( g ` 0 ) = P ) ) ` 1 ) = w ) ) ) -> ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. h ) /\ ( g ` 0 ) = P ) ) ` 1 ) = w )
72 70 71 eqtrd 
 |-  ( ( ( ( ( ph /\ X e. Y ) /\ ( a e. ( II Cn K ) /\ ( ( a ` 0 ) = O /\ ( a ` 1 ) = X ) ) ) /\ w e. B ) /\ ( h e. ( II Cn K ) /\ ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. h ) /\ ( g ` 0 ) = P ) ) ` 1 ) = w ) ) ) -> ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. a ) /\ ( g ` 0 ) = P ) ) ` 1 ) = w )
73 72 rexlimdvaa 
 |-  ( ( ( ( ph /\ X e. Y ) /\ ( a e. ( II Cn K ) /\ ( ( a ` 0 ) = O /\ ( a ` 1 ) = X ) ) ) /\ w e. B ) -> ( E. h e. ( II Cn K ) ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. h ) /\ ( g ` 0 ) = P ) ) ` 1 ) = w ) -> ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. a ) /\ ( g ` 0 ) = P ) ) ` 1 ) = w ) )
74 73 ralrimiva 
 |-  ( ( ( ph /\ X e. Y ) /\ ( a e. ( II Cn K ) /\ ( ( a ` 0 ) = O /\ ( a ` 1 ) = X ) ) ) -> A. w e. B ( E. h e. ( II Cn K ) ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. h ) /\ ( g ` 0 ) = P ) ) ` 1 ) = w ) -> ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. a ) /\ ( g ` 0 ) = P ) ) ` 1 ) = w ) )
75 eqeq2 
 |-  ( z = ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. a ) /\ ( g ` 0 ) = P ) ) ` 1 ) -> ( ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = z <-> ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. a ) /\ ( g ` 0 ) = P ) ) ` 1 ) ) )
76 75 3anbi3d 
 |-  ( z = ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. a ) /\ ( g ` 0 ) = P ) ) ` 1 ) -> ( ( ( f ` 0 ) = O /\ ( f ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = z ) <-> ( ( f ` 0 ) = O /\ ( f ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. a ) /\ ( g ` 0 ) = P ) ) ` 1 ) ) ) )
77 76 rexbidv 
 |-  ( z = ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. a ) /\ ( g ` 0 ) = P ) ) ` 1 ) -> ( E. f e. ( II Cn K ) ( ( f ` 0 ) = O /\ ( f ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = z ) <-> E. f e. ( II Cn K ) ( ( f ` 0 ) = O /\ ( f ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. a ) /\ ( g ` 0 ) = P ) ) ` 1 ) ) ) )
78 eqeq1 
 |-  ( z = ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. a ) /\ ( g ` 0 ) = P ) ) ` 1 ) -> ( z = w <-> ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. a ) /\ ( g ` 0 ) = P ) ) ` 1 ) = w ) )
79 78 imbi2d 
 |-  ( z = ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. a ) /\ ( g ` 0 ) = P ) ) ` 1 ) -> ( ( E. h e. ( II Cn K ) ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. h ) /\ ( g ` 0 ) = P ) ) ` 1 ) = w ) -> z = w ) <-> ( E. h e. ( II Cn K ) ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. h ) /\ ( g ` 0 ) = P ) ) ` 1 ) = w ) -> ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. a ) /\ ( g ` 0 ) = P ) ) ` 1 ) = w ) ) )
80 79 ralbidv 
 |-  ( z = ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. a ) /\ ( g ` 0 ) = P ) ) ` 1 ) -> ( A. w e. B ( E. h e. ( II Cn K ) ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. h ) /\ ( g ` 0 ) = P ) ) ` 1 ) = w ) -> z = w ) <-> A. w e. B ( E. h e. ( II Cn K ) ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. h ) /\ ( g ` 0 ) = P ) ) ` 1 ) = w ) -> ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. a ) /\ ( g ` 0 ) = P ) ) ` 1 ) = w ) ) )
81 77 80 anbi12d 
 |-  ( z = ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. a ) /\ ( g ` 0 ) = P ) ) ` 1 ) -> ( ( E. f e. ( II Cn K ) ( ( f ` 0 ) = O /\ ( f ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = z ) /\ A. w e. B ( E. h e. ( II Cn K ) ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. h ) /\ ( g ` 0 ) = P ) ) ` 1 ) = w ) -> z = w ) ) <-> ( E. f e. ( II Cn K ) ( ( f ` 0 ) = O /\ ( f ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. a ) /\ ( g ` 0 ) = P ) ) ` 1 ) ) /\ A. w e. B ( E. h e. ( II Cn K ) ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. h ) /\ ( g ` 0 ) = P ) ) ` 1 ) = w ) -> ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. a ) /\ ( g ` 0 ) = P ) ) ` 1 ) = w ) ) ) )
82 81 rspcev 
 |-  ( ( ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. a ) /\ ( g ` 0 ) = P ) ) ` 1 ) e. B /\ ( E. f e. ( II Cn K ) ( ( f ` 0 ) = O /\ ( f ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. a ) /\ ( g ` 0 ) = P ) ) ` 1 ) ) /\ A. w e. B ( E. h e. ( II Cn K ) ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. h ) /\ ( g ` 0 ) = P ) ) ` 1 ) = w ) -> ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. a ) /\ ( g ` 0 ) = P ) ) ` 1 ) = w ) ) ) -> E. z e. B ( E. f e. ( II Cn K ) ( ( f ` 0 ) = O /\ ( f ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = z ) /\ A. w e. B ( E. h e. ( II Cn K ) ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. h ) /\ ( g ` 0 ) = P ) ) ` 1 ) = w ) -> z = w ) ) )
83 40 55 74 82 syl12anc 
 |-  ( ( ( ph /\ X e. Y ) /\ ( a e. ( II Cn K ) /\ ( ( a ` 0 ) = O /\ ( a ` 1 ) = X ) ) ) -> E. z e. B ( E. f e. ( II Cn K ) ( ( f ` 0 ) = O /\ ( f ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = z ) /\ A. w e. B ( E. h e. ( II Cn K ) ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. h ) /\ ( g ` 0 ) = P ) ) ` 1 ) = w ) -> z = w ) ) )
84 fveq1 
 |-  ( f = h -> ( f ` 0 ) = ( h ` 0 ) )
85 84 eqeq1d 
 |-  ( f = h -> ( ( f ` 0 ) = O <-> ( h ` 0 ) = O ) )
86 fveq1 
 |-  ( f = h -> ( f ` 1 ) = ( h ` 1 ) )
87 86 eqeq1d 
 |-  ( f = h -> ( ( f ` 1 ) = X <-> ( h ` 1 ) = X ) )
88 coeq2 
 |-  ( f = h -> ( G o. f ) = ( G o. h ) )
89 88 eqeq2d 
 |-  ( f = h -> ( ( F o. g ) = ( G o. f ) <-> ( F o. g ) = ( G o. h ) ) )
90 89 anbi1d 
 |-  ( f = h -> ( ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) <-> ( ( F o. g ) = ( G o. h ) /\ ( g ` 0 ) = P ) ) )
91 90 riotabidv 
 |-  ( f = h -> ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) = ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. h ) /\ ( g ` 0 ) = P ) ) )
92 91 fveq1d 
 |-  ( f = h -> ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. h ) /\ ( g ` 0 ) = P ) ) ` 1 ) )
93 92 eqeq1d 
 |-  ( f = h -> ( ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = z <-> ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. h ) /\ ( g ` 0 ) = P ) ) ` 1 ) = z ) )
94 85 87 93 3anbi123d 
 |-  ( f = h -> ( ( ( f ` 0 ) = O /\ ( f ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = z ) <-> ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. h ) /\ ( g ` 0 ) = P ) ) ` 1 ) = z ) ) )
95 94 cbvrexvw 
 |-  ( E. f e. ( II Cn K ) ( ( f ` 0 ) = O /\ ( f ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = z ) <-> E. h e. ( II Cn K ) ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. h ) /\ ( g ` 0 ) = P ) ) ` 1 ) = z ) )
96 eqeq2 
 |-  ( z = w -> ( ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. h ) /\ ( g ` 0 ) = P ) ) ` 1 ) = z <-> ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. h ) /\ ( g ` 0 ) = P ) ) ` 1 ) = w ) )
97 96 3anbi3d 
 |-  ( z = w -> ( ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. h ) /\ ( g ` 0 ) = P ) ) ` 1 ) = z ) <-> ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. h ) /\ ( g ` 0 ) = P ) ) ` 1 ) = w ) ) )
98 97 rexbidv 
 |-  ( z = w -> ( E. h e. ( II Cn K ) ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. h ) /\ ( g ` 0 ) = P ) ) ` 1 ) = z ) <-> E. h e. ( II Cn K ) ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. h ) /\ ( g ` 0 ) = P ) ) ` 1 ) = w ) ) )
99 95 98 bitrid 
 |-  ( z = w -> ( E. f e. ( II Cn K ) ( ( f ` 0 ) = O /\ ( f ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = z ) <-> E. h e. ( II Cn K ) ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. h ) /\ ( g ` 0 ) = P ) ) ` 1 ) = w ) ) )
100 99 reu8 
 |-  ( E! z e. B E. f e. ( II Cn K ) ( ( f ` 0 ) = O /\ ( f ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = z ) <-> E. z e. B ( E. f e. ( II Cn K ) ( ( f ` 0 ) = O /\ ( f ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = z ) /\ A. w e. B ( E. h e. ( II Cn K ) ( ( h ` 0 ) = O /\ ( h ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. h ) /\ ( g ` 0 ) = P ) ) ` 1 ) = w ) -> z = w ) ) )
101 83 100 sylibr 
 |-  ( ( ( ph /\ X e. Y ) /\ ( a e. ( II Cn K ) /\ ( ( a ` 0 ) = O /\ ( a ` 1 ) = X ) ) ) -> E! z e. B E. f e. ( II Cn K ) ( ( f ` 0 ) = O /\ ( f ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = z ) )
102 101 rexlimdvaa 
 |-  ( ( ph /\ X e. Y ) -> ( E. a e. ( II Cn K ) ( ( a ` 0 ) = O /\ ( a ` 1 ) = X ) -> E! z e. B E. f e. ( II Cn K ) ( ( f ` 0 ) = O /\ ( f ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = z ) ) )
103 16 102 mpd 
 |-  ( ( ph /\ X e. Y ) -> E! z e. B E. f e. ( II Cn K ) ( ( f ` 0 ) = O /\ ( f ` 1 ) = X /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = z ) )