Theorem ptpjopn 21415

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

Hypotheses

Ref	Expression
ptpjcn.1	|- Y = U. J
ptpjcn.2	|- J = ( Xt_ ` F )

Assertion

Ref	Expression
ptpjopn	|- ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) -> ( ( x e. Y |-> ( x ` I ) ) " U ) e. ( F ` I ) )

Distinct variable groups:   x, A   x, F   x, I   x, V   x, Y   x, U

Allowed substitution hint:   J( x)

Proof of Theorem ptpjopn

Dummy variables g k n s w y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-ima 5127	. . 3 |- ( ( x e. Y |-> ( x ` I ) ) " U ) = ran ( ( x e. Y |-> ( x ` I ) ) |` U )
2		elssuni 4467	. . . . . . 7 |- ( U e. J -> U C_ U. J )
3		ptpjcn.1	. . . . . . 7 |- Y = U. J
4	2, 3	syl6sseqr 3652	. . . . . 6 |- ( U e. J -> U C_ Y )
5	4	adantl 482	. . . . 5 |- ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) -> U C_ Y )
6	5	resmptd 5452	. . . 4 |- ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) -> ( ( x e. Y |-> ( x ` I ) ) |` U ) = ( x e. U |-> ( x ` I ) ) )
7	6	rneqd 5353	. . 3 |- ( ( ( 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 ) ) )
8	1, 7	syl5eq 2668	. 2 |- ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) -> ( ( x e. Y |-> ( x ` I ) ) " U ) = ran ( x e. U |-> ( x ` I ) ) )
9		ptpjcn.2	. . . . . . . . . . 11 |- J = ( Xt_ ` F )
10		ffn 6045	. . . . . . . . . . . 12 |- ( F : A --> Top -> F Fn A )
11		eqid 2622	. . . . . . . . . . . . 13 |- { 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 21373	. . . . . . . . . . . 12 |- ( ( 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 491	. . . . . . . . . . 11 |- ( ( 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	9, 13	syl5eq 2668	. . . . . . . . . 10 |- ( ( 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 1081	. . . . . . . . 9 |- ( ( 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 2687	. . . . . . . 8 |- ( ( 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 501	. . . . . . 7 |- ( ( ( 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 20769	. . . . . . 7 |- ( ( 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 488	. . . . . 6 |- ( ( ( ( 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 3203	. . . . . . . . 9 |- w e. _V
21		eqeq1 2626	. . . . . . . . . . 11 |- ( s = w -> ( s = X_ y e. A ( g ` y ) <-> w = X_ y e. A ( g ` y ) ) )
22	21	anbi2d 740	. . . . . . . . . 10 |- ( 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 1850	. . . . . . . . 9 |- ( 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 3350	. . . . . . . 8 |- ( 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		simpl3 1066	. . . . . . . . . . . . . . 15 |- ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) -> I e. A )
26	25	ad3antrrr 766	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( 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 )
27		simplr2 1104	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( 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 ) )
28		fveq2 6191	. . . . . . . . . . . . . . . 16 |- ( y = I -> ( g ` y ) = ( g ` I ) )
29		fveq2 6191	. . . . . . . . . . . . . . . 16 |- ( y = I -> ( F ` y ) = ( F ` I ) )
30	28, 29	eleq12d 2695	. . . . . . . . . . . . . . 15 |- ( y = I -> ( ( g ` y ) e. ( F ` y ) <-> ( g ` I ) e. ( F ` I ) ) )
31	30	rspcv 3305	. . . . . . . . . . . . . 14 |- ( I e. A -> ( A. y e. A ( g ` y ) e. ( F ` y ) -> ( g ` I ) e. ( F ` I ) ) )
32	26, 27, 31	sylc 65	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( 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 ) )
33		vex 3203	. . . . . . . . . . . . . . . . 17 |- s e. _V
34	33	elixp 7915	. . . . . . . . . . . . . . . 16 |- ( s e. X_ y e. A ( g ` y ) <-> ( s Fn A /\ A. y e. A ( s ` y ) e. ( g ` y ) ) )
35	34	simprbi 480	. . . . . . . . . . . . . . 15 |- ( s e. X_ y e. A ( g ` y ) -> A. y e. A ( s ` y ) e. ( g ` y ) )
36	35	ad2antrl 764	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( 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 ) )
37		fveq2 6191	. . . . . . . . . . . . . . . 16 |- ( y = I -> ( s ` y ) = ( s ` I ) )
38	37, 28	eleq12d 2695	. . . . . . . . . . . . . . 15 |- ( y = I -> ( ( s ` y ) e. ( g ` y ) <-> ( s ` I ) e. ( g ` I ) ) )
39	38	rspcv 3305	. . . . . . . . . . . . . 14 |- ( I e. A -> ( A. y e. A ( s ` y ) e. ( g ` y ) -> ( s ` I ) e. ( g ` I ) ) )
40	26, 36, 39	sylc 65	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( 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 ) )
41		simplrr 801	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( 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 )
42		simplrl 800	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( ( ( ( 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 ) )
43		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( n = I -> ( g ` n ) = ( g ` I ) )
44	43	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( ( ( ( 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 ) )
45	42, 44	eleqtrrd 2704	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ( ( ( 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 ) )
46		simprr 796	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ( ( 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 )
47		simplrl 800	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ( ( ( 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, 35	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ( ( 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		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( y = n -> ( s ` y ) = ( s ` n ) )
50		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( y = n -> ( g ` y ) = ( g ` n ) )
51	49, 50	eleq12d 2695	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( y = n -> ( ( s ` y ) e. ( g ` y ) <-> ( s ` n ) e. ( g ` n ) ) )
52	51	rspcv 3305	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( n e. A -> ( A. y e. A ( s ` y ) e. ( g ` y ) -> ( s ` n ) e. ( g ` n ) ) )
53	46, 48, 52	sylc 65	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( ( ( 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 ) )
54	53	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ( ( ( 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 ) )
55	45, 54	ifclda 4120	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ( ( 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 ) )
56	55	anassrs 680	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ( ( ( 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 ) )
57	56	ralrimiva 2966	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ( ( 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 ) )
58		simpll1 1100	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) /\ s e. U ) -> A e. V )
59	58	ad3antrrr 766	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ( ( 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 )
60		mptelixpg 7945	. . . . . . . . . . . . . . . . . . . . 21 |- ( 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 ) ) )
61	59, 60	syl 17	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ( ( 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 ) ) )
62	57, 61	mpbird 247	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( ( 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 ) )
63		fveq2 6191	. . . . . . . . . . . . . . . . . . . 20 |- ( n = y -> ( g ` n ) = ( g ` y ) )
64	63	cbvixpv 7926	. . . . . . . . . . . . . . . . . . 19 |- X_ n e. A ( g ` n ) = X_ y e. A ( g ` y )
65	62, 64	syl6eleq 2711	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( 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 ) )
66	41, 65	sseldd 3604	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( 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 )
67	26	adantr 481	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( ( 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 )
68		iftrue 4092	. . . . . . . . . . . . . . . . . . . 20 |- ( n = I -> if ( n = I , k , ( s ` n ) ) = k )
69		eqid 2622	. . . . . . . . . . . . . . . . . . . 20 |- ( n e. A |-> if ( n = I , k , ( s ` n ) ) ) = ( n e. A |-> if ( n = I , k , ( s ` n ) ) )
70		vex 3203	. . . . . . . . . . . . . . . . . . . 20 |- k e. _V
71	68, 69, 70	fvmpt 6282	. . . . . . . . . . . . . . . . . . 19 |- ( I e. A -> ( ( n e. A |-> if ( n = I , k , ( s ` n ) ) ) ` I ) = k )
72	67, 71	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( 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 )
73	72	eqcomd 2628	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( 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 ) )
74		fveq1 6190	. . . . . . . . . . . . . . . . . . 19 |- ( x = ( n e. A |-> if ( n = I , k , ( s ` n ) ) ) -> ( x ` I ) = ( ( n e. A |-> if ( n = I , k , ( s ` n ) ) ) ` I ) )
75	74	eqeq2d 2632	. . . . . . . . . . . . . . . . . 18 |- ( x = ( n e. A |-> if ( n = I , k , ( s ` n ) ) ) -> ( k = ( x ` I ) <-> k = ( ( n e. A |-> if ( n = I , k , ( s ` n ) ) ) ` I ) ) )
76	75	rspcev 3309	. . . . . . . . . . . . . . . . 17 |- ( ( ( 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 ) )
77	66, 73, 76	syl2anc 693	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( 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 ) )
78		eqid 2622	. . . . . . . . . . . . . . . . . 18 |- ( x e. U |-> ( x ` I ) ) = ( x e. U |-> ( x ` I ) )
79	78	elrnmpt 5372	. . . . . . . . . . . . . . . . 17 |- ( k e. _V -> ( k e. ran ( x e. U |-> ( x ` I ) ) <-> E. x e. U k = ( x ` I ) ) )
80	70, 79	ax-mp 5	. . . . . . . . . . . . . . . 16 |- ( k e. ran ( x e. U |-> ( x ` I ) ) <-> E. x e. U k = ( x ` I ) )
81	77, 80	sylibr 224	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( ( 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 ) ) )
82	81	ex 450	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( 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 ) ) ) )
83	82	ssrdv 3609	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( 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 ) ) )
84		eleq2 2690	. . . . . . . . . . . . . . 15 |- ( z = ( g ` I ) -> ( ( s ` I ) e. z <-> ( s ` I ) e. ( g ` I ) ) )
85		sseq1 3626	. . . . . . . . . . . . . . 15 |- ( z = ( g ` I ) -> ( z C_ ran ( x e. U |-> ( x ` I ) ) <-> ( g ` I ) C_ ran ( x e. U |-> ( x ` I ) ) ) )
86	84, 85	anbi12d 747	. . . . . . . . . . . . . 14 |- ( 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 ) ) ) ) )
87	86	rspcev 3309	. . . . . . . . . . . . 13 |- ( ( ( 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 ) ) ) )
88	32, 40, 83, 87	syl12anc 1324	. . . . . . . . . . . 12 |- ( ( ( ( ( ( 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 ) ) ) )
89	88	ex 450	. . . . . . . . . . 11 |- ( ( ( ( ( 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 ) ) ) ) )
90		eleq2 2690	. . . . . . . . . . . . 13 |- ( w = X_ y e. A ( g ` y ) -> ( s e. w <-> s e. X_ y e. A ( g ` y ) ) )
91		sseq1 3626	. . . . . . . . . . . . 13 |- ( w = X_ y e. A ( g ` y ) -> ( w C_ U <-> X_ y e. A ( g ` y ) C_ U ) )
92	90, 91	anbi12d 747	. . . . . . . . . . . 12 |- ( 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 ) ) )
93	92	imbi1d 331	. . . . . . . . . . 11 |- ( 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 ) ) ) ) ) )
94	89, 93	syl5ibrcom 237	. . . . . . . . . 10 |- ( ( ( ( ( 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 ) ) ) ) ) )
95	94	expimpd 629	. . . . . . . . 9 |- ( ( ( ( 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 ) ) ) ) ) )
96	95	exlimdv 1861	. . . . . . . 8 |- ( ( ( ( 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 ) ) ) ) ) )
97	24, 96	syl5bi 232	. . . . . . 7 |- ( ( ( ( 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 ) ) ) ) ) )
98	97	rexlimdv 3030	. . . . . 6 |- ( ( ( ( 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 ) ) ) ) )
99	19, 98	mpd 15	. . . . 5 |- ( ( ( ( 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 ) ) ) )
100	99	ralrimiva 2966	. . . 4 |- ( ( ( 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 ) ) ) )
101		fvex 6201	. . . . . 6 |- ( s ` I ) e. _V
102	101	rgenw 2924	. . . . 5 |- A. s e. U ( s ` I ) e. _V
103		fveq1 6190	. . . . . . 7 |- ( x = s -> ( x ` I ) = ( s ` I ) )
104	103	cbvmptv 4750	. . . . . 6 |- ( x e. U |-> ( x ` I ) ) = ( s e. U |-> ( s ` I ) )
105		eleq1 2689	. . . . . . . 8 |- ( y = ( s ` I ) -> ( y e. z <-> ( s ` I ) e. z ) )
106	105	anbi1d 741	. . . . . . 7 |- ( 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 ) ) ) ) )
107	106	rexbidv 3052	. . . . . 6 |- ( 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 ) ) ) ) )
108	104, 107	ralrnmpt 6368	. . . . 5 |- ( 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 ) ) ) ) )
109	102, 108	ax-mp 5	. . . 4 |- ( 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 ) ) ) )
110	100, 109	sylibr 224	. . 3 |- ( ( ( 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 ) ) ) )
111		simpl2 1065	. . . . 5 |- ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) -> F : A --> Top )
112	111, 25	ffvelrnd 6360	. . . 4 |- ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) -> ( F ` I ) e. Top )
113		eltop2 20779	. . . 4 |- ( ( 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 ) ) ) ) )
114	112, 113	syl 17	. . 3 |- ( ( ( 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 ) ) ) ) )
115	110, 114	mpbird 247	. 2 |- ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) -> ran ( x e. U |-> ( x ` I ) ) e. ( F ` I ) )
116	8, 115	eqeltrd 2701	1 |- ( ( ( A e. V /\ F : A --> Top /\ I e. A ) /\ U e. J ) -> ( ( x e. Y |-> ( x ` I ) ) " U ) e. ( F ` I ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   E.wex 1704   e. wcel 1990   {cab 2608   A.wral 2912   E.wrex 2913   _Vcvv 3200   \ cdif 3571   C_ wss 3574   ifcif 4086   U.cuni 4436   |-> cmpt 4729   ran crn 5115   |` cres 5116   "cima 5117   Fn wfn 5883   -->wf 5884   ` cfv 5888   X_cixp 7908   Fincfn 7955   topGenctg 16098   Xt_cpt 16099   Topctop 20698

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ixp 7909  df-topgen 16104  df-pt 16105  df-top 20699

This theorem is referenced by: (None)