Metamath Proof Explorer

Theorem cvmopnlem

Description: Lemma for cvmopn . (Contributed by Mario Carneiro, 7-May-2015)

Ref Expression
Hypotheses cvmcov.1 
|- S = ( k e. J |-> { s e. ( ~P C \ { (/) } ) | ( U. s = ( `' F " k ) /\ A. u e. s ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t k ) ) ) ) } )
cvmseu.1 
|- B = U. C
Assertion cvmopnlem 
|- ( ( F e. ( C CovMap J ) /\ A e. C ) -> ( F " A ) e. J )

Proof

Step Hyp Ref Expression
1 cvmcov.1 
 |-  S = ( k e. J |-> { s e. ( ~P C \ { (/) } ) | ( U. s = ( `' F " k ) /\ A. u e. s ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t k ) ) ) ) } )
2 cvmseu.1 
 |-  B = U. C
3 simpll 
 |-  ( ( ( F e. ( C CovMap J ) /\ A e. C ) /\ z e. A ) -> F e. ( C CovMap J ) )
4 cvmcn 
 |-  ( F e. ( C CovMap J ) -> F e. ( C Cn J ) )
5 4 adantr 
 |-  ( ( F e. ( C CovMap J ) /\ A e. C ) -> F e. ( C Cn J ) )
6 eqid 
 |-  U. J = U. J
7 2 6 cnf 
 |-  ( F e. ( C Cn J ) -> F : B --> U. J )
8 5 7 syl 
 |-  ( ( F e. ( C CovMap J ) /\ A e. C ) -> F : B --> U. J )
9 8 adantr 
 |-  ( ( ( F e. ( C CovMap J ) /\ A e. C ) /\ z e. A ) -> F : B --> U. J )
10 elssuni 
 |-  ( A e. C -> A C_ U. C )
11 10 2 sseqtrrdi 
 |-  ( A e. C -> A C_ B )
12 11 adantl 
 |-  ( ( F e. ( C CovMap J ) /\ A e. C ) -> A C_ B )
13 12 sselda 
 |-  ( ( ( F e. ( C CovMap J ) /\ A e. C ) /\ z e. A ) -> z e. B )
14 9 13 ffvelrnd 
 |-  ( ( ( F e. ( C CovMap J ) /\ A e. C ) /\ z e. A ) -> ( F ` z ) e. U. J )
15 1 6 cvmcov 
 |-  ( ( F e. ( C CovMap J ) /\ ( F ` z ) e. U. J ) -> E. t e. J ( ( F ` z ) e. t /\ ( S ` t ) =/= (/) ) )
16 3 14 15 syl2anc 
 |-  ( ( ( F e. ( C CovMap J ) /\ A e. C ) /\ z e. A ) -> E. t e. J ( ( F ` z ) e. t /\ ( S ` t ) =/= (/) ) )
17 n0 
 |-  ( ( S ` t ) =/= (/) <-> E. w w e. ( S ` t ) )
18 inss2 
 |-  ( A i^i ( iota_ x e. w z e. x ) ) C_ ( iota_ x e. w z e. x )
19 resima2 
 |-  ( ( A i^i ( iota_ x e. w z e. x ) ) C_ ( iota_ x e. w z e. x ) -> ( ( F |` ( iota_ x e. w z e. x ) ) " ( A i^i ( iota_ x e. w z e. x ) ) ) = ( F " ( A i^i ( iota_ x e. w z e. x ) ) ) )
20 18 19 ax-mp 
 |-  ( ( F |` ( iota_ x e. w z e. x ) ) " ( A i^i ( iota_ x e. w z e. x ) ) ) = ( F " ( A i^i ( iota_ x e. w z e. x ) ) )
21 simprr 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ A e. C ) /\ z e. A ) /\ ( ( F ` z ) e. t /\ w e. ( S ` t ) ) ) -> w e. ( S ` t ) )
22 3 adantr 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ A e. C ) /\ z e. A ) /\ ( ( F ` z ) e. t /\ w e. ( S ` t ) ) ) -> F e. ( C CovMap J ) )
23 13 adantr 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ A e. C ) /\ z e. A ) /\ ( ( F ` z ) e. t /\ w e. ( S ` t ) ) ) -> z e. B )
24 simprl 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ A e. C ) /\ z e. A ) /\ ( ( F ` z ) e. t /\ w e. ( S ` t ) ) ) -> ( F ` z ) e. t )
25 eqid 
 |-  ( iota_ x e. w z e. x ) = ( iota_ x e. w z e. x )
