Theorem kelac1 29263

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 2435	. . . . . . . 8 |- U. J = U. J
3	2	cldss 18477	. . . . . . 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 2791	. . . . 5 |- ( ph -> A. x e. I C C_ U. J )
6		boxriin 7295	. . . . 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 18842	. . . . . . . . 9 |- ( ( Xt_ ` ( x e. I |-> J ) ) e. Comp -> ( Xt_ ` ( x e. I |-> J ) ) e. Top )
10		0ntop 18362	. . . . . . . . . . 11 |- -. (/) e. Top
11		fvprc 5675	. . . . . . . . . . . 12 |- ( -. ( x e. I |-> J ) e. _V -> ( Xt_ ` ( x e. I |-> J ) ) = (/) )
12	11	eleq1d 2501	. . . . . . . . . . 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 2435	. . . . . . . . 9 |- ( x e. I |-> J ) = ( x e. I |-> J )
18	16, 17	fmptd 5857	. . . . . . . 8 |- ( ph -> ( x e. I |-> J ) : I --> Top )
19		dmfex 6526	. . . . . . . 8 |- ( ( ( x e. I |-> J ) e. _V /\ ( x e. I |-> J ) : I --> Top ) -> I e. _V )
20	15, 18, 19	syl2anc 656	. . . . . . 7 |- ( ph -> I e. _V )
21	16	ralrimiva 2791	. . . . . . 7 |- ( ph -> A. x e. I J e. Top )
22		eqid 2435	. . . . . . . 8 |- ( Xt_ ` ( x e. I |-> J ) ) = ( Xt_ ` ( x e. I |-> J ) )
23	22	ptunimpt 19012	. . . . . . 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 656	. . . . . 6 |- ( ph -> X_ x e. I U. J = U. ( Xt_ ` ( x e. I |-> J ) ) )
25	24	ineq1d 3541	. . . . 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 2435	. . . . . 6 |- U. ( Xt_ ` ( x e. I |-> J ) ) = U. ( Xt_ ` ( x e. I |-> J ) )
27	2	topcld 18483	. . . . . . . . . 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 3821	. . . . . . . . 9 |- ( ( C e. ( Clsd ` J ) /\ U. J e. ( Clsd ` J ) ) -> if ( x = y , C , U. J ) e. ( Clsd ` J ) )
30	1, 28, 29	syl2anc 656	. . . . . . . 8 |- ( ( ph /\ x e. I ) -> if ( x = y , C , U. J ) e. ( Clsd ` J ) )
31	20, 16, 30	ptcldmpt 19031	. . . . . . 7 |- ( ph -> X_ x e. I if ( x = y , C , U. J ) e. ( Clsd ` ( Xt_ ` ( x e. I |-> J ) ) ) )
32	31	adantr 462	. . . . . 6 |- ( ( ph /\ y e. I ) -> X_ x e. I if ( x = y , C , U. J ) e. ( Clsd ` ( Xt_ ` ( x e. I |-> J ) ) ) )
33		simprr 751	. . . . . . . 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 5638	. . . . . . . . . . . . . . 15 |- ( B : S -1-1-onto-> C -> B : S -onto-> C )
36		foima 5615	. . . . . . . . . . . . . . 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 2440	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. I ) -> C = ( B " S ) )
39		kelac1.z	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. I ) -> S =/= (/) )
40		f1ofn 5632	. . . . . . . . . . . . . . . . 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 3365	. . . . . . . . . . . . . . . 16 |- S C_ S
43		fnimaeq0 5522	. . . . . . . . . . . . . . . 16 |- ( ( B Fn S /\ S C_ S ) -> ( ( B " S ) = (/) <-> S = (/) ) )
44	41, 42, 43	sylancl 657	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. I ) -> ( ( B " S ) = (/) <-> S = (/) ) )
45	44	necon3bid 2635	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. I ) -> ( ( B " S ) =/= (/) <-> S =/= (/) ) )
46	39, 45	mpbird 232	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. I ) -> ( B " S ) =/= (/) )
47	38, 46	eqnetrd 2618	. . . . . . . . . . . 12 |- ( ( ph /\ x e. I ) -> C =/= (/) )
48		n0 3636	. . . . . . . . . . . 12 |- ( C =/= (/) <-> E. w w e. C )
49	47, 48	sylib 196	. . . . . . . . . . 11 |- ( ( ph /\ x e. I ) -> E. w w e. C )
50		rexv 2979	. . . . . . . . . . 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 2791	. . . . . . . . 9 |- ( ph -> A. x e. I E. w e. _V w e. C )
53		ssralv 3406	. . . . . . . . . 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 462	. . . . . . . . 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 466	. . . . . . . 8 |- ( ( ph /\ ( z C_ I /\ z e. Fin ) ) -> A. x e. z E. w e. _V w e. C )
56		eleq1 2495	. . . . . . . . 9 |- ( w = ( f ` x ) -> ( w e. C <-> ( f ` x ) e. C ) )
57	56	ac6sfi 7546	. . . . . . . 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 656	. . . . . . 7 |- ( ( ph /\ ( z C_ I /\ z e. Fin ) ) -> E. f ( f : z --> _V /\ A. x e. z ( f ` x ) e. C ) )
59	24	eqcomd 2440	. . . . . . . . . . 11 |- ( ph -> U. ( Xt_ ` ( x e. I |-> J ) ) = X_ x e. I U. J )
60	59	ineq1d 3541	. . . . . . . . . 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 720	. . . . . . . . 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 3787	. . . . . . . . . . . . . . . . . . 19 |- ( x e. z -> if ( x e. z , ( f ` x ) , U ) = ( f ` x ) )
63	62	ad2antrl 722	. . . . . . . . . . . . . . . . . 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 748	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ x e. z ) -> ph )
65		simprl 750	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ( z C_ I /\ z e. Fin ) ) -> z C_ I )
66	65	sselda 3346	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ x e. z ) -> x e. I )
67	64, 66, 4	syl2anc 656	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ x e. z ) -> C C_ U. J )
68	67	sseld 3345	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ x e. z ) -> ( ( f ` x ) e. C -> ( f ` x ) e. U. J ) )
69	68	impr 616	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ ( x e. z /\ ( f ` x ) e. C ) ) -> ( f ` x ) e. U. J )
70	63, 69	eqeltrd 2509	. . . . . . . . . . . . . . . . 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 612	. . . . . . . . . . . . . . . 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 2786	. . . . . . . . . . . . . . 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 3469	. . . . . . . . . . . . . . . . . . 19 |- ( x e. ( I \ z ) -> -. x e. z )
75		iffalse 3789	. . . . . . . . . . . . . . . . . . 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 463	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. ( I \ z ) ) -> if ( x e. z , ( f ` x ) , U ) = U )
78		eldifi 3468	. . . . . . . . . . . . . . . . . 18 |- ( x e. ( I \ z ) -> x e. I )
79		kelac1.u	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. I ) -> U e. U. J )
80	78, 79	sylan2 471	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ x e. ( I \ z ) ) -> U e. U. J )
81	77, 80	eqeltrd 2509	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ x e. ( I \ z ) ) -> if ( x e. z , ( f ` x ) , U ) e. U. J )
82	81	ralrimiva 2791	. . . . . . . . . . . . . . 15 |- ( ph -> A. x e. ( I \ z ) if ( x e. z , ( f ` x ) , U ) e. U. J )
83	82	ad2antrr 720	. . . . . . . . . . . . . 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 3528	. . . . . . . . . . . . . 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 656	. . . . . . . . . . . . 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 3749	. . . . . . . . . . . . . . . . 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 722	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( z C_ I /\ z e. Fin ) ) -> ( z u. ( I \ z ) ) = I )
89	88	raleqdv 2915	. . . . . . . . . . . . . 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 462	. . . . . . . . . . . . 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 720	. . . . . . . . . . . . 13 |- ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) -> I e. _V )
93		mptelixpg 7290	. . . . . . . . . . . . 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 2496	. . . . . . . . . . . . . . . . . . . . . 22 |- ( C = if ( x = y , C , U. J ) -> ( ( f ` x ) e. C <-> ( f ` x ) e. if ( x = y , C , U. J ) ) )
97		eleq2 2496	. . . . . . . . . . . . . . . . . . . . . 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 755	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ ( x e. z /\ ( f ` x ) e. C ) ) /\ x = y ) -> ( f ` x ) e. C )
99	69	adantr 462	. . . . . . . . . . . . . . . . . . . . . 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 3814	. . . . . . . . . . . . . . . . . . . . 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 2509	. . . . . . . . . . . . . . . . . . . 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 612	. . . . . . . . . . . . . . . . . . 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 2786	. . . . . . . . . . . . . . . . . 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 462	. . . . . . . . . . . . . . . 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 709	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ y e. z ) /\ x e. ( I \ z ) ) -> U e. U. J )
107	76	adantl 463	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ y e. z ) /\ x e. ( I \ z ) ) -> if ( x e. z , ( f ` x ) , U ) = U )
108		incom 3533	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( I \ z ) i^i z ) = ( z i^i ( I \ z ) )
109		disjdif 3741	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( z i^i ( I \ z ) ) = (/)
110	108, 109	eqtri 2455	. . . . . . . . . . . . . . . . . . . . . . . 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 458	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ y e. z ) /\ x e. ( I \ z ) ) -> x e. ( I \ z ) )
113		simplr 749	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ y e. z ) /\ x e. ( I \ z ) ) -> y e. z )
114		disjne 3714	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( I \ z ) i^i z ) = (/) /\ x e. ( I \ z ) /\ y e. z ) -> x =/= y )
115	111, 112, 113, 114	syl3anc 1213	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ y e. z ) /\ x e. ( I \ z ) ) -> x =/= y )
116	115	neneqd 2616	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ y e. z ) /\ x e. ( I \ z ) ) -> -. x = y )
117		iffalse 3789	. . . . . . . . . . . . . . . . . . . . 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 2516	. . . . . . . . . . . . . . . . . . 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 2791	. . . . . . . . . . . . . . . . . 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 709	. . . . . . . . . . . . . . . . 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 709	. . . . . . . . . . . . . . . 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 3528	. . . . . . . . . . . . . . . 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 656	. . . . . . . . . . . . . . 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 2915	. . . . . . . . . . . . . . . 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 720	. . . . . . . . . . . . . . 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 724	. . . . . . . . . . . . . . 15 |- ( ( ( ( ph /\ ( z C_ I /\ z e. Fin ) ) /\ A. x e. z ( f ` x ) e. C ) /\ y e. z ) -> I e. _V )
129		mptelixpg 7290	. . . . . . . . . . . . . . 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 2791	. . . . . . . . . . . 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 5936	. . . . . . . . . . . . . . 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 720	. . . . . . . . . . . . 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 4166	. . . . . . . . . . . . 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 3530	. . . . . . . . . 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 3633	. . . . . . . . . 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 2618	. . . . . . . 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 710	. . . . . . 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 1693	. . . . . 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 28880	. . . . 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 2618	. . . 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 2618	. . 3 |- ( ph -> X_ x e. I C =/= (/) )
148		n0 3636	. . 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 7257	. . . . . 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 1000	. . . . 5 |- ( y e. X_ x e. I C -> A. x e. I ( y ` x ) e. C )
152		f1ocnv 5643	. . . . . . . 8 |- ( B : S -1-1-onto-> C -> `' B : C -1-1-onto-> S )
153		f1of 5631	. . . . . . . 8 |- ( `' B : C -1-1-onto-> S -> `' B : C --> S )
154		ffvelrn 5831	. . . . . . . . 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 2786	. . . . . 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 471	. . . 4 |- ( ( ph /\ y e. X_ x e. I C ) -> A. x e. I ( `' B ` ( y ` x ) ) e. S )
160		mptelixpg 7290	. . . . . 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 462	. . . 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 3633	. . 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 1693	1 |- ( ph -> X_ x e. I S =/= (/) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1364   E.wex 1591   e. wcel 1757   =/= wne 2598   A.wral 2707   E.wrex 2708   _Vcvv 2964   \ cdif 3315   u. cun 3316   i^i cin 3317   C_ wss 3318   (/)c0 3627   ifcif 3781   U.cuni 4081   |^|_ciin 4162   e. cmpt 4340   `'ccnv 4828   "cima 4832   Fn wfn 5403   -->wf 5404   -onto->wfo 5406   -1-1-onto->wf1o 5407   ` cfv 5408   X_cixp 7253   Fincfn 7300   Xt_cpt 14362   Topctop 18342   Clsdccld 18464   Compccmp 18833

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2416  ax-rep 4393  ax-sep 4403  ax-nul 4411  ax-pow 4460  ax-pr 4521  ax-un 6363

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1702  df-eu 2260  df-mo 2261  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2712  df-rex 2713  df-reu 2714  df-rab 2716  df-v 2966  df-sbc 3178  df-csb 3279  df-dif 3321  df-un 3323  df-in 3325  df-ss 3332  df-pss 3334  df-nul 3628  df-if 3782  df-pw 3852  df-sn 3868  df-pr 3870  df-tp 3872  df-op 3874  df-uni 4082  df-int 4119  df-iun 4163  df-iin 4164  df-br 4283  df-opab 4341  df-mpt 4342  df-tr 4376  df-eprel 4621  df-id 4625  df-po 4630  df-so 4631  df-fr 4668  df-we 4670  df-ord 4711  df-on 4712  df-lim 4713  df-suc 4714  df-xp 4835  df-rel 4836  df-cnv 4837  df-co 4838  df-dm 4839  df-rn 4840  df-res 4841  df-ima 4842  df-iota 5371  df-fun 5410  df-fn 5411  df-f 5412  df-f1 5413  df-fo 5414  df-f1o 5415  df-fv 5416  df-ov 6085  df-oprab 6086  df-mpt2 6087  df-om 6468  df-1st 6568  df-2nd 6569  df-recs 6820  df-rdg 6854  df-1o 6910  df-2o 6911  df-oadd 6914  df-er 7091  df-map 7206  df-ixp 7254  df-en 7301  df-dom 7302  df-sdom 7303  df-fin 7304  df-fi 7651  df-topgen 14367  df-pt 14368  df-top 18347  df-bases 18349  df-cld 18467  df-cmp 18834

This theorem is referenced by:  kelac2  29265