Theorem kelac1 30613

Description: Kelley's choice, basic form: if a collection of sets can be cast as closed sets in the factors of a topology, and there is a definable element in each topology (which need not be in the closed set - if it were this would be trivial), then compactness (via finite intersection) guarantees that the final product is nonempty. (Contributed by Stefan O'Rear, 22-Feb-2015.)

Hypotheses

Ref	Expression
kelac1.z	|- ( ( ph /\ x e. I ) -> S =/= (/) )
kelac1.j	|- ( ( ph /\ x e. I ) -> J e. Top )
kelac1.c	|- ( ( ph /\ x e. I ) -> C e. ( Clsd ` J ) )
kelac1.b	|- ( ( ph /\ x e. I ) -> B : S -1-1-onto-> C )
kelac1.u	|- ( ( ph /\ x e. I ) -> U e. U. J )
kelac1.k	|- ( ph -> ( Xt_ ` ( x e. I |-> J ) ) e. Comp )

Assertion

Ref	Expression
kelac1	|- ( ph -> X_ x e. I S =/= (/) )

Distinct variable groups:   ph, x   x, I

Allowed substitution hints:   B( x)   C( x)   S( x)   U( x)   J( x)

Proof of Theorem kelac1

Dummy variables f y z w are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		kelac1.c	. . . . . . 7 |- ( ( ph /\ x e. I ) -> C e. ( Clsd ` J ) )
2		eqid 2467	. . . . . . . 8 |- U. J = U. J
3	2	cldss 19296	. . . . . . 7 |- ( C e. ( Clsd ` J ) -> C C_ U. J )
4	1, 3	syl 16	. . . . . 6 |- ( ( ph /\ x e. I ) -> C C_ U. J )
5	4	ralrimiva 2878	. . . . 5 |- ( ph -> A. x e. I C C_ U. J )
6		boxriin 7508	. . . . 5 |- ( A. x e. I C C_ U. J -> X_ x e. I C = ( X_ x e. I U. J i^i |^|_ y e. I X_ x e. I if ( x = y , C , U. J ) ) )
7	5, 6	syl 16	. . . 4 |- ( ph -> X_ x e. I C = ( X_ x e. I U. J i^i |^|_ y e. I X_ x e. I if ( x = y , C , U. J ) ) )
8		kelac1.k	. . . . . . . . 9 |- ( ph -> ( Xt_ ` ( x e. I |-> J ) ) e. Comp )
9		cmptop 19661	. . . . . . . . 9 |- ( ( Xt_ ` ( x e. I |-> J ) ) e. Comp -> ( Xt_ ` ( x e. I |-> J ) ) e. Top )
10		0ntop 19181	. . . . . . . . . . 11 |- -. (/) e. Top
11		fvprc 5858	. . . . . . . . . . . 12 |- ( -. ( x e. I |-> J ) e. _V -> ( Xt_ ` ( x e. I |-> J ) ) = (/) )
12	11	eleq1d 2536	. . . . . . . . . . 11 |- ( -. ( x e. I |-> J ) e. _V -> ( ( Xt_ ` ( x e. I |-> J ) ) e. Top <-> (/) e. Top ) )
13	10, 12	mtbiri 303	. . . . . . . . . 10 |- ( -. ( x e. I |-> J ) e. _V -> -. ( Xt_ ` ( x e. I |-> J ) ) e. Top )
14	13	con4i 130	. . . . . . . . 9 |- ( ( Xt_ ` ( x e. I |-> J ) ) e. Top -> ( x e. I |-> J ) e. _V )
15	8, 9, 14	3syl 20	. . . . . . . 8 |- ( ph -> ( x e. I |-> J ) e. _V )
16		kelac1.j	. . . . . . . . 9 |- ( ( ph /\ x e. I ) -> J e. Top )
17		eqid 2467	. . . . . . . . 9 |- ( x e. I |-> J ) = ( x e. I |-> J )
18	16, 17	fmptd 6043	. . . . . . . 8 |- ( ph -> ( x e. I |-> J ) : I --> Top )
19		dmfex 6739	. . . . . . . 8 |- ( ( ( x e. I |-> J ) e. _V /\ ( x e. I |-> J ) : I --> Top ) -> I e. _V )
20	15, 18, 19	syl2anc 661	. . . . . . 7 |- ( ph -> I e. _V )
21	16	ralrimiva 2878	. . . . . . 7 |- ( ph -> A. x e. I J e. Top )
22		eqid 2467	. . . . . . . 8 |- ( Xt_ ` ( x e. I |-> J ) ) = ( Xt_ ` ( x e. I |-> J ) )
23	22	ptunimpt 19831	. . . . . . 7 |- ( ( I e. _V /\ A. x e. I J e. Top ) -> X_ x e. I U. J = U. ( Xt_ ` ( x e. I |-> J ) ) )
24	20, 21, 23	syl2anc 661	. . . . . 6 |- ( ph -> X_ x e. I U. J = U. ( Xt_ ` ( x e. I |-> J ) ) )
25	24	ineq1d 3699	. . . . 5 |- ( ph -> ( X_ x e. I U. J i^i |^|_ y e. I X_ x e. I if ( x = y , C , U. J ) ) = ( U. ( Xt_ ` ( x e. I |-> J ) ) i^i |^|_ y e. I X_ x e. I if ( x = y , C , U. J ) ) )
26		eqid 2467	. . . . . 6 |- U. ( Xt_ ` ( x e. I |-> J ) ) = U. ( Xt_ ` ( x e. I |-> J ) )
27	2	topcld 19302	. . . . . . . . . 10 |- ( J e. Top -> U. J e. ( Clsd ` J ) )
28	16, 27	syl 16	. . . . . . . . 9 |- ( ( ph /\ x e. I ) -> U. J e. ( Clsd ` J ) )
29		ifcl 3981	. . . . . . . . 9 |- ( ( C e. ( Clsd ` J ) /\ U. J e. ( Clsd ` J ) ) -> if ( x = y , C , U. J ) e. ( Clsd ` J ) )
30	1, 28, 29	syl2anc 661	. . . . . . . 8 |- ( ( ph /\ x e. I ) -> if ( x = y , C , U. J ) e. ( Clsd ` J ) )
31	20, 16, 30	ptcldmpt 19850	. . . . . . 7 |- ( ph -> X_ x e. I if ( x = y , C , U. J ) e. ( Clsd ` ( Xt_ ` ( x e. I |-> J ) ) ) )
32	31	adantr 465	. . . . . 6 |- ( ( ph /\ y e. I ) -> X_ x e. I if ( x = y , C , U. J ) e. ( Clsd ` ( Xt_ ` ( x e. I |-> J ) ) ) )
33		simprr 756	. . . . . . . 8 |- ( ( ph /\ ( z C_ I /\ z e. Fin ) ) -> z e. Fin )
34		kelac1.b	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. I ) -> B : S -1-1-onto-> C )
35		f1ofo 5821	. . . . . . . . . . . . . . 15 |- ( B : S -1-1-onto-> C -> B : S -onto-> C )
36		foima 5798	. . . . . . . . . . . . . . 15 |- ( B : S -onto-> C -> ( B " S ) = C )
37	34, 35, 36	3syl 20	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. I ) -> ( B " S ) = C )
38	37	eqcomd 2475	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. I ) -> C = ( B " S ) )
39		kelac1.z	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. I ) -> S =/= (/) )
40		f1ofn 5815	. . . . . . . . . . . . . . . . 17 |- ( B : S -1-1-onto-> C -> B Fn S )
41	34, 40	syl 16	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. I ) -> B Fn S )
42		ssid 3523	. . . . . . . . . . . . . . . 16 |- S C_ S
43		fnimaeq0 5700	. . . . . . . . . . . . . . . 16 |- ( ( B Fn S /\ S C_ S ) -> ( ( B " S ) = (/) <-> S = (/) ) )
44	41, 42, 43	sylancl 662	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. I ) -> ( ( B " S ) = (/) <-> S = (/) ) )
45	44	necon3bid 2725	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. I ) -> ( ( B " S ) =/= (/) <-> S =/= (/) ) )
46	39, 45	mpbird 232	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. I ) -> ( B " S ) =/= (/) )
47	38, 46	eqnetrd 2760	. . . . . . . . . . . 12 |- ( ( ph /\ x e. I ) -> C =/= (/) )
48		n0 3794	. . . . . . . . . . . 12 |- ( C =/= (/) <-> E. w w e. C )
49	47, 48	sylib 196	. . . . . . . . . . 11 |- ( ( ph /\ x e. I ) -> E. w w e. C )
50		rexv 3128	. . . . . . . . . . 11 |- ( E. w e. _V w e. C <-> E. w w e. C )
51	49, 50	sylibr 212	. . . . . . . . . 10 |- ( ( ph /\ x e. I ) -> E. w e. _V w e. C )
52	51	ralrimiva 2878	. . . . . . . . 9 |- ( ph -> A. x e. I E. w e. _V w e. C )
53		ssralv 3564	. . . . . . . . . 10 |- ( z C_ I -> ( A. x e. I E. w e. _V w e. C -> A. x e. z E. w e. _V w e. C ) )
54	53	adantr 465	. . . . . . . . 9 |- ( ( z C_ I /\ z e. Fin ) -> ( A. x e. I E. w e. _V w e. C -> A. x e. z E. w e. _V w e. C ) )
55	52, 54	mpan9 469	. . . . . . . 8 |- ( ( ph /\ ( z C_ I /\ z e. Fin ) ) -> A. x e. z E. w e. _V w e. C )
56		eleq1 2539	. . . . . . . . 9 |- ( w = ( f ` x ) -> ( w e. C <-> ( f ` x ) e. C ) )
57	56	ac6sfi 7760	. . . . . . . 8 |- ( ( z e. Fin /\ A. x e. z E. w e. _V w e. C ) -> E. f ( f : z --> _V /\ A. x e. z ( f ` x ) e. C ) )
58	33, 55, 57	syl2anc 661	. . . . . . 7 |- ( ( ph /\ ( z C_ I /\ z e. Fin ) ) -> E. f ( f : z --> _V /\ A. x e. z ( f ` x ) e. C ) )
59	24	eqcomd 2475	. . . . . . . . . . 11 |- ( ph -> U. ( Xt_ ` ( x e. I |-> J ) ) = X_ x e. I U. J )
60	59	ineq1d 3699	. . . . . . . . . 10 |- ( ph -> ( U. ( Xt_ ` ( x e. I |-> J ) ) i^i |^|_ y e. z X_ x e. I if ( x = y , C , U. J ) ) = ( X_ x e. I U. J i^i |^|_ y e. z X_ x e. I if ( x = y , C , U. J ) ) )
61	60	ad2antrr 725	. . . . . . . . 9 |- ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) -> ( U. ( Xt_ ` ( x e. I |-> J ) ) i^i |^|_ y e. z X_ x e. I if ( x = y , C , U. J ) ) = ( X_ x e. I U. J i^i |^|_ y e. z X_ x e. I if ( x = y , C , U. J ) ) )
62		iftrue 3945	. . . . . . . . . . . . . . . . . . 19 |- ( x e. z -> if ( x e. z , ( f ` x ) , U ) = ( f ` x ) )
63	62	ad2antrl 727	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ ( x e. z /\ ( f ` x ) e. C ) ) -> if ( x e. z , ( f ` x ) , U ) = ( f ` x ) )
64		simpll 753	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ x e. z ) -> ph )
65		simprl 755	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ( z C_ I /\ z e. Fin ) ) -> z C_ I )
66	65	sselda 3504	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ x e. z ) -> x e. I )
67	64, 66, 4	syl2anc 661	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ x e. z ) -> C C_ U. J )
68	67	sseld 3503	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ x e. z ) -> ( ( f ` x ) e. C -> ( f ` x ) e. U. J ) )
69	68	impr 619	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ ( x e. z /\ ( f ` x ) e. C ) ) -> ( f ` x ) e. U. J )
70	63, 69	eqeltrd 2555	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ ( x e. z /\ ( f ` x ) e. C ) ) -> if ( x e. z , ( f ` x ) , U ) e. U. J )
71	70	expr 615	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ x e. z ) -> ( ( f ` x ) e. C -> if ( x e. z , ( f ` x ) , U ) e. U. J ) )
72	71	ralimdva 2872	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( z C_ I /\ z e. Fin ) ) -> ( A. x e. z ( f ` x ) e. C -> A. x e. z if ( x e. z , ( f ` x ) , U ) e. U. J ) )
73	72	imp 429	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) -> A. x e. z if ( x e. z , ( f ` x ) , U ) e. U. J )
74		eldifn 3627	. . . . . . . . . . . . . . . . . . 19 |- ( x e. ( I \ z ) -> -. x e. z )
75		iffalse 3948	. . . . . . . . . . . . . . . . . . 19 |- ( -. x e. z -> if ( x e. z , ( f ` x ) , U ) = U )
76	74, 75	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( I \ z ) -> if ( x e. z , ( f ` x ) , U ) = U )
77	76	adantl 466	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. ( I \ z ) ) -> if ( x e. z , ( f ` x ) , U ) = U )
78		eldifi 3626	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( I \ z ) -> x e. I )
79		kelac1.u	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. I ) -> U e. U. J )
80	78, 79	sylan2 474	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. ( I \ z ) ) -> U e. U. J )
81	77, 80	eqeltrd 2555	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( I \ z ) ) -> if ( x e. z , ( f ` x ) , U ) e. U. J )
82	81	ralrimiva 2878	. . . . . . . . . . . . . . 15 |- ( ph -> A. x e. ( I \ z ) if ( x e. z , ( f ` x ) , U ) e. U. J )
83	82	ad2antrr 725	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) -> A. x e. ( I \ z ) if ( x e. z , ( f ` x ) , U ) e. U. J )
84		ralun 3686	. . . . . . . . . . . . . 14 |- ( ( A. x e. z if ( x e. z , ( f ` x ) , U ) e. U. J /\ A. x e. ( I \ z ) if ( x e. z , ( f ` x ) , U ) e. U. J ) -> A. x e. ( z u. ( I \ z ) ) if ( x e. z , ( f ` x ) , U ) e. U. J )
85	73, 83, 84	syl2anc 661	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) -> A. x e. ( z u. ( I \ z ) ) if ( x e. z , ( f ` x ) , U ) e. U. J )
86		undif 3907	. . . . . . . . . . . . . . . . 17 |- ( z C_ I <-> ( z u. ( I \ z ) ) = I )
87	86	biimpi 194	. . . . . . . . . . . . . . . 16 |- ( z C_ I -> ( z u. ( I \ z ) ) = I )
88	87	ad2antrl 727	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( z C_ I /\ z e. Fin ) ) -> ( z u. ( I \ z ) ) = I )
89	88	raleqdv 3064	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( z C_ I /\ z e. Fin ) ) -> ( A. x e. ( z u. ( I \ z ) ) if ( x e. z , ( f ` x ) , U ) e. U. J <-> A. x e. I if ( x e. z , ( f ` x ) , U ) e. U. J ) )
90	89	adantr 465	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) -> ( A. x e. ( z u. ( I \ z ) ) if ( x e. z , ( f ` x ) , U ) e. U. J <-> A. x e. I if ( x e. z , ( f ` x ) , U ) e. U. J ) )
91	85, 90	mpbid 210	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) -> A. x e. I if ( x e. z , ( f ` x ) , U ) e. U. J )
92	20	ad2antrr 725	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) -> I e. _V )
93		mptelixpg 7503	. . . . . . . . . . . . 13 |- ( I e. _V -> ( ( x e. I |-> if ( x e. z , ( f ` x ) , U ) ) e. X_ x e. I U. J <-> A. x e. I if ( x e. z , ( f ` x ) , U ) e. U. J ) )
94	92, 93	syl 16	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) -> ( ( x e. I |-> if ( x e. z , ( f ` x ) , U ) ) e. X_ x e. I U. J <-> A. x e. I if ( x e. z , ( f ` x ) , U ) e. U. J ) )
95	91, 94	mpbird 232	. . . . . . . . . . 11 |- ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) -> ( x e. I |-> if ( x e. z , ( f ` x ) , U ) ) e. X_ x e. I U. J )
96		eleq2 2540	. . . . . . . . . . . . . . . . . . . . . 22 |- ( C = if ( x = y , C , U. J ) -> ( ( f ` x ) e. C <-> ( f ` x ) e. if ( x = y , C , U. J ) ) )
97		eleq2 2540	. . . . . . . . . . . . . . . . . . . . . 22 |- ( U. J = if ( x = y , C , U. J ) -> ( ( f ` x ) e. U. J <-> ( f ` x ) e. if ( x = y , C , U. J ) ) )
98		simplrr 760	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ ( x e. z /\ ( f ` x ) e. C ) ) /\ x = y ) -> ( f ` x ) e. C )
99	69	adantr 465	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ ( x e. z /\ ( f ` x ) e. C ) ) /\ -. x = y ) -> ( f ` x ) e. U. J )
100	96, 97, 98, 99	ifbothda 3974	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ ( x e. z /\ ( f ` x ) e. C ) ) -> ( f ` x ) e. if ( x = y , C , U. J ) )
101	63, 100	eqeltrd 2555	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ ( x e. z /\ ( f ` x ) e. C ) ) -> if ( x e. z , ( f ` x ) , U ) e. if ( x = y , C , U. J ) )
102	101	expr 615	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ x e. z ) -> ( ( f ` x ) e. C -> if ( x e. z , ( f ` x ) , U ) e. if ( x = y , C , U. J ) ) )
103	102	ralimdva 2872	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ( z C_ I /\ z e. Fin ) ) -> ( A. x e. z ( f ` x ) e. C -> A. x e. z if ( x e. z , ( f ` x ) , U ) e. if ( x = y , C , U. J ) ) )
104	103	imp 429	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) -> A. x e. z if ( x e. z , ( f ` x ) , U ) e. if ( x = y , C , U. J ) )
105	104	adantr 465	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) /\ y e. z ) -> A. x e. z if ( x e. z , ( f ` x ) , U ) e. if ( x = y , C , U. J ) )
106	80	adantlr 714	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ y e. z ) /\ x e. ( I \ z ) ) -> U e. U. J )
107	76	adantl 466	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ y e. z ) /\ x e. ( I \ z ) ) -> if ( x e. z , ( f ` x ) , U ) = U )
108		incom 3691	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( I \ z ) i^i z ) = ( z i^i ( I \ z ) )
109		disjdif 3899	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( z i^i ( I \ z ) ) = (/)
110	108, 109	eqtri 2496	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( I \ z ) i^i z ) = (/)
111	110	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ y e. z ) /\ x e. ( I \ z ) ) -> ( ( I \ z ) i^i z ) = (/) )
112		simpr 461	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ y e. z ) /\ x e. ( I \ z ) ) -> x e. ( I \ z ) )
113		simplr 754	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ y e. z ) /\ x e. ( I \ z ) ) -> y e. z )
114		disjne 3872	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( I \ z ) i^i z ) = (/) /\ x e. ( I \ z ) /\ y e. z ) -> x =/= y )
115	111, 112, 113, 114	syl3anc 1228	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ y e. z ) /\ x e. ( I \ z ) ) -> x =/= y )
116	115	neneqd 2669	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ y e. z ) /\ x e. ( I \ z ) ) -> -. x = y )
117		iffalse 3948	. . . . . . . . . . . . . . . . . . . . 21 |- ( -. x = y -> if ( x = y , C , U. J ) = U. J )
118	116, 117	syl 16	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ y e. z ) /\ x e. ( I \ z ) ) -> if ( x = y , C , U. J ) = U. J )
119	106, 107, 118	3eltr4d 2570	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ y e. z ) /\ x e. ( I \ z ) ) -> if ( x e. z , ( f ` x ) , U ) e. if ( x = y , C , U. J ) )
120	119	ralrimiva 2878	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ y e. z ) -> A. x e. ( I \ z ) if ( x e. z , ( f ` x ) , U ) e. if ( x = y , C , U. J ) )
121	120	adantlr 714	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ y e. z ) -> A. x e. ( I \ z ) if ( x e. z , ( f ` x ) , U ) e. if ( x = y , C , U. J ) )
122	121	adantlr 714	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) /\ y e. z ) -> A. x e. ( I \ z ) if ( x e. z , ( f ` x ) , U ) e. if ( x = y , C , U. J ) )
123		ralun 3686	. . . . . . . . . . . . . . . 16 |- ( ( A. x e. z if ( x e. z , ( f ` x ) , U ) e. if ( x = y , C , U. J ) /\ A. x e. ( I \ z ) if ( x e. z , ( f ` x ) , U ) e. if ( x = y , C , U. J ) ) -> A. x e. ( z u. ( I \ z ) ) if ( x e. z , ( f ` x ) , U ) e. if ( x = y , C , U. J ) )
124	105, 122, 123	syl2anc 661	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) /\ y e. z ) -> A. x e. ( z u. ( I \ z ) ) if ( x e. z , ( f ` x ) , U ) e. if ( x = y , C , U. J ) )
125	88	raleqdv 3064	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( z C_ I /\ z e. Fin ) ) -> ( A. x e. ( z u. ( I \ z ) ) if ( x e. z , ( f ` x ) , U ) e. if ( x = y , C , U. J ) <-> A. x e. I if ( x e. z , ( f ` x ) , U ) e. if ( x = y , C , U. J ) ) )
126	125	ad2antrr 725	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) /\ y e. z ) -> ( A. x e. ( z u. ( I \ z ) ) if ( x e. z , ( f ` x ) , U ) e. if ( x = y , C , U. J ) <-> A. x e. I if ( x e. z , ( f ` x ) , U ) e. if ( x = y , C , U. J ) ) )
127	124, 126	mpbid 210	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) /\ y e. z ) -> A. x e. I if ( x e. z , ( f ` x ) , U ) e. if ( x = y , C , U. J ) )
128	20	ad3antrrr 729	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) /\ y e. z ) -> I e. _V )
129		mptelixpg 7503	. . . . . . . . . . . . . . 15 |- ( I e. _V -> ( ( x e. I |-> if ( x e. z , ( f ` x ) , U ) ) e. X_ x e. I if ( x = y , C , U. J ) <-> A. x e. I if ( x e. z , ( f ` x ) , U ) e. if ( x = y , C , U. J ) ) )
130	128, 129	syl 16	. . . . . . . . . . . . . 14 |- ( ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) /\ y e. z ) -> ( ( x e. I |-> if ( x e. z , ( f ` x ) , U ) ) e. X_ x e. I if ( x = y , C , U. J ) <-> A. x e. I if ( x e. z , ( f ` x ) , U ) e. if ( x = y , C , U. J ) ) )
131	127, 130	mpbird 232	. . . . . . . . . . . . 13 |- ( ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) /\ y e. z ) -> ( x e. I |-> if ( x e. z , ( f ` x ) , U ) ) e. X_ x e. I if ( x = y , C , U. J ) )
132	131	ralrimiva 2878	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) -> A. y e. z ( x e. I |-> if ( x e. z , ( f ` x ) , U ) ) e. X_ x e. I if ( x = y , C , U. J ) )
133		mptexg 6128	. . . . . . . . . . . . . . 15 |- ( I e. _V -> ( x e. I |-> if ( x e. z , ( f ` x ) , U ) ) e. _V )
134	20, 133	syl 16	. . . . . . . . . . . . . 14 |- ( ph -> ( x e. I |-> if ( x e. z , ( f ` x ) , U ) ) e. _V )
135	134	ad2antrr 725	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) -> ( x e. I |-> if ( x e. z , ( f ` x ) , U ) ) e. _V )
136		eliin 4331	. . . . . . . . . . . . 13 |- ( ( x e. I |-> if ( x e. z , ( f ` x ) , U ) ) e. _V -> ( ( x e. I |-> if ( x e. z , ( f ` x ) , U ) ) e. |^|_ y e. z X_ x e. I if ( x = y , C , U. J ) <-> A. y e. z ( x e. I |-> if ( x e. z , ( f ` x ) , U ) ) e. X_ x e. I if ( x = y , C , U. J ) ) )
137	135, 136	syl 16	. . . . . . . . . . . 12 |- ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) -> ( ( x e. I |-> if ( x e. z , ( f ` x ) , U ) ) e. |^|_ y e. z X_ x e. I if ( x = y , C , U. J ) <-> A. y e. z ( x e. I |-> if ( x e. z , ( f ` x ) , U ) ) e. X_ x e. I if ( x = y , C , U. J ) ) )
138	132, 137	mpbird 232	. . . . . . . . . . 11 |- ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) -> ( x e. I |-> if ( x e. z , ( f ` x ) , U ) ) e. |^|_ y e. z X_ x e. I if ( x = y , C , U. J ) )
139	95, 138	elind 3688	. . . . . . . . . 10 |- ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) -> ( x e. I |-> if ( x e. z , ( f ` x ) , U ) ) e. ( X_ x e. I U. J i^i |^|_ y e. z X_ x e. I if ( x = y , C , U. J ) ) )
140		ne0i 3791	. . . . . . . . . 10 |- ( ( x e. I |-> if ( x e. z , ( f ` x ) , U ) ) e. ( X_ x e. I U. J i^i |^|_ y e. z X_ x e. I if ( x = y , C , U. J ) ) -> ( X_ x e. I U. J i^i |^|_ y e. z X_ x e. I if ( x = y , C , U. J ) ) =/= (/) )
141	139, 140	syl 16	. . . . . . . . 9 |- ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) -> ( X_ x e. I U. J i^i |^|_ y e. z X_ x e. I if ( x = y , C , U. J ) ) =/= (/) )
142	61, 141	eqnetrd 2760	. . . . . . . 8 |- ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) -> ( U. ( Xt_ ` ( x e. I |-> J ) ) i^i |^|_ y e. z X_ x e. I if ( x = y , C , U. J ) ) =/= (/) )
143	142	adantrl 715	. . . . . . 7 |- ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ ( f : z --> _V /\ A. x e. z ( f ` x ) e. C ) ) -> ( U. ( Xt_ ` ( x e. I |-> J ) ) i^i |^|_ y e. z X_ x e. I if ( x = y , C , U. J ) ) =/= (/) )
144	58, 143	exlimddv 1702	. . . . . 6 |- ( ( ph /\ ( z C_ I /\ z e. Fin ) ) -> ( U. ( Xt_ ` ( x e. I |-> J ) ) i^i |^|_ y e. z X_ x e. I if ( x = y , C , U. J ) ) =/= (/) )
145	26, 8, 32, 144	cmpfiiin 30233	. . . . 5 |- ( ph -> ( U. ( Xt_ ` ( x e. I |-> J ) ) i^i |^|_ y e. I X_ x e. I if ( x = y , C , U. J ) ) =/= (/) )
146	25, 145	eqnetrd 2760	. . . 4 |- ( ph -> ( X_ x e. I U. J i^i |^|_ y e. I X_ x e. I if ( x = y , C , U. J ) ) =/= (/) )
147	7, 146	eqnetrd 2760	. . 3 |- ( ph -> X_ x e. I C =/= (/) )
148		n0 3794	. . 3 |- ( X_ x e. I C =/= (/) <-> E. y y e. X_ x e. I C )
149	147, 148	sylib 196	. 2 |- ( ph -> E. y y e. X_ x e. I C )
150		elixp2 7470	. . . . . 6 |- ( y e. X_ x e. I C <-> ( y e. _V /\ y Fn I /\ A. x e. I ( y ` x ) e. C ) )
151	150	simp3bi 1013	. . . . 5 |- ( y e. X_ x e. I C -> A. x e. I ( y ` x ) e. C )
152		f1ocnv 5826	. . . . . . . 8 |- ( B : S -1-1-onto-> C -> `' B : C -1-1-onto-> S )
153		f1of 5814	. . . . . . . 8 |- ( `' B : C -1-1-onto-> S -> `' B : C --> S )
154		ffvelrn 6017	. . . . . . . . 9 |- ( ( `' B : C --> S /\ ( y ` x ) e. C ) -> ( `' B ` ( y ` x ) ) e. S )
155	154	ex 434	. . . . . . . 8 |- ( `' B : C --> S -> ( ( y ` x ) e. C -> ( `' B ` ( y ` x ) ) e. S ) )
156	34, 152, 153, 155	4syl 21	. . . . . . 7 |- ( ( ph /\ x e. I ) -> ( ( y ` x ) e. C -> ( `' B ` ( y ` x ) ) e. S ) )
157	156	ralimdva 2872	. . . . . 6 |- ( ph -> ( A. x e. I ( y ` x ) e. C -> A. x e. I ( `' B ` ( y ` x ) ) e. S ) )
158	157	imp 429	. . . . 5 |- ( ( ph /\ A. x e. I ( y ` x ) e. C ) -> A. x e. I ( `' B ` ( y ` x ) ) e. S )
159	151, 158	sylan2 474	. . . 4 |- ( ( ph /\ y e. X_ x e. I C ) -> A. x e. I ( `' B ` ( y ` x ) ) e. S )
160		mptelixpg 7503	. . . . . 6 |- ( I e. _V -> ( ( x e. I |-> ( `' B ` ( y ` x ) ) ) e. X_ x e. I S <-> A. x e. I ( `' B ` ( y ` x ) ) e. S ) )
161	20, 160	syl 16	. . . . 5 |- ( ph -> ( ( x e. I |-> ( `' B ` ( y ` x ) ) ) e. X_ x e. I S <-> A. x e. I ( `' B ` ( y ` x ) ) e. S ) )
162	161	adantr 465	. . . 4 |- ( ( ph /\ y e. X_ x e. I C ) -> ( ( x e. I |-> ( `' B ` ( y ` x ) ) ) e. X_ x e. I S <-> A. x e. I ( `' B ` ( y ` x ) ) e. S ) )
163	159, 162	mpbird 232	. . 3 |- ( ( ph /\ y e. X_ x e. I C ) -> ( x e. I |-> ( `' B ` ( y ` x ) ) ) e. X_ x e. I S )
164		ne0i 3791	. . 3 |- ( ( x e. I |-> ( `' B ` ( y ` x ) ) ) e. X_ x e. I S -> X_ x e. I S =/= (/) )
165	163, 164	syl 16	. 2 |- ( ( ph /\ y e. X_ x e. I C ) -> X_ x e. I S =/= (/) )
166	149, 165	exlimddv 1702	1 |- ( ph -> X_ x e. I S =/= (/) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1379   E.wex 1596   e. wcel 1767   =/= wne 2662   A.wral 2814   E.wrex 2815   _Vcvv 3113   \ cdif 3473   u. cun 3474   i^i cin 3475   C_ wss 3476   (/)c0 3785   ifcif 3939   U.cuni 4245   |^|_ciin 4326   |-> cmpt 4505   `'ccnv 4998   "cima 5002   Fn wfn 5581   -->wf 5582   -onto->wfo 5584   -1-1-onto->wf1o 5585   ` cfv 5586   X_cixp 7466   Fincfn 7513   Xt_cpt 14690   Topctop 19161   Clsdccld 19283   Compccmp 19652

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6574

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-reu 2821  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-int 4283  df-iun 4327  df-iin 4328  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5549  df-fun 5588  df-fn 5589  df-f 5590  df-f1 5591  df-fo 5592  df-f1o 5593  df-fv 5594  df-ov 6285  df-oprab 6286  df-mpt2 6287  df-om 6679  df-1st 6781  df-2nd 6782  df-recs 7039  df-rdg 7073  df-1o 7127  df-2o 7128  df-oadd 7131  df-er 7308  df-map 7419  df-ixp 7467  df-en 7514  df-dom 7515  df-sdom 7516  df-fin 7517  df-fi 7867  df-topgen 14695  df-pt 14696  df-top 19166  df-bases 19168  df-cld 19286  df-cmp 19653

This theorem is referenced by:  kelac2  30615