26 1 2 25 cvmsiota 
 |-  ( ( F e. ( C CovMap J ) /\ ( w e. ( S ` t ) /\ z e. B /\ ( F ` z ) e. t ) ) -> ( ( iota_ x e. w z e. x ) e. w /\ z e. ( iota_ x e. w z e. x ) ) )
27 22 21 23 24 26 syl13anc 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ A e. C ) /\ z e. A ) /\ ( ( F ` z ) e. t /\ w e. ( S ` t ) ) ) -> ( ( iota_ x e. w z e. x ) e. w /\ z e. ( iota_ x e. w z e. x ) ) )
28 27 simpld 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ A e. C ) /\ z e. A ) /\ ( ( F ` z ) e. t /\ w e. ( S ` t ) ) ) -> ( iota_ x e. w z e. x ) e. w )
29 1 cvmshmeo 
 |-  ( ( w e. ( S ` t ) /\ ( iota_ x e. w z e. x ) e. w ) -> ( F |` ( iota_ x e. w z e. x ) ) e. ( ( C |`t ( iota_ x e. w z e. x ) ) Homeo ( J |`t t ) ) )
30 21 28 29 syl2anc 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ A e. C ) /\ z e. A ) /\ ( ( F ` z ) e. t /\ w e. ( S ` t ) ) ) -> ( F |` ( iota_ x e. w z e. x ) ) e. ( ( C |`t ( iota_ x e. w z e. x ) ) Homeo ( J |`t t ) ) )
31 cvmtop1 
 |-  ( F e. ( C CovMap J ) -> C e. Top )
32 22 31 syl 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ A e. C ) /\ z e. A ) /\ ( ( F ` z ) e. t /\ w e. ( S ` t ) ) ) -> C e. Top )
33 simpllr 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ A e. C ) /\ z e. A ) /\ ( ( F ` z ) e. t /\ w e. ( S ` t ) ) ) -> A e. C )
34 elrestr 
 |-  ( ( C e. Top /\ ( iota_ x e. w z e. x ) e. w /\ A e. C ) -> ( A i^i ( iota_ x e. w z e. x ) ) e. ( C |`t ( iota_ x e. w z e. x ) ) )
35 32 28 33 34 syl3anc 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ A e. C ) /\ z e. A ) /\ ( ( F ` z ) e. t /\ w e. ( S ` t ) ) ) -> ( A i^i ( iota_ x e. w z e. x ) ) e. ( C |`t ( iota_ x e. w z e. x ) ) )
36 hmeoima 
 |-  ( ( ( F |` ( iota_ x e. w z e. x ) ) e. ( ( C |`t ( iota_ x e. w z e. x ) ) Homeo ( J |`t t ) ) /\ ( A i^i ( iota_ x e. w z e. x ) ) e. ( C |`t ( iota_ x e. w z e. x ) ) ) -> ( ( F |` ( iota_ x e. w z e. x ) ) " ( A i^i ( iota_ x e. w z e. x ) ) ) e. ( J |`t t ) )
37 30 35 36 syl2anc 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ A e. C ) /\ z e. A ) /\ ( ( F ` z ) e. t /\ w e. ( S ` t ) ) ) -> ( ( F |` ( iota_ x e. w z e. x ) ) " ( A i^i ( iota_ x e. w z e. x ) ) ) e. ( J |`t t ) )
38 20 37 eqeltrrid 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ A e. C ) /\ z e. A ) /\ ( ( F ` z ) e. t /\ w e. ( S ` t ) ) ) -> ( F " ( A i^i ( iota_ x e. w z e. x ) ) ) e. ( J |`t t ) )
39 cvmtop2 
 |-  ( F e. ( C CovMap J ) -> J e. Top )
40 39 adantr 
 |-  ( ( F e. ( C CovMap J ) /\ A e. C ) -> J e. Top )
41 40 ad2antrr 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ A e. C ) /\ z e. A ) /\ ( ( F ` z ) e. t /\ w e. ( S ` t ) ) ) -> J e. Top )
42 1 cvmsrcl 
 |-  ( w e. ( S ` t ) -> t e. J )
43 42 ad2antll 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ A e. C ) /\ z e. A ) /\ ( ( F ` z ) e. t /\ w e. ( S ` t ) ) ) -> t e. J )
44 restopn2 
 |-  ( ( J e. Top /\ t e. J ) -> ( ( F " ( A i^i ( iota_ x e. w z e. x ) ) ) e. ( J |`t t ) <-> ( ( F " ( A i^i ( iota_ x e. w z e. x ) ) ) e. J /\ ( F " ( A i^i ( iota_ x e. w z e. x ) ) ) C_ t ) ) )
