Metamath Proof Explorer

Theorem ptpjopn

Description: The projection map is an open map. (Contributed by Mario Carneiro, 2-Sep-2015)

Ref Expression
Hypotheses ptpjcn.1 
|- Y = U. J
ptpjcn.2 
|- J = ( Xt_ ` F )
Assertion ptpjopn 
|- ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) -> ( ( x e. Y |-> ( x ` I ) ) " U ) e. ( F ` I ) )

Proof

Step Hyp Ref Expression
1 ptpjcn.1 
 |-  Y = U. J
2 ptpjcn.2 
 |-  J = ( Xt_ ` F )
3 df-ima 
 |-  ( ( x e. Y |-> ( x ` I ) ) " U ) = ran ( ( x e. Y |-> ( x ` I ) ) |` U )
4 elssuni 
 |-  ( U e. J -> U C_ U. J )
5 4 1 sseqtrrdi 
 |-  ( U e. J -> U C_ Y )
6 5 adantl 
 |-  ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) -> U C_ Y )
7 6 resmptd 
 |-  ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) -> ( ( x e. Y |-> ( x ` I ) ) |` U ) = ( x e. U |-> ( x ` I ) ) )
8 7 rneqd 
 |-  ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) -> ran ( ( x e. Y |-> ( x ` I ) ) |` U ) = ran ( x e. U |-> ( x ` I ) ) )
9 3 8 eqtrid 
 |-  ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) -> ( ( x e. Y |-> ( x ` I ) ) " U ) = ran ( x e. U |-> ( x ` I ) ) )
10 ffn 
 |-  ( F : A --> Top -> F Fn A )
11 eqid 
 |-  { s | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ s = X_ y e. A ( g ` y ) ) } = { s | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ s = X_ y e. A ( g ` y ) ) }
12 11 ptval 
 |-  ( ( A e. V /\ F Fn A ) -> ( Xt_ ` F ) = ( topGen ` { s | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ s = X_ y e. A ( g ` y ) ) } ) )
13 10 12 sylan2 
 |-  ( ( A e. V /\ F : A --> Top ) -> ( Xt_ ` F ) = ( topGen ` { s | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ s = X_ y e. A ( g ` y ) ) } ) )
14 2 13 eqtrid 
 |-  ( ( A e. V /\ F : A --> Top ) -> J = ( topGen ` { s | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ s = X_ y e. A ( g ` y ) ) } ) )
15 14 3adant3 
 |-  ( ( A e. V /\ F : A --> Top /\ I e. A ) -> J = ( topGen ` { s | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ s = X_ y e. A ( g ` y ) ) } ) )
16 15 eleq2d 
 |-  ( ( A e. V /\ F : A --> Top /\ I e. A ) -> ( U e. J <-> U e. ( topGen ` { s | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ s = X_ y e. A ( g ` y ) ) } ) ) )
17 16 biimpa 
 |-  ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) -> U e. ( topGen ` { s | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ s = X_ y e. A ( g ` y ) ) } ) )
18 tg2 
 |-  ( ( U e. ( topGen ` { s | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ s = X_ y e. A ( g ` y ) ) } ) /\ s e. U ) -> E. w e. { s | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ s = X_ y e. A ( g ` y ) ) } ( s e. w /\ w C_ U ) )
19 17 18 sylan 
 |-  ( ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) /\ s e. U ) -> E. w e. { s | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ s = X_ y e. A ( g ` y ) ) } ( s e. w /\ w C_ U ) )
20 vex 
 |-  w e. _V
21 eqeq1 
 |-  ( s = w -> ( s = X_ y e. A ( g ` y ) <-> w = X_ y e. A ( g ` y ) ) )
22 21 anbi2d 
 |-  ( s = w -> ( ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ s = X_ y e. A ( g ` y ) ) <-> ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ w = X_ y e. A ( g ` y ) ) ) )
23 22 exbidv 
 |-  ( s = w -> ( E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ s = X_ y e. A ( g ` y ) ) <-> E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ w = X_ y e. A ( g ` y ) ) ) )
