Theorem kelac1 43790

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 2763	. . . . . . . 8 ⊢ ∪ 𝐽 = ∪ 𝐽
3	2	cldss 23186	. . . . . . 7 ⊢ (𝐶 ∈ (Clsd‘𝐽) → 𝐶 ⊆ ∪ 𝐽)
4	1, 3	syl 18	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐶 ⊆ ∪ 𝐽)
5	4	ralrimiva 3157	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ 𝐼 𝐶 ⊆ ∪ 𝐽)
6		boxriin 8934	. . . . 5 ⊢ (∀𝑥 ∈ 𝐼 𝐶 ⊆ ∪ 𝐽 → X𝑥 ∈ 𝐼 𝐶 = (X𝑥 ∈ 𝐼 ∪ 𝐽 ∩ ∩ 𝑦 ∈ 𝐼 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
7	5, 6	syl 18	. . . 4 ⊢ (𝜑 → X𝑥 ∈ 𝐼 𝐶 = (X𝑥 ∈ 𝐼 ∪ 𝐽 ∩ ∩ 𝑦 ∈ 𝐼 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
8		kelac1.k	. . . . . . . . 9 ⊢ (𝜑 → (∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∈ Comp)
9		cmptop 23552	. . . . . . . . 9 ⊢ ((∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∈ Comp → (∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∈ Top)
10		0ntop 23062	. . . . . . . . . . 11 ⊢ ¬ ∅ ∈ Top
11		fvprc 6873	. . . . . . . . . . . 12 ⊢ (¬ (𝑥 ∈ 𝐼 ↦ 𝐽) ∈ V → (∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) = ∅)
12	11	eleq1d 2848	. . . . . . . . . . 11 ⊢ (¬ (𝑥 ∈ 𝐼 ↦ 𝐽) ∈ V → ((∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∈ Top ↔ ∅ ∈ Top))
13	10, 12	mtbiri 330	. . . . . . . . . 10 ⊢ (¬ (𝑥 ∈ 𝐼 ↦ 𝐽) ∈ V → ¬ (∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∈ Top)
14	13	con4i 115	. . . . . . . . 9 ⊢ ((∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∈ Top → (𝑥 ∈ 𝐼 ↦ 𝐽) ∈ V)
15	8, 9, 14	3syl 19	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ 𝐽) ∈ V)
16		kelac1.j	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐽 ∈ Top)
17	16	fmpttd 7110	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ 𝐽):𝐼⟶Top)
18		dmfex 7898	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐼 ↦ 𝐽) ∈ V ∧ (𝑥 ∈ 𝐼 ↦ 𝐽):𝐼⟶Top) → 𝐼 ∈ V)
19	15, 17, 18	syl2anc 595	. . . . . . 7 ⊢ (𝜑 → 𝐼 ∈ V)
20	16	ralrimiva 3157	. . . . . . 7 ⊢ (𝜑 → ∀𝑥 ∈ 𝐼 𝐽 ∈ Top)
21		eqid 2763	. . . . . . . 8 ⊢ (∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) = (∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽))
22	21	ptunimpt 23752	. . . . . . 7 ⊢ ((𝐼 ∈ V ∧ ∀𝑥 ∈ 𝐼 𝐽 ∈ Top) → X𝑥 ∈ 𝐼 ∪ 𝐽 = ∪ (∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)))
23	19, 20, 22	syl2anc 595	. . . . . 6 ⊢ (𝜑 → X𝑥 ∈ 𝐼 ∪ 𝐽 = ∪ (∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)))
24	23	ineq1d 4172	. . . . 5 ⊢ (𝜑 → (X𝑥 ∈ 𝐼 ∪ 𝐽 ∩ ∩ 𝑦 ∈ 𝐼 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) = (∪ (∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∩ ∩ 𝑦 ∈ 𝐼 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
25		eqid 2763	. . . . . 6 ⊢ ∪ (∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) = ∪ (∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽))
26	2	topcld 23192	. . . . . . . . . 10 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ (Clsd‘𝐽))
27	16, 26	syl 18	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ∪ 𝐽 ∈ (Clsd‘𝐽))
28	1, 27	ifcld 4534	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) ∈ (Clsd‘𝐽))
29	19, 16, 28	ptcldmpt 23771	. . . . . . 7 ⊢ (𝜑 → X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) ∈ (Clsd‘(∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽))))
30	29	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) ∈ (Clsd‘(∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽))))
31		simprr 784	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) → 𝑧 ∈ Fin)
32		kelac1.b	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐵:𝑆–1-1-onto→𝐶)
33		f1ofo 6828	. . . . . . . . . . . . . . 15 ⊢ (𝐵:𝑆–1-1-onto→𝐶 → 𝐵:𝑆–onto→𝐶)
34		foima 6797	. . . . . . . . . . . . . . 15 ⊢ (𝐵:𝑆–onto→𝐶 → (𝐵 “ 𝑆) = 𝐶)
35	32, 33, 34	3syl 19	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐵 “ 𝑆) = 𝐶)
36	35	eqcomd 2769	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐶 = (𝐵 “ 𝑆))
37		kelac1.z	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑆 ≠ ∅)
38		f1ofn 6821	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵:𝑆–1-1-onto→𝐶 → 𝐵 Fn 𝑆)
39	32, 38	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐵 Fn 𝑆)
40		ssid 3959	. . . . . . . . . . . . . . . 16 ⊢ 𝑆 ⊆ 𝑆
41		fnimaeq0 6668	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 Fn 𝑆 ∧ 𝑆 ⊆ 𝑆) → ((𝐵 “ 𝑆) = ∅ ↔ 𝑆 = ∅))
42	39, 40, 41	sylancl 597	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐵 “ 𝑆) = ∅ ↔ 𝑆 = ∅))
43	42	necon3bid 3002	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐵 “ 𝑆) ≠ ∅ ↔ 𝑆 ≠ ∅))
44	37, 43	mpbird 260	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐵 “ 𝑆) ≠ ∅)
45	36, 44	eqnetrd 3025	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐶 ≠ ∅)
46		n0 4307	. . . . . . . . . . . 12 ⊢ (𝐶 ≠ ∅ ↔ ∃𝑤 𝑤 ∈ 𝐶)
47	45, 46	sylib 221	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ∃𝑤 𝑤 ∈ 𝐶)
48		rexv 3482	. . . . . . . . . . 11 ⊢ (∃𝑤 ∈ V 𝑤 ∈ 𝐶 ↔ ∃𝑤 𝑤 ∈ 𝐶)
49	47, 48	sylibr 237	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ∃𝑤 ∈ V 𝑤 ∈ 𝐶)
50	49	ralrimiva 3157	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑥 ∈ 𝐼 ∃𝑤 ∈ V 𝑤 ∈ 𝐶)
51		ssralv 4006	. . . . . . . . . 10 ⊢ (𝑧 ⊆ 𝐼 → (∀𝑥 ∈ 𝐼 ∃𝑤 ∈ V 𝑤 ∈ 𝐶 → ∀𝑥 ∈ 𝑧 ∃𝑤 ∈ V 𝑤 ∈ 𝐶))
52	51	adantr 485	. . . . . . . . 9 ⊢ ((𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin) → (∀𝑥 ∈ 𝐼 ∃𝑤 ∈ V 𝑤 ∈ 𝐶 → ∀𝑥 ∈ 𝑧 ∃𝑤 ∈ V 𝑤 ∈ 𝐶))
53	50, 52	mpan9 515	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) → ∀𝑥 ∈ 𝑧 ∃𝑤 ∈ V 𝑤 ∈ 𝐶)
54		eleq1 2851	. . . . . . . . 9 ⊢ (𝑤 = (𝑓‘𝑥) → (𝑤 ∈ 𝐶 ↔ (𝑓‘𝑥) ∈ 𝐶))
55	54	ac6sfi 9240	. . . . . . . 8 ⊢ ((𝑧 ∈ Fin ∧ ∀𝑥 ∈ 𝑧 ∃𝑤 ∈ V 𝑤 ∈ 𝐶) → ∃𝑓(𝑓:𝑧⟶V ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶))
56	31, 53, 55	syl2anc 595	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) → ∃𝑓(𝑓:𝑧⟶V ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶))
57	23	eqcomd 2769	. . . . . . . . . . 11 ⊢ (𝜑 → ∪ (∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) = X𝑥 ∈ 𝐼 ∪ 𝐽)
58	57	ineq1d 4172	. . . . . . . . . 10 ⊢ (𝜑 → (∪ (∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∩ ∩ 𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) = (X𝑥 ∈ 𝐼 ∪ 𝐽 ∩ ∩ 𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
59	58	ad2antrr 738	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → (∪ (∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∩ ∩ 𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) = (X𝑥 ∈ 𝐼 ∪ 𝐽 ∩ ∩ 𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
60		iftrue 4493	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ 𝑧 → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) = (𝑓‘𝑥))
61	60	ad2antrl 740	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ (𝑥 ∈ 𝑧 ∧ (𝑓‘𝑥) ∈ 𝐶)) → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) = (𝑓‘𝑥))
62		simpll 778	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ 𝑥 ∈ 𝑧) → 𝜑)
63		simprl 782	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) → 𝑧 ⊆ 𝐼)
64	63	sselda 3937	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ 𝑥 ∈ 𝑧) → 𝑥 ∈ 𝐼)
65	62, 64, 4	syl2anc 595	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ 𝑥 ∈ 𝑧) → 𝐶 ⊆ ∪ 𝐽)
66	65	sseld 3936	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ 𝑥 ∈ 𝑧) → ((𝑓‘𝑥) ∈ 𝐶 → (𝑓‘𝑥) ∈ ∪ 𝐽))
67	66	impr 459	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ (𝑥 ∈ 𝑧 ∧ (𝑓‘𝑥) ∈ 𝐶)) → (𝑓‘𝑥) ∈ ∪ 𝐽)
68	61, 67	eqeltrd 2863	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ (𝑥 ∈ 𝑧 ∧ (𝑓‘𝑥) ∈ 𝐶)) → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽)
69	68	expr 461	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ 𝑥 ∈ 𝑧) → ((𝑓‘𝑥) ∈ 𝐶 → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽))
70	69	ralimdva 3177	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) → (∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶 → ∀𝑥 ∈ 𝑧 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽))
71	70	imp 411	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → ∀𝑥 ∈ 𝑧 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽)
72		eldifn 4086	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (𝐼 ∖ 𝑧) → ¬ 𝑥 ∈ 𝑧)
73	72	iffalsed 4498	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝐼 ∖ 𝑧) → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) = 𝑈)
74	73	adantl 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) = 𝑈)
75		eldifi 4085	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝐼 ∖ 𝑧) → 𝑥 ∈ 𝐼)
76		kelac1.u	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑈 ∈ ∪ 𝐽)
77	75, 76	sylan2 604	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → 𝑈 ∈ ∪ 𝐽)
78	74, 77	eqeltrd 2863	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽)
79	78	ralrimiva 3157	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∀𝑥 ∈ (𝐼 ∖ 𝑧)if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽)
80	79	ad2antrr 738	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → ∀𝑥 ∈ (𝐼 ∖ 𝑧)if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽)
81		ralun 4151	. . . . . . . . . . . . . 14 ⊢ ((∀𝑥 ∈ 𝑧 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽 ∧ ∀𝑥 ∈ (𝐼 ∖ 𝑧)if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽) → ∀𝑥 ∈ (𝑧 ∪ (𝐼 ∖ 𝑧))if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽)
82	71, 80, 81	syl2anc 595	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → ∀𝑥 ∈ (𝑧 ∪ (𝐼 ∖ 𝑧))if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽)
83		undif 4443	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ⊆ 𝐼 ↔ (𝑧 ∪ (𝐼 ∖ 𝑧)) = 𝐼)
84	83	biimpi 219	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ⊆ 𝐼 → (𝑧 ∪ (𝐼 ∖ 𝑧)) = 𝐼)
85	84	ad2antrl 740	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) → (𝑧 ∪ (𝐼 ∖ 𝑧)) = 𝐼)
86	85	raleqdv 3323	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) → (∀𝑥 ∈ (𝑧 ∪ (𝐼 ∖ 𝑧))if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽 ↔ ∀𝑥 ∈ 𝐼 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽))
87	86	adantr 485	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → (∀𝑥 ∈ (𝑧 ∪ (𝐼 ∖ 𝑧))if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽 ↔ ∀𝑥 ∈ 𝐼 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽))
88	82, 87	mpbid 235	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → ∀𝑥 ∈ 𝐼 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽)
89	19	ad2antrr 738	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → 𝐼 ∈ V)
90		mptelixpg 8929	. . . . . . . . . . . . 13 ⊢ (𝐼 ∈ V → ((𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ X𝑥 ∈ 𝐼 ∪ 𝐽 ↔ ∀𝑥 ∈ 𝐼 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽))
91	89, 90	syl 18	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → ((𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ X𝑥 ∈ 𝐼 ∪ 𝐽 ↔ ∀𝑥 ∈ 𝐼 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽))
92	88, 91	mpbird 260	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ X𝑥 ∈ 𝐼 ∪ 𝐽)
93		eleq2 2852	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐶 = if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) → ((𝑓‘𝑥) ∈ 𝐶 ↔ (𝑓‘𝑥) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
94		eleq2 2852	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∪ 𝐽 = if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) → ((𝑓‘𝑥) ∈ ∪ 𝐽 ↔ (𝑓‘𝑥) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
95		simplrr 789	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ (𝑥 ∈ 𝑧 ∧ (𝑓‘𝑥) ∈ 𝐶)) ∧ 𝑥 = 𝑦) → (𝑓‘𝑥) ∈ 𝐶)
96	67	adantr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ (𝑥 ∈ 𝑧 ∧ (𝑓‘𝑥) ∈ 𝐶)) ∧ ¬ 𝑥 = 𝑦) → (𝑓‘𝑥) ∈ ∪ 𝐽)
97	93, 94, 95, 96	ifbothda 4526	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ (𝑥 ∈ 𝑧 ∧ (𝑓‘𝑥) ∈ 𝐶)) → (𝑓‘𝑥) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
98	61, 97	eqeltrd 2863	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ (𝑥 ∈ 𝑧 ∧ (𝑓‘𝑥) ∈ 𝐶)) → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
99	98	expr 461	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ 𝑥 ∈ 𝑧) → ((𝑓‘𝑥) ∈ 𝐶 → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
100	99	ralimdva 3177	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) → (∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶 → ∀𝑥 ∈ 𝑧 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
101	100	imp 411	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → ∀𝑥 ∈ 𝑧 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
102	101	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) ∧ 𝑦 ∈ 𝑧) → ∀𝑥 ∈ 𝑧 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
103	77	adantlr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑧) ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → 𝑈 ∈ ∪ 𝐽)
104	73	adantl 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑧) ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) = 𝑈)
105		disjdifr 4434	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐼 ∖ 𝑧) ∩ 𝑧) = ∅
106	105	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑧) ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → ((𝐼 ∖ 𝑧) ∩ 𝑧) = ∅)
107		simpr 489	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑧) ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → 𝑥 ∈ (𝐼 ∖ 𝑧))
108		simplr 780	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑧) ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → 𝑦 ∈ 𝑧)
109		disjne 4415	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐼 ∖ 𝑧) ∩ 𝑧) = ∅ ∧ 𝑥 ∈ (𝐼 ∖ 𝑧) ∧ 𝑦 ∈ 𝑧) → 𝑥 ≠ 𝑦)
110	106, 107, 108, 109	syl3anc 1398	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑧) ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → 𝑥 ≠ 𝑦)
111	110	neneqd 2963	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑧) ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → ¬ 𝑥 = 𝑦)
112	111	iffalsed 4498	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑧) ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) = ∪ 𝐽)
113	103, 104, 112	3eltr4d 2878	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑧) ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
114	113	ralrimiva 3157	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑧) → ∀𝑥 ∈ (𝐼 ∖ 𝑧)if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
115	114	adantlr 727	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ 𝑦 ∈ 𝑧) → ∀𝑥 ∈ (𝐼 ∖ 𝑧)if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
116	115	adantlr 727	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) ∧ 𝑦 ∈ 𝑧) → ∀𝑥 ∈ (𝐼 ∖ 𝑧)if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
117		ralun 4151	. . . . . . . . . . . . . . . 16 ⊢ ((∀𝑥 ∈ 𝑧 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) ∧ ∀𝑥 ∈ (𝐼 ∖ 𝑧)if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) → ∀𝑥 ∈ (𝑧 ∪ (𝐼 ∖ 𝑧))if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
118	102, 116, 117	syl2anc 595	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) ∧ 𝑦 ∈ 𝑧) → ∀𝑥 ∈ (𝑧 ∪ (𝐼 ∖ 𝑧))if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
119	85	raleqdv 3323	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) → (∀𝑥 ∈ (𝑧 ∪ (𝐼 ∖ 𝑧))if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) ↔ ∀𝑥 ∈ 𝐼 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
120	119	ad2antrr 738	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) ∧ 𝑦 ∈ 𝑧) → (∀𝑥 ∈ (𝑧 ∪ (𝐼 ∖ 𝑧))if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) ↔ ∀𝑥 ∈ 𝐼 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
121	118, 120	mpbid 235	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) ∧ 𝑦 ∈ 𝑧) → ∀𝑥 ∈ 𝐼 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
122	19	ad3antrrr 742	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) ∧ 𝑦 ∈ 𝑧) → 𝐼 ∈ V)
123		mptelixpg 8929	. . . . . . . . . . . . . . 15 ⊢ (𝐼 ∈ V → ((𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) ↔ ∀𝑥 ∈ 𝐼 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
124	122, 123	syl 18	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) ∧ 𝑦 ∈ 𝑧) → ((𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) ↔ ∀𝑥 ∈ 𝐼 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
125	121, 124	mpbird 260	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) ∧ 𝑦 ∈ 𝑧) → (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
126	125	ralrimiva 3157	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → ∀𝑦 ∈ 𝑧 (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
127		mptexg 7219	. . . . . . . . . . . . . . 15 ⊢ (𝐼 ∈ V → (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ V)
128	19, 127	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ V)
129	128	ad2antrr 738	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ V)
130		eliin 4961	. . . . . . . . . . . . 13 ⊢ ((𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ V → ((𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ ∩ 𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) ↔ ∀𝑦 ∈ 𝑧 (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
131	129, 130	syl 18	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → ((𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ ∩ 𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) ↔ ∀𝑦 ∈ 𝑧 (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
132	126, 131	mpbird 260	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ ∩ 𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
133	92, 132	elind 4153	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ (X𝑥 ∈ 𝐼 ∪ 𝐽 ∩ ∩ 𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
134	133	ne0d 4295	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → (X𝑥 ∈ 𝐼 ∪ 𝐽 ∩ ∩ 𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) ≠ ∅)
135	59, 134	eqnetrd 3025	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → (∪ (∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∩ ∩ 𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) ≠ ∅)
136	135	adantrl 728	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ (𝑓:𝑧⟶V ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶)) → (∪ (∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∩ ∩ 𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) ≠ ∅)
137	56, 136	exlimddv 1965	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) → (∪ (∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∩ ∩ 𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) ≠ ∅)
138	25, 8, 30, 137	cmpfiiin 43428	. . . . 5 ⊢ (𝜑 → (∪ (∏t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∩ ∩ 𝑦 ∈ 𝐼 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) ≠ ∅)
139	24, 138	eqnetrd 3025	. . . 4 ⊢ (𝜑 → (X𝑥 ∈ 𝐼 ∪ 𝐽 ∩ ∩ 𝑦 ∈ 𝐼 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) ≠ ∅)
140	7, 139	eqnetrd 3025	. . 3 ⊢ (𝜑 → X𝑥 ∈ 𝐼 𝐶 ≠ ∅)
141		n0 4307	. . 3 ⊢ (X𝑥 ∈ 𝐼 𝐶 ≠ ∅ ↔ ∃𝑦 𝑦 ∈ X𝑥 ∈ 𝐼 𝐶)
142	140, 141	sylib 221	. 2 ⊢ (𝜑 → ∃𝑦 𝑦 ∈ X𝑥 ∈ 𝐼 𝐶)
143		elixp2 8895	. . . . . 6 ⊢ (𝑦 ∈ X𝑥 ∈ 𝐼 𝐶 ↔ (𝑦 ∈ V ∧ 𝑦 Fn 𝐼 ∧ ∀𝑥 ∈ 𝐼 (𝑦‘𝑥) ∈ 𝐶))
144	143	simp3bi 1165	. . . . 5 ⊢ (𝑦 ∈ X𝑥 ∈ 𝐼 𝐶 → ∀𝑥 ∈ 𝐼 (𝑦‘𝑥) ∈ 𝐶)
145		f1ocnv 6833	. . . . . . . 8 ⊢ (𝐵:𝑆–1-1-onto→𝐶 → ◡𝐵:𝐶–1-1-onto→𝑆)
146		f1of 6820	. . . . . . . 8 ⊢ (◡𝐵:𝐶–1-1-onto→𝑆 → ◡𝐵:𝐶⟶𝑆)
147		ffvelcdm 7076	. . . . . . . . 9 ⊢ ((◡𝐵:𝐶⟶𝑆 ∧ (𝑦‘𝑥) ∈ 𝐶) → (◡𝐵‘(𝑦‘𝑥)) ∈ 𝑆)
148	147	ex 417	. . . . . . . 8 ⊢ (◡𝐵:𝐶⟶𝑆 → ((𝑦‘𝑥) ∈ 𝐶 → (◡𝐵‘(𝑦‘𝑥)) ∈ 𝑆))
149	32, 145, 146, 148	4syl 20	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑦‘𝑥) ∈ 𝐶 → (◡𝐵‘(𝑦‘𝑥)) ∈ 𝑆))
150	149	ralimdva 3177	. . . . . 6 ⊢ (𝜑 → (∀𝑥 ∈ 𝐼 (𝑦‘𝑥) ∈ 𝐶 → ∀𝑥 ∈ 𝐼 (◡𝐵‘(𝑦‘𝑥)) ∈ 𝑆))
151	150	imp 411	. . . . 5 ⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐼 (𝑦‘𝑥) ∈ 𝐶) → ∀𝑥 ∈ 𝐼 (◡𝐵‘(𝑦‘𝑥)) ∈ 𝑆)
152	144, 151	sylan2 604	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ X𝑥 ∈ 𝐼 𝐶) → ∀𝑥 ∈ 𝐼 (◡𝐵‘(𝑦‘𝑥)) ∈ 𝑆)
153		mptelixpg 8929	. . . . . 6 ⊢ (𝐼 ∈ V → ((𝑥 ∈ 𝐼 ↦ (◡𝐵‘(𝑦‘𝑥))) ∈ X𝑥 ∈ 𝐼 𝑆 ↔ ∀𝑥 ∈ 𝐼 (◡𝐵‘(𝑦‘𝑥)) ∈ 𝑆))
154	19, 153	syl 18	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ 𝐼 ↦ (◡𝐵‘(𝑦‘𝑥))) ∈ X𝑥 ∈ 𝐼 𝑆 ↔ ∀𝑥 ∈ 𝐼 (◡𝐵‘(𝑦‘𝑥)) ∈ 𝑆))
155	154	adantr 485	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ X𝑥 ∈ 𝐼 𝐶) → ((𝑥 ∈ 𝐼 ↦ (◡𝐵‘(𝑦‘𝑥))) ∈ X𝑥 ∈ 𝐼 𝑆 ↔ ∀𝑥 ∈ 𝐼 (◡𝐵‘(𝑦‘𝑥)) ∈ 𝑆))
156	152, 155	mpbird 260	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ X𝑥 ∈ 𝐼 𝐶) → (𝑥 ∈ 𝐼 ↦ (◡𝐵‘(𝑦‘𝑥))) ∈ X𝑥 ∈ 𝐼 𝑆)
157	156	ne0d 4295	. 2 ⊢ ((𝜑 ∧ 𝑦 ∈ X𝑥 ∈ 𝐼 𝐶) → X𝑥 ∈ 𝐼 𝑆 ≠ ∅)
158	142, 157	exlimddv 1965	1 ⊢ (𝜑 → X𝑥 ∈ 𝐼 𝑆 ≠ ∅)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1570  ∃wex 1809   ∈ wcel 2143   ≠ wne 2958  ∀wral 3079  ∃wrex 3089  Vcvv 3455   ∖ cdif 3902   ∪ cun 3903   ∩ cin 3904   ⊆ wss 3905  ∅c0 4286  ifcif 4487  ∪ cuni 4872  ∩ ciin 4957   ↦ cmpt 5192  ^◡ccnv 5660   “ cima 5664   Fn wfn 6531  ⟶wf 6532  –onto→wfo 6534  –1-1-onto→wf1o 6535  ‘cfv 6536  Xcixp 8891  Fincfn 8939  ∏_tcpt 17486  Topctop 23050  Clsdccld 23173  Compccmp 23543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5238  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-int 4913  df-iun 4958  df-iin 4959  df-br 5110  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-om 7859  df-1o 8449  df-2o 8450  df-ixp 8892  df-en 8940  df-dom 8941  df-fin 8943  df-fi 9367  df-topgen 17491  df-pt 17492  df-top 23051  df-bases 23103  df-cld 23176  df-cmp 23544

This theorem is referenced by:  kelac2  43792