Theorem kelac1 40888

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	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑆 ≠ ∅)
kelac1.j	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐽 ∈ Top)
kelac1.c	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐶 ∈ (Clsd‘𝐽))
kelac1.b	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐵:𝑆–1-1-onto→𝐶)
kelac1.u	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑈 ∈ ∪ 𝐽)
kelac1.k	⊢ (𝜑 → (∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∈ Comp)

Assertion

Ref	Expression
kelac1	⊢ (𝜑 → X𝑥 ∈ 𝐼 𝑆 ≠ ∅)

Distinct variable groups:   𝜑,𝑥   𝑥,𝐼

Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑥)   𝑆(𝑥)   𝑈(𝑥)   𝐽(𝑥)

Proof of Theorem kelac1

Dummy variables 𝑓 𝑦 𝑧 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		kelac1.c	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐶 ∈ (Clsd‘𝐽))
2		eqid 2738	. . . . . . . 8 ⊢ ∪ 𝐽 = ∪ 𝐽
3	2	cldss 22180	. . . . . . 7 ⊢ (𝐶 ∈ (Clsd‘𝐽) → 𝐶 ⊆ ∪ 𝐽)
4	1, 3	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐶 ⊆ ∪ 𝐽)
5	4	ralrimiva 3103	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ 𝐼 𝐶 ⊆ ∪ 𝐽)
6		boxriin 8728	. . . . 5 ⊢ (∀𝑥 ∈ 𝐼 𝐶 ⊆ ∪ 𝐽 → X𝑥 ∈ 𝐼 𝐶 = (X𝑥 ∈ 𝐼 ∪ 𝐽 ∩ ∩ 𝑦 ∈ 𝐼 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
7	5, 6	syl 17	. . . 4 ⊢ (𝜑 → X𝑥 ∈ 𝐼 𝐶 = (X𝑥 ∈ 𝐼 ∪ 𝐽 ∩ ∩ 𝑦 ∈ 𝐼 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
8		kelac1.k	. . . . . . . . 9 ⊢ (𝜑 → (∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∈ Comp)
9		cmptop 22546	. . . . . . . . 9 ⊢ ((∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∈ Comp → (∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∈ Top)
10		0ntop 22054	. . . . . . . . . . 11 ⊢ ¬ ∅ ∈ Top
11		fvprc 6766	. . . . . . . . . . . 12 ⊢ (¬ (𝑥 ∈ 𝐼 ↦ 𝐽) ∈ V → (∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) = ∅)
12	11	eleq1d 2823	. . . . . . . . . . 11 ⊢ (¬ (𝑥 ∈ 𝐼 ↦ 𝐽) ∈ V → ((∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∈ Top ↔ ∅ ∈ Top))
13	10, 12	mtbiri 327	. . . . . . . . . 10 ⊢ (¬ (𝑥 ∈ 𝐼 ↦ 𝐽) ∈ V → ¬ (∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∈ Top)
14	13	con4i 114	. . . . . . . . 9 ⊢ ((∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∈ Top → (𝑥 ∈ 𝐼 ↦ 𝐽) ∈ V)
15	8, 9, 14	3syl 18	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ 𝐽) ∈ V)
16		kelac1.j	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐽 ∈ Top)
17	16	fmpttd 6989	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ 𝐽):𝐼⟶Top)
18		dmfex 7754	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐼 ↦ 𝐽) ∈ V ∧ (𝑥 ∈ 𝐼 ↦ 𝐽):𝐼⟶Top) → 𝐼 ∈ V)
19	15, 17, 18	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → 𝐼 ∈ V)
20	16	ralrimiva 3103	. . . . . . 7 ⊢ (𝜑 → ∀𝑥 ∈ 𝐼 𝐽 ∈ Top)
21		eqid 2738	. . . . . . . 8 ⊢ (∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) = (∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽))
22	21	ptunimpt 22746	. . . . . . 7 ⊢ ((𝐼 ∈ V ∧ ∀𝑥 ∈ 𝐼 𝐽 ∈ Top) → X𝑥 ∈ 𝐼 ∪ 𝐽 = ∪ (∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)))
23	19, 20, 22	syl2anc 584	. . . . . 6 ⊢ (𝜑 → X𝑥 ∈ 𝐼 ∪ 𝐽 = ∪ (∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)))
24	23	ineq1d 4145	. . . . 5 ⊢ (𝜑 → (X𝑥 ∈ 𝐼 ∪ 𝐽 ∩ ∩ 𝑦 ∈ 𝐼 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) = (∪ (∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∩ ∩ 𝑦 ∈ 𝐼 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
25		eqid 2738	. . . . . 6 ⊢ ∪ (∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) = ∪ (∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽))
26	2	topcld 22186	. . . . . . . . . 10 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ (Clsd‘𝐽))
27	16, 26	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ∪ 𝐽 ∈ (Clsd‘𝐽))
28	1, 27	ifcld 4505	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) ∈ (Clsd‘𝐽))
29	19, 16, 28	ptcldmpt 22765	. . . . . . 7 ⊢ (𝜑 → X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) ∈ (Clsd‘(∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽))))
30	29	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) ∈ (Clsd‘(∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽))))
31		simprr 770	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) → 𝑧 ∈ Fin)
32		kelac1.b	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐵:𝑆–1-1-onto→𝐶)
33		f1ofo 6723	. . . . . . . . . . . . . . 15 ⊢ (𝐵:𝑆–1-1-onto→𝐶 → 𝐵:𝑆–onto→𝐶)
34		foima 6693	. . . . . . . . . . . . . . 15 ⊢ (𝐵:𝑆–onto→𝐶 → (𝐵 “ 𝑆) = 𝐶)
35	32, 33, 34	3syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐵 “ 𝑆) = 𝐶)
36	35	eqcomd 2744	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐶 = (𝐵 “ 𝑆))
37		kelac1.z	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑆 ≠ ∅)
38		f1ofn 6717	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵:𝑆–1-1-onto→𝐶 → 𝐵 Fn 𝑆)
39	32, 38	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐵 Fn 𝑆)
40		ssid 3943	. . . . . . . . . . . . . . . 16 ⊢ 𝑆 ⊆ 𝑆
41		fnimaeq0 6566	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 Fn 𝑆 ∧ 𝑆 ⊆ 𝑆) → ((𝐵 “ 𝑆) = ∅ ↔ 𝑆 = ∅))
42	39, 40, 41	sylancl 586	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐵 “ 𝑆) = ∅ ↔ 𝑆 = ∅))
43	42	necon3bid 2988	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐵 “ 𝑆) ≠ ∅ ↔ 𝑆 ≠ ∅))
44	37, 43	mpbird 256	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐵 “ 𝑆) ≠ ∅)
45	36, 44	eqnetrd 3011	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐶 ≠ ∅)
46		n0 4280	. . . . . . . . . . . 12 ⊢ (𝐶 ≠ ∅ ↔ ∃𝑤 𝑤 ∈ 𝐶)
47	45, 46	sylib 217	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ∃𝑤 𝑤 ∈ 𝐶)
48		rexv 3457	. . . . . . . . . . 11 ⊢ (∃𝑤 ∈ V 𝑤 ∈ 𝐶 ↔ ∃𝑤 𝑤 ∈ 𝐶)
49	47, 48	sylibr 233	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ∃𝑤 ∈ V 𝑤 ∈ 𝐶)
50	49	ralrimiva 3103	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑥 ∈ 𝐼 ∃𝑤 ∈ V 𝑤 ∈ 𝐶)
51		ssralv 3987	. . . . . . . . . 10 ⊢ (𝑧 ⊆ 𝐼 → (∀𝑥 ∈ 𝐼 ∃𝑤 ∈ V 𝑤 ∈ 𝐶 → ∀𝑥 ∈ 𝑧 ∃𝑤 ∈ V 𝑤 ∈ 𝐶))
52	51	adantr 481	. . . . . . . . 9 ⊢ ((𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin) → (∀𝑥 ∈ 𝐼 ∃𝑤 ∈ V 𝑤 ∈ 𝐶 → ∀𝑥 ∈ 𝑧 ∃𝑤 ∈ V 𝑤 ∈ 𝐶))
53	50, 52	mpan9 507	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) → ∀𝑥 ∈ 𝑧 ∃𝑤 ∈ V 𝑤 ∈ 𝐶)
54		eleq1 2826	. . . . . . . . 9 ⊢ (𝑤 = (𝑓‘𝑥) → (𝑤 ∈ 𝐶 ↔ (𝑓‘𝑥) ∈ 𝐶))
55	54	ac6sfi 9058	. . . . . . . 8 ⊢ ((𝑧 ∈ Fin ∧ ∀𝑥 ∈ 𝑧 ∃𝑤 ∈ V 𝑤 ∈ 𝐶) → ∃𝑓(𝑓:𝑧⟶V ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶))
56	31, 53, 55	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) → ∃𝑓(𝑓:𝑧⟶V ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶))
57	23	eqcomd 2744	. . . . . . . . . . 11 ⊢ (𝜑 → ∪ (∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) = X𝑥 ∈ 𝐼 ∪ 𝐽)
58	57	ineq1d 4145	. . . . . . . . . 10 ⊢ (𝜑 → (∪ (∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∩ ∩ 𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) = (X𝑥 ∈ 𝐼 ∪ 𝐽 ∩ ∩ 𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
59	58	ad2antrr 723	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → (∪ (∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∩ ∩ 𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) = (X𝑥 ∈ 𝐼 ∪ 𝐽 ∩ ∩ 𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
60		iftrue 4465	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ 𝑧 → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) = (𝑓‘𝑥))
61	60	ad2antrl 725	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ (𝑥 ∈ 𝑧 ∧ (𝑓‘𝑥) ∈ 𝐶)) → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) = (𝑓‘𝑥))
62		simpll 764	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ 𝑥 ∈ 𝑧) → 𝜑)
63		simprl 768	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) → 𝑧 ⊆ 𝐼)
64	63	sselda 3921	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ 𝑥 ∈ 𝑧) → 𝑥 ∈ 𝐼)
65	62, 64, 4	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ 𝑥 ∈ 𝑧) → 𝐶 ⊆ ∪ 𝐽)
66	65	sseld 3920	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ 𝑥 ∈ 𝑧) → ((𝑓‘𝑥) ∈ 𝐶 → (𝑓‘𝑥) ∈ ∪ 𝐽))
67	66	impr 455	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ (𝑥 ∈ 𝑧 ∧ (𝑓‘𝑥) ∈ 𝐶)) → (𝑓‘𝑥) ∈ ∪ 𝐽)
68	61, 67	eqeltrd 2839	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ (𝑥 ∈ 𝑧 ∧ (𝑓‘𝑥) ∈ 𝐶)) → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽)
69	68	expr 457	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ 𝑥 ∈ 𝑧) → ((𝑓‘𝑥) ∈ 𝐶 → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽))
70	69	ralimdva 3108	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) → (∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶 → ∀𝑥 ∈ 𝑧 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽))
71	70	imp 407	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → ∀𝑥 ∈ 𝑧 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽)
72		eldifn 4062	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (𝐼 ∖ 𝑧) → ¬ 𝑥 ∈ 𝑧)
73	72	iffalsed 4470	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝐼 ∖ 𝑧) → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) = 𝑈)
74	73	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) = 𝑈)
75		eldifi 4061	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝐼 ∖ 𝑧) → 𝑥 ∈ 𝐼)
76		kelac1.u	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑈 ∈ ∪ 𝐽)
77	75, 76	sylan2 593	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → 𝑈 ∈ ∪ 𝐽)
78	74, 77	eqeltrd 2839	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽)
79	78	ralrimiva 3103	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∀𝑥 ∈ (𝐼 ∖ 𝑧)if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽)
80	79	ad2antrr 723	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → ∀𝑥 ∈ (𝐼 ∖ 𝑧)if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽)
81		ralun 4126	. . . . . . . . . . . . . 14 ⊢ ((∀𝑥 ∈ 𝑧 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽 ∧ ∀𝑥 ∈ (𝐼 ∖ 𝑧)if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽) → ∀𝑥 ∈ (𝑧 ∪ (𝐼 ∖ 𝑧))if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽)
82	71, 80, 81	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → ∀𝑥 ∈ (𝑧 ∪ (𝐼 ∖ 𝑧))if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽)
83		undif 4415	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ⊆ 𝐼 ↔ (𝑧 ∪ (𝐼 ∖ 𝑧)) = 𝐼)
84	83	biimpi 215	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ⊆ 𝐼 → (𝑧 ∪ (𝐼 ∖ 𝑧)) = 𝐼)
85	84	ad2antrl 725	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) → (𝑧 ∪ (𝐼 ∖ 𝑧)) = 𝐼)
86	85	raleqdv 3348	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) → (∀𝑥 ∈ (𝑧 ∪ (𝐼 ∖ 𝑧))if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽 ↔ ∀𝑥 ∈ 𝐼 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽))
87	86	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → (∀𝑥 ∈ (𝑧 ∪ (𝐼 ∖ 𝑧))if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽 ↔ ∀𝑥 ∈ 𝐼 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽))
88	82, 87	mpbid 231	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → ∀𝑥 ∈ 𝐼 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽)
89	19	ad2antrr 723	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → 𝐼 ∈ V)
90		mptelixpg 8723	. . . . . . . . . . . . 13 ⊢ (𝐼 ∈ V → ((𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ X𝑥 ∈ 𝐼 ∪ 𝐽 ↔ ∀𝑥 ∈ 𝐼 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽))
91	89, 90	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → ((𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ X𝑥 ∈ 𝐼 ∪ 𝐽 ↔ ∀𝑥 ∈ 𝐼 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽))
92	88, 91	mpbird 256	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ X𝑥 ∈ 𝐼 ∪ 𝐽)
93		eleq2 2827	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐶 = if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) → ((𝑓‘𝑥) ∈ 𝐶 ↔ (𝑓‘𝑥) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
94		eleq2 2827	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∪ 𝐽 = if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) → ((𝑓‘𝑥) ∈ ∪ 𝐽 ↔ (𝑓‘𝑥) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
95		simplrr 775	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ (𝑥 ∈ 𝑧 ∧ (𝑓‘𝑥) ∈ 𝐶)) ∧ 𝑥 = 𝑦) → (𝑓‘𝑥) ∈ 𝐶)
96	67	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ (𝑥 ∈ 𝑧 ∧ (𝑓‘𝑥) ∈ 𝐶)) ∧ ¬ 𝑥 = 𝑦) → (𝑓‘𝑥) ∈ ∪ 𝐽)
97	93, 94, 95, 96	ifbothda 4497	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ (𝑥 ∈ 𝑧 ∧ (𝑓‘𝑥) ∈ 𝐶)) → (𝑓‘𝑥) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
98	61, 97	eqeltrd 2839	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ (𝑥 ∈ 𝑧 ∧ (𝑓‘𝑥) ∈ 𝐶)) → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
99	98	expr 457	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ 𝑥 ∈ 𝑧) → ((𝑓‘𝑥) ∈ 𝐶 → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
100	99	ralimdva 3108	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) → (∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶 → ∀𝑥 ∈ 𝑧 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
101	100	imp 407	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → ∀𝑥 ∈ 𝑧 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
102	101	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) ∧ 𝑦 ∈ 𝑧) → ∀𝑥 ∈ 𝑧 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
103	77	adantlr 712	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑧) ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → 𝑈 ∈ ∪ 𝐽)
104	73	adantl 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑧) ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) = 𝑈)
105		disjdifr 4406	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐼 ∖ 𝑧) ∩ 𝑧) = ∅
106	105	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑧) ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → ((𝐼 ∖ 𝑧) ∩ 𝑧) = ∅)
107		simpr 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑧) ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → 𝑥 ∈ (𝐼 ∖ 𝑧))
108		simplr 766	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑧) ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → 𝑦 ∈ 𝑧)
109		disjne 4388	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐼 ∖ 𝑧) ∩ 𝑧) = ∅ ∧ 𝑥 ∈ (𝐼 ∖ 𝑧) ∧ 𝑦 ∈ 𝑧) → 𝑥 ≠ 𝑦)
110	106, 107, 108, 109	syl3anc 1370	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑧) ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → 𝑥 ≠ 𝑦)
111	110	neneqd 2948	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑧) ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → ¬ 𝑥 = 𝑦)
112	111	iffalsed 4470	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑧) ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) = ∪ 𝐽)
113	103, 104, 112	3eltr4d 2854	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑧) ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
114	113	ralrimiva 3103	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑧) → ∀𝑥 ∈ (𝐼 ∖ 𝑧)if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
115	114	adantlr 712	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ 𝑦 ∈ 𝑧) → ∀𝑥 ∈ (𝐼 ∖ 𝑧)if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
116	115	adantlr 712	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) ∧ 𝑦 ∈ 𝑧) → ∀𝑥 ∈ (𝐼 ∖ 𝑧)if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
117		ralun 4126	. . . . . . . . . . . . . . . 16 ⊢ ((∀𝑥 ∈ 𝑧 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) ∧ ∀𝑥 ∈ (𝐼 ∖ 𝑧)if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) → ∀𝑥 ∈ (𝑧 ∪ (𝐼 ∖ 𝑧))if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
118	102, 116, 117	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) ∧ 𝑦 ∈ 𝑧) → ∀𝑥 ∈ (𝑧 ∪ (𝐼 ∖ 𝑧))if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
119	85	raleqdv 3348	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) → (∀𝑥 ∈ (𝑧 ∪ (𝐼 ∖ 𝑧))if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) ↔ ∀𝑥 ∈ 𝐼 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
120	119	ad2antrr 723	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) ∧ 𝑦 ∈ 𝑧) → (∀𝑥 ∈ (𝑧 ∪ (𝐼 ∖ 𝑧))if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) ↔ ∀𝑥 ∈ 𝐼 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
121	118, 120	mpbid 231	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) ∧ 𝑦 ∈ 𝑧) → ∀𝑥 ∈ 𝐼 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
122	19	ad3antrrr 727	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) ∧ 𝑦 ∈ 𝑧) → 𝐼 ∈ V)
123		mptelixpg 8723	. . . . . . . . . . . . . . 15 ⊢ (𝐼 ∈ V → ((𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) ↔ ∀𝑥 ∈ 𝐼 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
124	122, 123	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) ∧ 𝑦 ∈ 𝑧) → ((𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) ↔ ∀𝑥 ∈ 𝐼 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
125	121, 124	mpbird 256	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) ∧ 𝑦 ∈ 𝑧) → (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
126	125	ralrimiva 3103	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → ∀𝑦 ∈ 𝑧 (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
127		mptexg 7097	. . . . . . . . . . . . . . 15 ⊢ (𝐼 ∈ V → (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ V)
128	19, 127	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ V)
129	128	ad2antrr 723	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ V)
130		eliin 4929	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ V → ((𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ ∩ 𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) ↔ ∀𝑦 ∈ 𝑧 (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
131	129, 130	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → ((𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ ∩ 𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) ↔ ∀𝑦 ∈ 𝑧 (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
132	126, 131	mpbird 256	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ ∩ 𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
133	92, 132	elind 4128	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ (X𝑥 ∈ 𝐼 ∪ 𝐽 ∩ ∩ 𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
134	133	ne0d 4269	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → (X𝑥 ∈ 𝐼 ∪ 𝐽 ∩ ∩ 𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) ≠ ∅)
135	59, 134	eqnetrd 3011	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → (∪ (∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∩ ∩ 𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) ≠ ∅)
136	135	adantrl 713	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ (𝑓:𝑧⟶V ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶)) → (∪ (∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∩ ∩ 𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) ≠ ∅)
137	56, 136	exlimddv 1938	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) → (∪ (∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∩ ∩ 𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) ≠ ∅)
138	25, 8, 30, 137	cmpfiiin 40519	. . . . 5 ⊢ (𝜑 → (∪ (∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∩ ∩ 𝑦 ∈ 𝐼 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) ≠ ∅)
139	24, 138	eqnetrd 3011	. . . 4 ⊢ (𝜑 → (X𝑥 ∈ 𝐼 ∪ 𝐽 ∩ ∩ 𝑦 ∈ 𝐼 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) ≠ ∅)
140	7, 139	eqnetrd 3011	. . 3 ⊢ (𝜑 → X𝑥 ∈ 𝐼 𝐶 ≠ ∅)
141		n0 4280	. . 3 ⊢ (X𝑥 ∈ 𝐼 𝐶 ≠ ∅ ↔ ∃𝑦 𝑦 ∈ X𝑥 ∈ 𝐼 𝐶)
142	140, 141	sylib 217	. 2 ⊢ (𝜑 → ∃𝑦 𝑦 ∈ X𝑥 ∈ 𝐼 𝐶)
143		elixp2 8689	. . . . . 6 ⊢ (𝑦 ∈ X𝑥 ∈ 𝐼 𝐶 ↔ (𝑦 ∈ V ∧ 𝑦 Fn 𝐼 ∧ ∀𝑥 ∈ 𝐼 (𝑦‘𝑥) ∈ 𝐶))
144	143	simp3bi 1146	. . . . 5 ⊢ (𝑦 ∈ X𝑥 ∈ 𝐼 𝐶 → ∀𝑥 ∈ 𝐼 (𝑦‘𝑥) ∈ 𝐶)
145		f1ocnv 6728	. . . . . . . 8 ⊢ (𝐵:𝑆–1-1-onto→𝐶 → ◡𝐵:𝐶–1-1-onto→𝑆)
146		f1of 6716	. . . . . . . 8 ⊢ (◡𝐵:𝐶–1-1-onto→𝑆 → ◡𝐵:𝐶⟶𝑆)
147		ffvelrn 6959	. . . . . . . . 9 ⊢ ((◡𝐵:𝐶⟶𝑆 ∧ (𝑦‘𝑥) ∈ 𝐶) → (◡𝐵‘(𝑦‘𝑥)) ∈ 𝑆)
148	147	ex 413	. . . . . . . 8 ⊢ (◡𝐵:𝐶⟶𝑆 → ((𝑦‘𝑥) ∈ 𝐶 → (◡𝐵‘(𝑦‘𝑥)) ∈ 𝑆))
149	32, 145, 146, 148	4syl 19	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑦‘𝑥) ∈ 𝐶 → (◡𝐵‘(𝑦‘𝑥)) ∈ 𝑆))
150	149	ralimdva 3108	. . . . . 6 ⊢ (𝜑 → (∀𝑥 ∈ 𝐼 (𝑦‘𝑥) ∈ 𝐶 → ∀𝑥 ∈ 𝐼 (◡𝐵‘(𝑦‘𝑥)) ∈ 𝑆))
151	150	imp 407	. . . . 5 ⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐼 (𝑦‘𝑥) ∈ 𝐶) → ∀𝑥 ∈ 𝐼 (◡𝐵‘(𝑦‘𝑥)) ∈ 𝑆)
152	144, 151	sylan2 593	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ X𝑥 ∈ 𝐼 𝐶) → ∀𝑥 ∈ 𝐼 (◡𝐵‘(𝑦‘𝑥)) ∈ 𝑆)
153		mptelixpg 8723	. . . . . 6 ⊢ (𝐼 ∈ V → ((𝑥 ∈ 𝐼 ↦ (◡𝐵‘(𝑦‘𝑥))) ∈ X𝑥 ∈ 𝐼 𝑆 ↔ ∀𝑥 ∈ 𝐼 (◡𝐵‘(𝑦‘𝑥)) ∈ 𝑆))
154	19, 153	syl 17	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ 𝐼 ↦ (◡𝐵‘(𝑦‘𝑥))) ∈ X𝑥 ∈ 𝐼 𝑆 ↔ ∀𝑥 ∈ 𝐼 (◡𝐵‘(𝑦‘𝑥)) ∈ 𝑆))
155	154	adantr 481	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ X𝑥 ∈ 𝐼 𝐶) → ((𝑥 ∈ 𝐼 ↦ (◡𝐵‘(𝑦‘𝑥))) ∈ X𝑥 ∈ 𝐼 𝑆 ↔ ∀𝑥 ∈ 𝐼 (◡𝐵‘(𝑦‘𝑥)) ∈ 𝑆))
156	152, 155	mpbird 256	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ X𝑥 ∈ 𝐼 𝐶) → (𝑥 ∈ 𝐼 ↦ (◡𝐵‘(𝑦‘𝑥))) ∈ X𝑥 ∈ 𝐼 𝑆)
157	156	ne0d 4269	. 2 ⊢ ((𝜑 ∧ 𝑦 ∈ X𝑥 ∈ 𝐼 𝐶) → X𝑥 ∈ 𝐼 𝑆 ≠ ∅)
158	142, 157	exlimddv 1938	1 ⊢ (𝜑 → X𝑥 ∈ 𝐼 𝑆 ≠ ∅)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539  ∃wex 1782   ∈ wcel 2106   ≠ wne 2943  ∀wral 3064  ∃wrex 3065  Vcvv 3432   ∖ cdif 3884   ∪ cun 3885   ∩ cin 3886   ⊆ wss 3887  ∅c0 4256  ifcif 4459  ∪ cuni 4839  ∩ ciin 4925   ↦ cmpt 5157  ^◡ccnv 5588   “ cima 5592   Fn wfn 6428  ⟶wf 6429  –onto→wfo 6431  –1-1-onto→wf1o 6432  ‘cfv 6433  Xcixp 8685  Fincfn 8733  ∏_tcpt 17149  Topctop 22042  Clsdccld 22167  Compccmp 22537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-int 4880  df-iun 4926  df-iin 4927  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-om 7713  df-1o 8297  df-er 8498  df-ixp 8686  df-en 8734  df-fin 8737  df-fi 9170  df-topgen 17154  df-pt 17155  df-top 22043  df-bases 22096  df-cld 22170  df-cmp 22538

This theorem is referenced by:  kelac2  40890