24 20 23 elab 
 |-  ( w e. { s | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ s = X_ y e. A ( g ` y ) ) } <-> E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ w = X_ y e. A ( g ` y ) ) )
25 fveq2 
 |-  ( y = I -> ( g ` y ) = ( g ` I ) )
26 fveq2 
 |-  ( y = I -> ( F ` y ) = ( F ` I ) )
27 25 26 eleq12d 
 |-  ( y = I -> ( ( g ` y ) e. ( F ` y ) <-> ( g ` I ) e. ( F ` I ) ) )
28 simplr2 
 |-  ( ( ( ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) /\ s e. U ) /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) ) /\ ( s e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ U ) ) -> A. y e. A ( g ` y ) e. ( F ` y ) )
29 simpl3 
 |-  ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) -> I e. A )
30 29 ad3antrrr 
 |-  ( ( ( ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) /\ s e. U ) /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) ) /\ ( s e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ U ) ) -> I e. A )
31 27 28 30 rspcdva 
 |-  ( ( ( ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) /\ s e. U ) /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) ) /\ ( s e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ U ) ) -> ( g ` I ) e. ( F ` I ) )
32 fveq2 
 |-  ( y = I -> ( s ` y ) = ( s ` I ) )
33 32 25 eleq12d 
 |-  ( y = I -> ( ( s ` y ) e. ( g ` y ) <-> ( s ` I ) e. ( g ` I ) ) )
34 vex 
 |-  s e. _V
35 34 elixp 
 |-  ( s e. X_ y e. A ( g ` y ) <-> ( s Fn A /\ A. y e. A ( s ` y ) e. ( g ` y ) ) )
36 35 simprbi 
 |-  ( s e. X_ y e. A ( g ` y ) -> A. y e. A ( s ` y ) e. ( g ` y ) )
37 36 ad2antrl 
 |-  ( ( ( ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) /\ s e. U ) /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) ) /\ ( s e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ U ) ) -> A. y e. A ( s ` y ) e. ( g ` y ) )
38 33 37 30 rspcdva 
 |-  ( ( ( ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) /\ s e. U ) /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) ) /\ ( s e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ U ) ) -> ( s ` I ) e. ( g ` I ) )
39 simplrr 
 |-  ( ( ( ( ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) /\ s e. U ) /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) ) /\ ( s e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ U ) ) /\ k e. ( g ` I ) ) -> X_ y e. A ( g ` y ) C_ U )
40 simplrl 
 |-  ( ( ( ( ( ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) /\ s e. U ) /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) ) /\ ( s e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ U ) ) /\ ( k e. ( g ` I ) /\ n e. A ) ) /\ n = I ) -> k e. ( g ` I ) )
41 fveq2 
 |-  ( n = I -> ( g ` n ) = ( g ` I ) )
42 41 adantl 
 |-  ( ( ( ( ( ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) /\ s e. U ) /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) ) /\ ( s e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ U ) ) /\ ( k e. ( g ` I ) /\ n e. A ) ) /\ n = I ) -> ( g ` n ) = ( g ` I ) )
43 40 42 eleqtrrd 
 |-  ( ( ( ( ( ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) /\ s e. U ) /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) ) /\ ( s e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ U ) ) /\ ( k e. ( g ` I ) /\ n e. A ) ) /\ n = I ) -> k e. ( g ` n ) )
44 fveq2 
 |-  ( y = n -> ( s ` y ) = ( s ` n ) )
45 fveq2 
 |-  ( y = n -> ( g ` y ) = ( g ` n ) )
46 44 45 eleq12d 
 |-  ( y = n -> ( ( s ` y ) e. ( g ` y ) <-> ( s ` n ) e. ( g ` n ) ) )
47 simplrl 
 |-  ( ( ( ( ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) /\ s e. U ) /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) ) /\ ( s e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ U ) ) /\ ( k e. ( g ` I ) /\ n e. A ) ) -> s e. X_ y e. A ( g ` y ) )
48 47 36 syl 
 |-  ( ( ( ( ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) /\ s e. U ) /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) ) /\ ( s e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ U ) ) /\ ( k e. ( g ` I ) /\ n e. A ) ) -> A. y e. A ( s ` y ) e. ( g ` y ) )