45 41 43 44 syl2anc 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ A e. C ) /\ z e. A ) /\ ( ( F ` z ) e. t /\ w e. ( S ` t ) ) ) -> ( ( F " ( A i^i ( iota_ x e. w z e. x ) ) ) e. ( J |`t t ) <-> ( ( F " ( A i^i ( iota_ x e. w z e. x ) ) ) e. J /\ ( F " ( A i^i ( iota_ x e. w z e. x ) ) ) C_ t ) ) )
46 38 45 mpbid 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ A e. C ) /\ z e. A ) /\ ( ( F ` z ) e. t /\ w e. ( S ` t ) ) ) -> ( ( F " ( A i^i ( iota_ x e. w z e. x ) ) ) e. J /\ ( F " ( A i^i ( iota_ x e. w z e. x ) ) ) C_ t ) )
47 46 simpld 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ A e. C ) /\ z e. A ) /\ ( ( F ` z ) e. t /\ w e. ( S ` t ) ) ) -> ( F " ( A i^i ( iota_ x e. w z e. x ) ) ) e. J )
48 8 ffnd 
 |-  ( ( F e. ( C CovMap J ) /\ A e. C ) -> F Fn B )
49 48 ad2antrr 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ A e. C ) /\ z e. A ) /\ ( ( F ` z ) e. t /\ w e. ( S ` t ) ) ) -> F Fn B )
50 inss1 
 |-  ( A i^i ( iota_ x e. w z e. x ) ) C_ A
51 33 11 syl 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ A e. C ) /\ z e. A ) /\ ( ( F ` z ) e. t /\ w e. ( S ` t ) ) ) -> A C_ B )
52 50 51 sstrid 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ A e. C ) /\ z e. A ) /\ ( ( F ` z ) e. t /\ w e. ( S ` t ) ) ) -> ( A i^i ( iota_ x e. w z e. x ) ) C_ B )
53 simplr 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ A e. C ) /\ z e. A ) /\ ( ( F ` z ) e. t /\ w e. ( S ` t ) ) ) -> z e. A )
54 27 simprd 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ A e. C ) /\ z e. A ) /\ ( ( F ` z ) e. t /\ w e. ( S ` t ) ) ) -> z e. ( iota_ x e. w z e. x ) )
55 53 54 elind 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ A e. C ) /\ z e. A ) /\ ( ( F ` z ) e. t /\ w e. ( S ` t ) ) ) -> z e. ( A i^i ( iota_ x e. w z e. x ) ) )
56 fnfvima 
 |-  ( ( F Fn B /\ ( A i^i ( iota_ x e. w z e. x ) ) C_ B /\ z e. ( A i^i ( iota_ x e. w z e. x ) ) ) -> ( F ` z ) e. ( F " ( A i^i ( iota_ x e. w z e. x ) ) ) )
57 49 52 55 56 syl3anc 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ A e. C ) /\ z e. A ) /\ ( ( F ` z ) e. t /\ w e. ( S ` t ) ) ) -> ( F ` z ) e. ( F " ( A i^i ( iota_ x e. w z e. x ) ) ) )
58 imass2 
 |-  ( ( A i^i ( iota_ x e. w z e. x ) ) C_ A -> ( F " ( A i^i ( iota_ x e. w z e. x ) ) ) C_ ( F " A ) )
59 50 58 mp1i 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ A e. C ) /\ z e. A ) /\ ( ( F ` z ) e. t /\ w e. ( S ` t ) ) ) -> ( F " ( A i^i ( iota_ x e. w z e. x ) ) ) C_ ( F " A ) )
60 eleq2 
 |-  ( y = ( F " ( A i^i ( iota_ x e. w z e. x ) ) ) -> ( ( F ` z ) e. y <-> ( F ` z ) e. ( F " ( A i^i ( iota_ x e. w z e. x ) ) ) ) )
61 sseq1 
 |-  ( y = ( F " ( A i^i ( iota_ x e. w z e. x ) ) ) -> ( y C_ ( F " A ) <-> ( F " ( A i^i ( iota_ x e. w z e. x ) ) ) C_ ( F " A ) ) )
62 60 61 anbi12d 
 |-  ( y = ( F " ( A i^i ( iota_ x e. w z e. x ) ) ) -> ( ( ( F ` z ) e. y /\ y C_ ( F " A ) ) <-> ( ( F ` z ) e. ( F " ( A i^i ( iota_ x e. w z e. x ) ) ) /\ ( F " ( A i^i ( iota_ x e. w z e. x ) ) ) C_ ( F " A ) ) ) )
63 62 rspcev 
 |-  ( ( ( F " ( A i^i ( iota_ x e. w z e. x ) ) ) e. J /\ ( ( F ` z ) e. ( F " ( A i^i ( iota_ x e. w z e. x ) ) ) /\ ( F " ( A i^i ( iota_ x e. w z e. x ) ) ) C_ ( F " A ) ) ) -> E. y e. J ( ( F ` z ) e. y /\ y C_ ( F " A ) ) )
