kelac1

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)

	Ref	Expression
Hypotheses	kelac1.z	$⊢ (φ \land x \in I) \to S \neq \emptyset$
	kelac1.j	$⊢ (φ \land x \in I) \to J \in Top$
	kelac1.c	$⊢ (φ \land x \in I) \to C \in Clsd (J)$
	kelac1.b	$⊢ (φ \land x \in I) \to B : S \underset{1-1 onto}{⟶} C$
	kelac1.u	$⊢ (φ \land x \in I) \to U \in ⋃ J$
	kelac1.k	$⊢ φ \to \prod_{𝑡} ((x \in I ⟼ J)) \in Comp$
Assertion	kelac1	$⊢ φ \to \underset{x \in I}{⨉} S \neq \emptyset$

Proof

Step	Hyp	Ref	Expression
1		kelac1.z	$⊢ (φ \land x \in I) \to S \neq \emptyset$
2		kelac1.j	$⊢ (φ \land x \in I) \to J \in Top$
3		kelac1.c	$⊢ (φ \land x \in I) \to C \in Clsd (J)$
4		kelac1.b	$⊢ (φ \land x \in I) \to B : S \underset{1-1 onto}{⟶} C$
5		kelac1.u	$⊢ (φ \land x \in I) \to U \in ⋃ J$
6		kelac1.k	$⊢ φ \to \prod_{𝑡} ((x \in I ⟼ J)) \in Comp$
7		eqid	$⊢ ⋃ J = ⋃ J$
8	7	cldss	$⊢ C \in Clsd (J) \to C \subseteq ⋃ J$
9	3 8	syl	$⊢ (φ \land x \in I) \to C \subseteq ⋃ J$
10	9	ralrimiva	$⊢ φ \to \forall x \in I C \subseteq ⋃ J$
11		boxriin	$⊢ \forall x \in I C \subseteq ⋃ J \to \underset{x \in I}{⨉} C = \underset{x \in I}{⨉} ⋃ J \cap ⋂_{y \in I} \underset{x \in I}{⨉} if (x = y, C, ⋃ J)$
12	10 11	syl	$⊢ φ \to \underset{x \in I}{⨉} C = \underset{x \in I}{⨉} ⋃ J \cap ⋂_{y \in I} \underset{x \in I}{⨉} if (x = y, C, ⋃ J)$
13		cmptop	$⊢ \prod_{𝑡} ((x \in I ⟼ J)) \in Comp \to \prod_{𝑡} ((x \in I ⟼ J)) \in Top$
14		0ntop	$⊢ \neg \emptyset \in Top$
15		fvprc	$⊢ \neg (x \in I ⟼ J) \in V \to \prod_{𝑡} ((x \in I ⟼ J)) = \emptyset$
16	15	eleq1d	$⊢ \neg (x \in I ⟼ J) \in V \to (\prod_{𝑡} ((x \in I ⟼ J)) \in Top \leftrightarrow \emptyset \in Top)$
17	14 16	mtbiri	$⊢ \neg (x \in I ⟼ J) \in V \to \neg \prod_{𝑡} ((x \in I ⟼ J)) \in Top$
18	17	con4i	$⊢ \prod_{𝑡} ((x \in I ⟼ J)) \in Top \to (x \in I ⟼ J) \in V$
19	6 13 18	3syl	$⊢ φ \to (x \in I ⟼ J) \in V$
20	2	fmpttd	$⊢ φ \to (x \in I ⟼ J) : I ⟶ Top$
21		dmfex	$⊢ ((x \in I ⟼ J) \in V \land (x \in I ⟼ J) : I ⟶ Top) \to I \in V$
22	19 20 21	syl2anc	$⊢ φ \to I \in V$
23	2	ralrimiva	$⊢ φ \to \forall x \in I J \in Top$
24		eqid	$⊢ \prod_{𝑡} ((x \in I ⟼ J)) = \prod_{𝑡} ((x \in I ⟼ J))$
25	24	ptunimpt	$⊢ (I \in V \land \forall x \in I J \in Top) \to \underset{x \in I}{⨉} ⋃ J = ⋃ \prod_{𝑡} ((x \in I ⟼ J))$
26	22 23 25	syl2anc	$⊢ φ \to \underset{x \in I}{⨉} ⋃ J = ⋃ \prod_{𝑡} ((x \in I ⟼ J))$
27	26	ineq1d	$⊢ φ \to \underset{x \in I}{⨉} ⋃ J \cap ⋂_{y \in I} \underset{x \in I}{⨉} if (x = y, C, ⋃ J) = ⋃ \prod_{𝑡} ((x \in I ⟼ J)) \cap ⋂_{y \in I} \underset{x \in I}{⨉} if (x = y, C, ⋃ J)$
28		eqid	$⊢ ⋃ \prod_{𝑡} ((x \in I ⟼ J)) = ⋃ \prod_{𝑡} ((x \in I ⟼ J))$
29	7	topcld	$⊢ J \in Top \to ⋃ J \in Clsd (J)$
30	2 29	syl	$⊢ (φ \land x \in I) \to ⋃ J \in Clsd (J)$
31	3 30	ifcld	$⊢ (φ \land x \in I) \to if (x = y, C, ⋃ J) \in Clsd (J)$
32	22 2 31	ptcldmpt	$⊢ φ \to \underset{x \in I}{⨉} if (x = y, C, ⋃ J) \in Clsd (\prod_{𝑡} ((x \in I ⟼ J)))$
33	32	adantr	$⊢ (φ \land y \in I) \to \underset{x \in I}{⨉} if (x = y, C, ⋃ J) \in Clsd (\prod_{𝑡} ((x \in I ⟼ J)))$
34		simprr	$⊢ (φ \land (z \subseteq I \land z \in Fin)) \to z \in Fin$
35		f1ofo	$⊢ B : S \underset{1-1 onto}{⟶} C \to B : S \underset{onto}{⟶} C$
36		foima	$⊢ B : S \underset{onto}{⟶} C \to B [S] = C$
37	4 35 36	3syl	$⊢ (φ \land x \in I) \to B [S] = C$
38	37	eqcomd	$⊢ (φ \land x \in I) \to C = B [S]$
39		f1ofn	$⊢ B : S \underset{1-1 onto}{⟶} C \to B Fn S$
40	4 39	syl	$⊢ (φ \land x \in I) \to B Fn S$
41		ssid	$⊢ S \subseteq S$
42		fnimaeq0	$⊢ (B Fn S \land S \subseteq S) \to (B [S] = \emptyset \leftrightarrow S = \emptyset)$
43	40 41 42	sylancl	$⊢ (φ \land x \in I) \to (B [S] = \emptyset \leftrightarrow S = \emptyset)$
44	43	necon3bid	$⊢ (φ \land x \in I) \to (B [S] \neq \emptyset \leftrightarrow S \neq \emptyset)$
45	1 44	mpbird	$⊢ (φ \land x \in I) \to B [S] \neq \emptyset$
46	38 45	eqnetrd	$⊢ (φ \land x \in I) \to C \neq \emptyset$
47		n0	$⊢ C \neq \emptyset \leftrightarrow \exists w w \in C$
48	46 47	sylib	$⊢ (φ \land x \in I) \to \exists w w \in C$
49		rexv	$⊢ \exists w \in V w \in C \leftrightarrow \exists w w \in C$
50	48 49	sylibr	$⊢ (φ \land x \in I) \to \exists w \in V w \in C$
51	50	ralrimiva	$⊢ φ \to \forall x \in I \exists w \in V w \in C$
52		ssralv	$⊢ z \subseteq I \to (\forall x \in I \exists w \in V w \in C \to \forall x \in z \exists w \in V w \in C)$
53	52	adantr	$⊢ (z \subseteq I \land z \in Fin) \to (\forall x \in I \exists w \in V w \in C \to \forall x \in z \exists w \in V w \in C)$
54	51 53	mpan9	$⊢ (φ \land (z \subseteq I \land z \in Fin)) \to \forall x \in z \exists w \in V w \in C$
55		eleq1	$⊢ w = f (x) \to (w \in C \leftrightarrow f (x) \in C)$
56	55	ac6sfi	$⊢ (z \in Fin \land \forall x \in z \exists w \in V w \in C) \to \exists f (f : z ⟶ V \land \forall x \in z f (x) \in C)$
57	34 54 56	syl2anc	$⊢ (φ \land (z \subseteq I \land z \in Fin)) \to \exists f (f : z ⟶ V \land \forall x \in z f (x) \in C)$
58	26	eqcomd	$⊢ φ \to ⋃ \prod_{𝑡} ((x \in I ⟼ J)) = \underset{x \in I}{⨉} ⋃ J$
59	58	ineq1d	$⊢ φ \to ⋃ \prod_{𝑡} ((x \in I ⟼ J)) \cap ⋂_{y \in z} \underset{x \in I}{⨉} if (x = y, C, ⋃ J) = \underset{x \in I}{⨉} ⋃ J \cap ⋂_{y \in z} \underset{x \in I}{⨉} if (x = y, C, ⋃ J)$
60	59	ad2antrr	$⊢ ((φ \land (z \subseteq I \land z \in Fin)) \land \forall x \in z f (x) \in C) \to ⋃ \prod_{𝑡} ((x \in I ⟼ J)) \cap ⋂_{y \in z} \underset{x \in I}{⨉} if (x = y, C, ⋃ J) = \underset{x \in I}{⨉} ⋃ J \cap ⋂_{y \in z} \underset{x \in I}{⨉} if (x = y, C, ⋃ J)$
61		iftrue	$⊢ x \in z \to if (x \in z, f (x), U) = f (x)$
62	61	ad2antrl	$⊢ ((φ \land (z \subseteq I \land z \in Fin)) \land (x \in z \land f (x) \in C)) \to if (x \in z, f (x), U) = f (x)$
63		simpll	$⊢ ((φ \land (z \subseteq I \land z \in Fin)) \land x \in z) \to φ$
64		simprl	$⊢ (φ \land (z \subseteq I \land z \in Fin)) \to z \subseteq I$
65	64	sselda	$⊢ ((φ \land (z \subseteq I \land z \in Fin)) \land x \in z) \to x \in I$
66	63 65 9	syl2anc	$⊢ ((φ \land (z \subseteq I \land z \in Fin)) \land x \in z) \to C \subseteq ⋃ J$
67	66	sseld	$⊢ ((φ \land (z \subseteq I \land z \in Fin)) \land x \in z) \to (f (x) \in C \to f (x) \in ⋃ J)$
68	67	impr	$⊢ ((φ \land (z \subseteq I \land z \in Fin)) \land (x \in z \land f (x) \in C)) \to f (x) \in ⋃ J$
69	62 68	eqeltrd	$⊢ ((φ \land (z \subseteq I \land z \in Fin)) \land (x \in z \land f (x) \in C)) \to if (x \in z, f (x), U) \in ⋃ J$
70	69	expr	$⊢ ((φ \land (z \subseteq I \land z \in Fin)) \land x \in z) \to (f (x) \in C \to if (x \in z, f (x), U) \in ⋃ J)$
71	70	ralimdva	$⊢ (φ \land (z \subseteq I \land z \in Fin)) \to (\forall x \in z f (x) \in C \to \forall x \in z if (x \in z, f (x), U) \in ⋃ J)$
72	71	imp	$⊢ ((φ \land (z \subseteq I \land z \in Fin)) \land \forall x \in z f (x) \in C) \to \forall x \in z if (x \in z, f (x), U) \in ⋃ J$
73		eldifn	$⊢ x \in (I ∖ z) \to \neg x \in z$
74	73	iffalsed	$⊢ x \in (I ∖ z) \to if (x \in z, f (x), U) = U$
75	74	adantl	$⊢ (φ \land x \in (I ∖ z)) \to if (x \in z, f (x), U) = U$
76		eldifi	$⊢ x \in (I ∖ z) \to x \in I$
77	76 5	sylan2	$⊢ (φ \land x \in (I ∖ z)) \to U \in ⋃ J$
78	75 77	eqeltrd	$⊢ (φ \land x \in (I ∖ z)) \to if (x \in z, f (x), U) \in ⋃ J$
79	78	ralrimiva	$⊢ φ \to \forall x \in (I ∖ z) if (x \in z, f (x), U) \in ⋃ J$
80	79	ad2antrr	$⊢ ((φ \land (z \subseteq I \land z \in Fin)) \land \forall x \in z f (x) \in C) \to \forall x \in (I ∖ z) if (x \in z, f (x), U) \in ⋃ J$
81		ralun	$⊢ (\forall x \in z if (x \in z, f (x), U) \in ⋃ J \land \forall x \in (I ∖ z) if (x \in z, f (x), U) \in ⋃ J) \to \forall x \in (z \cup (I ∖ z)) if (x \in z, f (x), U) \in ⋃ J$
82	72 80 81	syl2anc	$⊢ ((φ \land (z \subseteq I \land z \in Fin)) \land \forall x \in z f (x) \in C) \to \forall x \in (z \cup (I ∖ z)) if (x \in z, f (x), U) \in ⋃ J$
83		undif	$⊢ z \subseteq I \leftrightarrow z \cup (I ∖ z) = I$
84	83	biimpi	$⊢ z \subseteq I \to z \cup (I ∖ z) = I$
85	84	ad2antrl	$⊢ (φ \land (z \subseteq I \land z \in Fin)) \to z \cup (I ∖ z) = I$
86	85	raleqdv	$⊢ (φ \land (z \subseteq I \land z \in Fin)) \to (\forall x \in (z \cup (I ∖ z)) if (x \in z, f (x), U) \in ⋃ J \leftrightarrow \forall x \in I if (x \in z, f (x), U) \in ⋃ J)$
87	86	adantr	$⊢ ((φ \land (z \subseteq I \land z \in Fin)) \land \forall x \in z f (x) \in C) \to (\forall x \in (z \cup (I ∖ z)) if (x \in z, f (x), U) \in ⋃ J \leftrightarrow \forall x \in I if (x \in z, f (x), U) \in ⋃ J)$
88	82 87	mpbid	$⊢ ((φ \land (z \subseteq I \land z \in Fin)) \land \forall x \in z f (x) \in C) \to \forall x \in I if (x \in z, f (x), U) \in ⋃ J$
89	22	ad2antrr	$⊢ ((φ \land (z \subseteq I \land z \in Fin)) \land \forall x \in z f (x) \in C) \to I \in V$
90		mptelixpg	$⊢ I \in V \to ((x \in I ⟼ if (x \in z, f (x), U)) \in \underset{x \in I}{⨉} ⋃ J \leftrightarrow \forall x \in I if (x \in z, f (x), U) \in ⋃ J)$
91	89 90	syl	$⊢ ((φ \land (z \subseteq I \land z \in Fin)) \land \forall x \in z f (x) \in C) \to ((x \in I ⟼ if (x \in z, f (x), U)) \in \underset{x \in I}{⨉} ⋃ J \leftrightarrow \forall x \in I if (x \in z, f (x), U) \in ⋃ J)$
92	88 91	mpbird	$⊢ ((φ \land (z \subseteq I \land z \in Fin)) \land \forall x \in z f (x) \in C) \to (x \in I ⟼ if (x \in z, f (x), U)) \in \underset{x \in I}{⨉} ⋃ J$
93		eleq2	$⊢ C = if (x = y, C, ⋃ J) \to (f (x) \in C \leftrightarrow f (x) \in if (x = y, C, ⋃ J))$
94		eleq2	$⊢ ⋃ J = if (x = y, C, ⋃ J) \to (f (x) \in ⋃ J \leftrightarrow f (x) \in if (x = y, C, ⋃ J))$
95		simplrr	$⊢ (((φ \land (z \subseteq I \land z \in Fin)) \land (x \in z \land f (x) \in C)) \land x = y) \to f (x) \in C$
96	68	adantr	$⊢ (((φ \land (z \subseteq I \land z \in Fin)) \land (x \in z \land f (x) \in C)) \land \neg x = y) \to f (x) \in ⋃ J$
97	93 94 95 96	ifbothda	$⊢ ((φ \land (z \subseteq I \land z \in Fin)) \land (x \in z \land f (x) \in C)) \to f (x) \in if (x = y, C, ⋃ J)$
98	62 97	eqeltrd	$⊢ ((φ \land (z \subseteq I \land z \in Fin)) \land (x \in z \land f (x) \in C)) \to if (x \in z, f (x), U) \in if (x = y, C, ⋃ J)$
99	98	expr	$⊢ ((φ \land (z \subseteq I \land z \in Fin)) \land x \in z) \to (f (x) \in C \to if (x \in z, f (x), U) \in if (x = y, C, ⋃ J))$
100	99	ralimdva	$⊢ (φ \land (z \subseteq I \land z \in Fin)) \to (\forall x \in z f (x) \in C \to \forall x \in z if (x \in z, f (x), U) \in if (x = y, C, ⋃ J))$
101	100	imp	$⊢ ((φ \land (z \subseteq I \land z \in Fin)) \land \forall x \in z f (x) \in C) \to \forall x \in z if (x \in z, f (x), U) \in if (x = y, C, ⋃ J)$
102	101	adantr	$⊢ (((φ \land (z \subseteq I \land z \in Fin)) \land \forall x \in z f (x) \in C) \land y \in z) \to \forall x \in z if (x \in z, f (x), U) \in if (x = y, C, ⋃ J)$
103	77	adantlr	$⊢ ((φ \land y \in z) \land x \in (I ∖ z)) \to U \in ⋃ J$
104	74	adantl	$⊢ ((φ \land y \in z) \land x \in (I ∖ z)) \to if (x \in z, f (x), U) = U$
105		disjdifr	$⊢ (I ∖ z) \cap z = \emptyset$
106	105	a1i	$⊢ ((φ \land y \in z) \land x \in (I ∖ z)) \to (I ∖ z) \cap z = \emptyset$
107		simpr	$⊢ ((φ \land y \in z) \land x \in (I ∖ z)) \to x \in (I ∖ z)$
108		simplr	$⊢ ((φ \land y \in z) \land x \in (I ∖ z)) \to y \in z$
109		disjne	$⊢ ((I ∖ z) \cap z = \emptyset \land x \in (I ∖ z) \land y \in z) \to x \neq y$
110	106 107 108 109	syl3anc	$⊢ ((φ \land y \in z) \land x \in (I ∖ z)) \to x \neq y$
111	110	neneqd	$⊢ ((φ \land y \in z) \land x \in (I ∖ z)) \to \neg x = y$
112	111	iffalsed	$⊢ ((φ \land y \in z) \land x \in (I ∖ z)) \to if (x = y, C, ⋃ J) = ⋃ J$
113	103 104 112	3eltr4d	$⊢ ((φ \land y \in z) \land x \in (I ∖ z)) \to if (x \in z, f (x), U) \in if (x = y, C, ⋃ J)$
114	113	ralrimiva	$⊢ (φ \land y \in z) \to \forall x \in (I ∖ z) if (x \in z, f (x), U) \in if (x = y, C, ⋃ J)$
115	114	adantlr	$⊢ ((φ \land (z \subseteq I \land z \in Fin)) \land y \in z) \to \forall x \in (I ∖ z) if (x \in z, f (x), U) \in if (x = y, C, ⋃ J)$
116	115	adantlr	$⊢ (((φ \land (z \subseteq I \land z \in Fin)) \land \forall x \in z f (x) \in C) \land y \in z) \to \forall x \in (I ∖ z) if (x \in z, f (x), U) \in if (x = y, C, ⋃ J)$
117		ralun	$⊢ (\forall x \in z if (x \in z, f (x), U) \in if (x = y, C, ⋃ J) \land \forall x \in (I ∖ z) if (x \in z, f (x), U) \in if (x = y, C, ⋃ J)) \to \forall x \in (z \cup (I ∖ z)) if (x \in z, f (x), U) \in if (x = y, C, ⋃ J)$
118	102 116 117	syl2anc	$⊢ (((φ \land (z \subseteq I \land z \in Fin)) \land \forall x \in z f (x) \in C) \land y \in z) \to \forall x \in (z \cup (I ∖ z)) if (x \in z, f (x), U) \in if (x = y, C, ⋃ J)$
119	85	raleqdv	$⊢ (φ \land (z \subseteq I \land z \in Fin)) \to (\forall x \in (z \cup (I ∖ z)) if (x \in z, f (x), U) \in if (x = y, C, ⋃ J) \leftrightarrow \forall x \in I if (x \in z, f (x), U) \in if (x = y, C, ⋃ J))$
120	119	ad2antrr	$⊢ (((φ \land (z \subseteq I \land z \in Fin)) \land \forall x \in z f (x) \in C) \land y \in z) \to (\forall x \in (z \cup (I ∖ z)) if (x \in z, f (x), U) \in if (x = y, C, ⋃ J) \leftrightarrow \forall x \in I if (x \in z, f (x), U) \in if (x = y, C, ⋃ J))$
121	118 120	mpbid	$⊢ (((φ \land (z \subseteq I \land z \in Fin)) \land \forall x \in z f (x) \in C) \land y \in z) \to \forall x \in I if (x \in z, f (x), U) \in if (x = y, C, ⋃ J)$
122	22	ad3antrrr	$⊢ (((φ \land (z \subseteq I \land z \in Fin)) \land \forall x \in z f (x) \in C) \land y \in z) \to I \in V$
123		mptelixpg	$⊢ I \in V \to ((x \in I ⟼ if (x \in z, f (x), U)) \in \underset{x \in I}{⨉} if (x = y, C, ⋃ J) \leftrightarrow \forall x \in I if (x \in z, f (x), U) \in if (x = y, C, ⋃ J))$
124	122 123	syl	$⊢ (((φ \land (z \subseteq I \land z \in Fin)) \land \forall x \in z f (x) \in C) \land y \in z) \to ((x \in I ⟼ if (x \in z, f (x), U)) \in \underset{x \in I}{⨉} if (x = y, C, ⋃ J) \leftrightarrow \forall x \in I if (x \in z, f (x), U) \in if (x = y, C, ⋃ J))$
125	121 124	mpbird	$⊢ (((φ \land (z \subseteq I \land z \in Fin)) \land \forall x \in z f (x) \in C) \land y \in z) \to (x \in I ⟼ if (x \in z, f (x), U)) \in \underset{x \in I}{⨉} if (x = y, C, ⋃ J)$
126	125	ralrimiva	$⊢ ((φ \land (z \subseteq I \land z \in Fin)) \land \forall x \in z f (x) \in C) \to \forall y \in z (x \in I ⟼ if (x \in z, f (x), U)) \in \underset{x \in I}{⨉} if (x = y, C, ⋃ J)$
127		mptexg	$⊢ I \in V \to (x \in I ⟼ if (x \in z, f (x), U)) \in V$
128	22 127	syl	$⊢ φ \to (x \in I ⟼ if (x \in z, f (x), U)) \in V$
129	128	ad2antrr	$⊢ ((φ \land (z \subseteq I \land z \in Fin)) \land \forall x \in z f (x) \in C) \to (x \in I ⟼ if (x \in z, f (x), U)) \in V$
130		eliin	$⊢ (x \in I ⟼ if (x \in z, f (x), U)) \in V \to ((x \in I ⟼ if (x \in z, f (x), U)) \in ⋂_{y \in z} \underset{x \in I}{⨉} if (x = y, C, ⋃ J) \leftrightarrow \forall y \in z (x \in I ⟼ if (x \in z, f (x), U)) \in \underset{x \in I}{⨉} if (x = y, C, ⋃ J))$
131	129 130	syl	$⊢ ((φ \land (z \subseteq I \land z \in Fin)) \land \forall x \in z f (x) \in C) \to ((x \in I ⟼ if (x \in z, f (x), U)) \in ⋂_{y \in z} \underset{x \in I}{⨉} if (x = y, C, ⋃ J) \leftrightarrow \forall y \in z (x \in I ⟼ if (x \in z, f (x), U)) \in \underset{x \in I}{⨉} if (x = y, C, ⋃ J))$
132	126 131	mpbird	$⊢ ((φ \land (z \subseteq I \land z \in Fin)) \land \forall x \in z f (x) \in C) \to (x \in I ⟼ if (x \in z, f (x), U)) \in ⋂_{y \in z} \underset{x \in I}{⨉} if (x = y, C, ⋃ J)$
133	92 132	elind	$⊢ ((φ \land (z \subseteq I \land z \in Fin)) \land \forall x \in z f (x) \in C) \to (x \in I ⟼ if (x \in z, f (x), U)) \in (\underset{x \in I}{⨉} ⋃ J \cap ⋂_{y \in z} \underset{x \in I}{⨉} if (x = y, C, ⋃ J))$
134	133	ne0d	$⊢ ((φ \land (z \subseteq I \land z \in Fin)) \land \forall x \in z f (x) \in C) \to \underset{x \in I}{⨉} ⋃ J \cap ⋂_{y \in z} \underset{x \in I}{⨉} if (x = y, C, ⋃ J) \neq \emptyset$
135	60 134	eqnetrd	$⊢ ((φ \land (z \subseteq I \land z \in Fin)) \land \forall x \in z f (x) \in C) \to ⋃ \prod_{𝑡} ((x \in I ⟼ J)) \cap ⋂_{y \in z} \underset{x \in I}{⨉} if (x = y, C, ⋃ J) \neq \emptyset$
136	135	adantrl	$⊢ ((φ \land (z \subseteq I \land z \in Fin)) \land (f : z ⟶ V \land \forall x \in z f (x) \in C)) \to ⋃ \prod_{𝑡} ((x \in I ⟼ J)) \cap ⋂_{y \in z} \underset{x \in I}{⨉} if (x = y, C, ⋃ J) \neq \emptyset$
137	57 136	exlimddv	$⊢ (φ \land (z \subseteq I \land z \in Fin)) \to ⋃ \prod_{𝑡} ((x \in I ⟼ J)) \cap ⋂_{y \in z} \underset{x \in I}{⨉} if (x = y, C, ⋃ J) \neq \emptyset$
138	28 6 33 137	cmpfiiin	$⊢ φ \to ⋃ \prod_{𝑡} ((x \in I ⟼ J)) \cap ⋂_{y \in I} \underset{x \in I}{⨉} if (x = y, C, ⋃ J) \neq \emptyset$
139	27 138	eqnetrd	$⊢ φ \to \underset{x \in I}{⨉} ⋃ J \cap ⋂_{y \in I} \underset{x \in I}{⨉} if (x = y, C, ⋃ J) \neq \emptyset$
140	12 139	eqnetrd	$⊢ φ \to \underset{x \in I}{⨉} C \neq \emptyset$
141		n0	$⊢ \underset{x \in I}{⨉} C \neq \emptyset \leftrightarrow \exists y y \in \underset{x \in I}{⨉} C$
142	140 141	sylib	$⊢ φ \to \exists y y \in \underset{x \in I}{⨉} C$
143		elixp2	$⊢ y \in \underset{x \in I}{⨉} C \leftrightarrow (y \in V \land y Fn I \land \forall x \in I y (x) \in C)$
144	143	simp3bi	$⊢ y \in \underset{x \in I}{⨉} C \to \forall x \in I y (x) \in C$
145		f1ocnv	$⊢ B : S \underset{1-1 onto}{⟶} C \to B^{-1} : C \underset{1-1 onto}{⟶} S$
146		f1of	$⊢ B^{-1} : C \underset{1-1 onto}{⟶} S \to B^{-1} : C ⟶ S$
147		ffvelcdm	$⊢ (B^{-1} : C ⟶ S \land y (x) \in C) \to B^{-1} (y (x)) \in S$
148	147	ex	$⊢ B^{-1} : C ⟶ S \to (y (x) \in C \to B^{-1} (y (x)) \in S)$
149	4 145 146 148	4syl	$⊢ (φ \land x \in I) \to (y (x) \in C \to B^{-1} (y (x)) \in S)$
150	149	ralimdva	$⊢ φ \to (\forall x \in I y (x) \in C \to \forall x \in I B^{-1} (y (x)) \in S)$
151	150	imp	$⊢ (φ \land \forall x \in I y (x) \in C) \to \forall x \in I B^{-1} (y (x)) \in S$
152	144 151	sylan2	$⊢ (φ \land y \in \underset{x \in I}{⨉} C) \to \forall x \in I B^{-1} (y (x)) \in S$
153		mptelixpg	$⊢ I \in V \to ((x \in I ⟼ B^{-1} (y (x))) \in \underset{x \in I}{⨉} S \leftrightarrow \forall x \in I B^{-1} (y (x)) \in S)$
154	22 153	syl	$⊢ φ \to ((x \in I ⟼ B^{-1} (y (x))) \in \underset{x \in I}{⨉} S \leftrightarrow \forall x \in I B^{-1} (y (x)) \in S)$
155	154	adantr	$⊢ (φ \land y \in \underset{x \in I}{⨉} C) \to ((x \in I ⟼ B^{-1} (y (x))) \in \underset{x \in I}{⨉} S \leftrightarrow \forall x \in I B^{-1} (y (x)) \in S)$
156	152 155	mpbird	$⊢ (φ \land y \in \underset{x \in I}{⨉} C) \to (x \in I ⟼ B^{-1} (y (x))) \in \underset{x \in I}{⨉} S$
157	156	ne0d	$⊢ (φ \land y \in \underset{x \in I}{⨉} C) \to \underset{x \in I}{⨉} S \neq \emptyset$
158	142 157	exlimddv	$⊢ φ \to \underset{x \in I}{⨉} S \neq \emptyset$

Metamath Proof Explorer

Theorem kelac1

Proof