49 simprr 
 |-  ( ( ( ( ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) /\ s e. U ) /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) ) /\ ( s e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ U ) ) /\ ( k e. ( g ` I ) /\ n e. A ) ) -> n e. A )
50 46 48 49 rspcdva 
 |-  ( ( ( ( ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) /\ s e. U ) /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) ) /\ ( s e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ U ) ) /\ ( k e. ( g ` I ) /\ n e. A ) ) -> ( s ` n ) e. ( g ` n ) )
51 50 adantr 
 |-  ( ( ( ( ( ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) /\ s e. U ) /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) ) /\ ( s e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ U ) ) /\ ( k e. ( g ` I ) /\ n e. A ) ) /\ -. n = I ) -> ( s ` n ) e. ( g ` n ) )
52 43 51 ifclda 
 |-  ( ( ( ( ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) /\ s e. U ) /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) ) /\ ( s e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ U ) ) /\ ( k e. ( g ` I ) /\ n e. A ) ) -> if ( n = I , k , ( s ` n ) ) e. ( g ` n ) )
53 52 anassrs 
 |-  ( ( ( ( ( ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) /\ s e. U ) /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) ) /\ ( s e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ U ) ) /\ k e. ( g ` I ) ) /\ n e. A ) -> if ( n = I , k , ( s ` n ) ) e. ( g ` n ) )
54 53 ralrimiva 
 |-  ( ( ( ( ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) /\ s e. U ) /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) ) /\ ( s e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ U ) ) /\ k e. ( g ` I ) ) -> A. n e. A if ( n = I , k , ( s ` n ) ) e. ( g ` n ) )
55 simpll1 
 |-  ( ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) /\ s e. U ) -> A e. V )
56 55 ad3antrrr 
 |-  ( ( ( ( ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) /\ s e. U ) /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) ) /\ ( s e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ U ) ) /\ k e. ( g ` I ) ) -> A e. V )
57 mptelixpg 
 |-  ( A e. V -> ( ( n e. A |-> if ( n = I , k , ( s ` n ) ) ) e. X_ n e. A ( g ` n ) <-> A. n e. A if ( n = I , k , ( s ` n ) ) e. ( g ` n ) ) )
58 56 57 syl 
 |-  ( ( ( ( ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) /\ s e. U ) /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) ) /\ ( s e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ U ) ) /\ k e. ( g ` I ) ) -> ( ( n e. A |-> if ( n = I , k , ( s ` n ) ) ) e. X_ n e. A ( g ` n ) <-> A. n e. A if ( n = I , k , ( s ` n ) ) e. ( g ` n ) ) )
59 54 58 mpbird 
 |-  ( ( ( ( ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) /\ s e. U ) /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) ) /\ ( s e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ U ) ) /\ k e. ( g ` I ) ) -> ( n e. A |-> if ( n = I , k , ( s ` n ) ) ) e. X_ n e. A ( g ` n ) )
60 fveq2 
 |-  ( n = y -> ( g ` n ) = ( g ` y ) )
61 60 cbvixpv 
 |-  X_ n e. A ( g ` n ) = X_ y e. A ( g ` y )
62 59 61 eleqtrdi 
 |-  ( ( ( ( ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) /\ s e. U ) /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) ) /\ ( s e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ U ) ) /\ k e. ( g ` I ) ) -> ( n e. A |-> if ( n = I , k , ( s ` n ) ) ) e. X_ y e. A ( g ` y ) )
63 39 62 sseldd 
 |-  ( ( ( ( ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) /\ s e. U ) /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) ) /\ ( s e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ U ) ) /\ k e. ( g ` I ) ) -> ( n e. A |-> if ( n = I , k , ( s ` n ) ) ) e. U )