64 47 57 59 63 syl12anc 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ A e. C ) /\ z e. A ) /\ ( ( F ` z ) e. t /\ w e. ( S ` t ) ) ) -> E. y e. J ( ( F ` z ) e. y /\ y C_ ( F " A ) ) )
65 64 expr 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ A e. C ) /\ z e. A ) /\ ( F ` z ) e. t ) -> ( w e. ( S ` t ) -> E. y e. J ( ( F ` z ) e. y /\ y C_ ( F " A ) ) ) )
66 65 exlimdv 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ A e. C ) /\ z e. A ) /\ ( F ` z ) e. t ) -> ( E. w w e. ( S ` t ) -> E. y e. J ( ( F ` z ) e. y /\ y C_ ( F " A ) ) ) )
67 17 66 syl5bi 
 |-  ( ( ( ( F e. ( C CovMap J ) /\ A e. C ) /\ z e. A ) /\ ( F ` z ) e. t ) -> ( ( S ` t ) =/= (/) -> E. y e. J ( ( F ` z ) e. y /\ y C_ ( F " A ) ) ) )
68 67 expimpd 
 |-  ( ( ( F e. ( C CovMap J ) /\ A e. C ) /\ z e. A ) -> ( ( ( F ` z ) e. t /\ ( S ` t ) =/= (/) ) -> E. y e. J ( ( F ` z ) e. y /\ y C_ ( F " A ) ) ) )
69 68 rexlimdvw 
 |-  ( ( ( F e. ( C CovMap J ) /\ A e. C ) /\ z e. A ) -> ( E. t e. J ( ( F ` z ) e. t /\ ( S ` t ) =/= (/) ) -> E. y e. J ( ( F ` z ) e. y /\ y C_ ( F " A ) ) ) )
70 16 69 mpd 
 |-  ( ( ( F e. ( C CovMap J ) /\ A e. C ) /\ z e. A ) -> E. y e. J ( ( F ` z ) e. y /\ y C_ ( F " A ) ) )
71 70 ralrimiva 
 |-  ( ( F e. ( C CovMap J ) /\ A e. C ) -> A. z e. A E. y e. J ( ( F ` z ) e. y /\ y C_ ( F " A ) ) )
72 eleq1 
 |-  ( x = ( F ` z ) -> ( x e. y <-> ( F ` z ) e. y ) )
73 72 anbi1d 
 |-  ( x = ( F ` z ) -> ( ( x e. y /\ y C_ ( F " A ) ) <-> ( ( F ` z ) e. y /\ y C_ ( F " A ) ) ) )
74 73 rexbidv 
 |-  ( x = ( F ` z ) -> ( E. y e. J ( x e. y /\ y C_ ( F " A ) ) <-> E. y e. J ( ( F ` z ) e. y /\ y C_ ( F " A ) ) ) )
75 74 ralima 
 |-  ( ( F Fn B /\ A C_ B ) -> ( A. x e. ( F " A ) E. y e. J ( x e. y /\ y C_ ( F " A ) ) <-> A. z e. A E. y e. J ( ( F ` z ) e. y /\ y C_ ( F " A ) ) ) )
76 48 12 75 syl2anc 
 |-  ( ( F e. ( C CovMap J ) /\ A e. C ) -> ( A. x e. ( F " A ) E. y e. J ( x e. y /\ y C_ ( F " A ) ) <-> A. z e. A E. y e. J ( ( F ` z ) e. y /\ y C_ ( F " A ) ) ) )
77 71 76 mpbird 
 |-  ( ( F e. ( C CovMap J ) /\ A e. C ) -> A. x e. ( F " A ) E. y e. J ( x e. y /\ y C_ ( F " A ) ) )
78 eltop2 
 |-  ( J e. Top -> ( ( F " A ) e. J <-> A. x e. ( F " A ) E. y e. J ( x e. y /\ y C_ ( F " A ) ) ) )
79 40 78 syl 
 |-  ( ( F e. ( C CovMap J ) /\ A e. C ) -> ( ( F " A ) e. J <-> A. x e. ( F " A ) E. y e. J ( x e. y /\ y C_ ( F " A ) ) ) )
80 77 79 mpbird 
 |-  ( ( F e. ( C CovMap J ) /\ A e. C ) -> ( F " A ) e. J )