64 30 adantr 
 |-  ( ( ( ( ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) /\ s e. U ) /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) ) /\ ( s e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ U ) ) /\ k e. ( g ` I ) ) -> I e. A )
65 iftrue 
 |-  ( n = I -> if ( n = I , k , ( s ` n ) ) = k )
66 eqid 
 |-  ( n e. A |-> if ( n = I , k , ( s ` n ) ) ) = ( n e. A |-> if ( n = I , k , ( s ` n ) ) )
67 vex 
 |-  k e. _V
68 65 66 67 fvmpt 
 |-  ( I e. A -> ( ( n e. A |-> if ( n = I , k , ( s ` n ) ) ) ` I ) = k )
69 64 68 syl 
 |-  ( ( ( ( ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) /\ s e. U ) /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) ) /\ ( s e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ U ) ) /\ k e. ( g ` I ) ) -> ( ( n e. A |-> if ( n = I , k , ( s ` n ) ) ) ` I ) = k )
70 69 eqcomd 
 |-  ( ( ( ( ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) /\ s e. U ) /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) ) /\ ( s e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ U ) ) /\ k e. ( g ` I ) ) -> k = ( ( n e. A |-> if ( n = I , k , ( s ` n ) ) ) ` I ) )
71 fveq1 
 |-  ( x = ( n e. A |-> if ( n = I , k , ( s ` n ) ) ) -> ( x ` I ) = ( ( n e. A |-> if ( n = I , k , ( s ` n ) ) ) ` I ) )
72 71 rspceeqv 
 |-  ( ( ( n e. A |-> if ( n = I , k , ( s ` n ) ) ) e. U /\ k = ( ( n e. A |-> if ( n = I , k , ( s ` n ) ) ) ` I ) ) -> E. x e. U k = ( x ` I ) )
73 63 70 72 syl2anc 
 |-  ( ( ( ( ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) /\ s e. U ) /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) ) /\ ( s e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ U ) ) /\ k e. ( g ` I ) ) -> E. x e. U k = ( x ` I ) )
74 eqid 
 |-  ( x e. U |-> ( x ` I ) ) = ( x e. U |-> ( x ` I ) )
75 74 elrnmpt 
 |-  ( k e. _V -> ( k e. ran ( x e. U |-> ( x ` I ) ) <-> E. x e. U k = ( x ` I ) ) )
76 75 elv 
 |-  ( k e. ran ( x e. U |-> ( x ` I ) ) <-> E. x e. U k = ( x ` I ) )
77 73 76 sylibr 
 |-  ( ( ( ( ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) /\ s e. U ) /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) ) /\ ( s e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ U ) ) /\ k e. ( g ` I ) ) -> k e. ran ( x e. U |-> ( x ` I ) ) )
78 77 ex 
 |-  ( ( ( ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) /\ s e. U ) /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) ) /\ ( s e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ U ) ) -> ( k e. ( g ` I ) -> k e. ran ( x e. U |-> ( x ` I ) ) ) )
79 78 ssrdv 
 |-  ( ( ( ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) /\ s e. U ) /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) ) /\ ( s e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ U ) ) -> ( g ` I ) C_ ran ( x e. U |-> ( x ` I ) ) )
80 eleq2 
 |-  ( z = ( g ` I ) -> ( ( s ` I ) e. z <-> ( s ` I ) e. ( g ` I ) ) )
81 sseq1 
 |-  ( z = ( g ` I ) -> ( z C_ ran ( x e. U |-> ( x ` I ) ) <-> ( g ` I ) C_ ran ( x e. U |-> ( x ` I ) ) ) )
82 80 81 anbi12d 
 |-  ( z = ( g ` I ) -> ( ( ( s ` I ) e. z /\ z C_ ran ( x e. U |-> ( x ` I ) ) ) <-> ( ( s ` I ) e. ( g ` I ) /\ ( g ` I ) C_ ran ( x e. U |-> ( x ` I ) ) ) ) )
83 82 rspcev 
 |-  ( ( ( g ` I ) e. ( F ` I ) /\ ( ( s ` I ) e. ( g ` I ) /\ ( g ` I ) C_ ran ( x e. U |-> ( x ` I ) ) ) ) -> E. z e. ( F ` I ) ( ( s ` I ) e. z /\ z C_ ran ( x e. U |-> ( x ` I ) ) ) )
84 31 38 79 83 syl12anc 
 |-  ( ( ( ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) /\ s e. U ) /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) ) /\ ( s e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ U ) ) -> E. z e. ( F ` I ) ( ( s ` I ) e. z /\ z C_ ran ( x e. U |-> ( x ` I ) ) ) )
85 84 ex 
 |-  ( ( ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) /\ s e. U ) /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) ) -> ( ( s e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ U ) -> E. z e. ( F ` I ) ( ( s ` I ) e. z /\ z C_ ran ( x e. U |-> ( x ` I ) ) ) ) )
86 eleq2 
 |-  ( w = X_ y e. A ( g ` y ) -> ( s e. w <-> s e. X_ y e. A ( g ` y ) ) )
87 sseq1 
 |-  ( w = X_ y e. A ( g ` y ) -> ( w C_ U <-> X_ y e. A ( g ` y ) C_ U ) )
88 86 87 anbi12d 
 |-  ( w = X_ y e. A ( g ` y ) -> ( ( s e. w /\ w C_ U ) <-> ( s e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ U ) ) )
89 88 imbi1d 
 |-  ( w = X_ y e. A ( g ` y ) -> ( ( ( s e. w /\ w C_ U ) -> E. z e. ( F ` I ) ( ( s ` I ) e. z /\ z C_ ran ( x e. U |-> ( x ` I ) ) ) ) <-> ( ( s e. X_ y e. A ( g ` y ) /\ X_ y e. A ( g ` y ) C_ U ) -> E. z e. ( F ` I ) ( ( s ` I ) e. z /\ z C_ ran ( x e. U |-> ( x ` I ) ) ) ) ) )
90 85 89 syl5ibrcom 
 |-  ( ( ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) /\ s e. U ) /\ ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) ) -> ( w = X_ y e. A ( g ` y ) -> ( ( s e. w /\ w C_ U ) -> E. z e. ( F ` I ) ( ( s ` I ) e. z /\ z C_ ran ( x e. U |-> ( x ` I ) ) ) ) ) )
91 90 expimpd 
 |-  ( ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) /\ s e. U ) -> ( ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ w = X_ y e. A ( g ` y ) ) -> ( ( s e. w /\ w C_ U ) -> E. z e. ( F ` I ) ( ( s ` I ) e. z /\ z C_ ran ( x e. U |-> ( x ` I ) ) ) ) ) )
92 91 exlimdv 
 |-  ( ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) /\ s e. U ) -> ( E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ w = X_ y e. A ( g ` y ) ) -> ( ( s e. w /\ w C_ U ) -> E. z e. ( F ` I ) ( ( s ` I ) e. z /\ z C_ ran ( x e. U |-> ( x ` I ) ) ) ) ) )
93 24 92 biimtrid 
 |-  ( ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) /\ s e. U ) -> ( w e. { s | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ s = X_ y e. A ( g ` y ) ) } -> ( ( s e. w /\ w C_ U ) -> E. z e. ( F ` I ) ( ( s ` I ) e. z /\ z C_ ran ( x e. U |-> ( x ` I ) ) ) ) ) )
94 93 rexlimdv 
 |-  ( ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) /\ s e. U ) -> ( E. w e. { s | E. g ( ( g Fn A /\ A. y e. A ( g ` y ) e. ( F ` y ) /\ E. z e. Fin A. y e. ( A \ z ) ( g ` y ) = U. ( F ` y ) ) /\ s = X_ y e. A ( g ` y ) ) } ( s e. w /\ w C_ U ) -> E. z e. ( F ` I ) ( ( s ` I ) e. z /\ z C_ ran ( x e. U |-> ( x ` I ) ) ) ) )
95 19 94 mpd 
 |-  ( ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) /\ s e. U ) -> E. z e. ( F ` I ) ( ( s ` I ) e. z /\ z C_ ran ( x e. U |-> ( x ` I ) ) ) )
96 95 ralrimiva 
 |-  ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) -> A. s e. U E. z e. ( F ` I ) ( ( s ` I ) e. z /\ z C_ ran ( x e. U |-> ( x ` I ) ) ) )
97 fvex 
 |-  ( s ` I ) e. _V
98 97 rgenw 
 |-  A. s e. U ( s ` I ) e. _V
99 fveq1 
 |-  ( x = s -> ( x ` I ) = ( s ` I ) )
100 99 cbvmptv 
 |-  ( x e. U |-> ( x ` I ) ) = ( s e. U |-> ( s ` I ) )
101 eleq1 
 |-  ( y = ( s ` I ) -> ( y e. z <-> ( s ` I ) e. z ) )
102 101 anbi1d 
 |-  ( y = ( s ` I ) -> ( ( y e. z /\ z C_ ran ( x e. U |-> ( x ` I ) ) ) <-> ( ( s ` I ) e. z /\ z C_ ran ( x e. U |-> ( x ` I ) ) ) ) )
103 102 rexbidv 
 |-  ( y = ( s ` I ) -> ( E. z e. ( F ` I ) ( y e. z /\ z C_ ran ( x e. U |-> ( x ` I ) ) ) <-> E. z e. ( F ` I ) ( ( s ` I ) e. z /\ z C_ ran ( x e. U |-> ( x ` I ) ) ) ) )
104 100 103 ralrnmptw 
 |-  ( A. s e. U ( s ` I ) e. _V -> ( A. y e. ran ( x e. U |-> ( x ` I ) ) E. z e. ( F ` I ) ( y e. z /\ z C_ ran ( x e. U |-> ( x ` I ) ) ) <-> A. s e. U E. z e. ( F ` I ) ( ( s ` I ) e. z /\ z C_ ran ( x e. U |-> ( x ` I ) ) ) ) )
105 98 104 ax-mp 
 |-  ( A. y e. ran ( x e. U |-> ( x ` I ) ) E. z e. ( F ` I ) ( y e. z /\ z C_ ran ( x e. U |-> ( x ` I ) ) ) <-> A. s e. U E. z e. ( F ` I ) ( ( s ` I ) e. z /\ z C_ ran ( x e. U |-> ( x ` I ) ) ) )
106 96 105 sylibr 
 |-  ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) -> A. y e. ran ( x e. U |-> ( x ` I ) ) E. z e. ( F ` I ) ( y e. z /\ z C_ ran ( x e. U |-> ( x ` I ) ) ) )
107 simpl2 
 |-  ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) -> F : A --> Top )
108 107 29 ffvelcdmd 
 |-  ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) -> ( F ` I ) e. Top )
109 eltop2 
 |-  ( ( F ` I ) e. Top -> ( ran ( x e. U |-> ( x ` I ) ) e. ( F ` I ) <-> A. y e. ran ( x e. U |-> ( x ` I ) ) E. z e. ( F ` I ) ( y e. z /\ z C_ ran ( x e. U |-> ( x ` I ) ) ) ) )
110 108 109 syl 
 |-  ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) -> ( ran ( x e. U |-> ( x ` I ) ) e. ( F ` I ) <-> A. y e. ran ( x e. U |-> ( x ` I ) ) E. z e. ( F ` I ) ( y e. z /\ z C_ ran ( x e. U |-> ( x ` I ) ) ) ) )
111 106 110 mpbird 
 |-  ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) -> ran ( x e. U |-> ( x ` I ) ) e. ( F ` I ) )
112 9 111 eqeltrd 
 |-  ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) -> ( ( x e. Y |-> ( x ` I ) ) " U ) e. ( F ` I ) )