kelac1 - Mathbox for Stefan O'Rear

	Mathbox for Stefan O'Rear		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > kelac1		Structured version Visualization version GIF version

Theorem kelac1 43494

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 2737	. . . . . . . 8 ⊢ ∪ 𝐽 = ∪ 𝐽
3	2	cldss 22972	. . . . . . 7 ⊢ (𝐶 ∈ (Clsd‘𝐽) → 𝐶 ⊆ ∪ 𝐽)
4	1, 3	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐶 ⊆ ∪ 𝐽)
5	4	ralrimiva 3130	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ 𝐼 𝐶 ⊆ ∪ 𝐽)
6		boxriin 8879	. . . . 5 ⊢ (∀𝑥 ∈ 𝐼 𝐶 ⊆ ∪ 𝐽 → X𝑥 ∈ 𝐼 𝐶 = (X𝑥 ∈ 𝐼 ∪ 𝐽 ∩ ∩ 𝑦 ∈ 𝐼 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
7	5, 6	syl 17	. . . 4 ⊢ (𝜑 → X𝑥 ∈ 𝐼 𝐶 = (X𝑥 ∈ 𝐼 ∪ 𝐽 ∩ ∩ 𝑦 ∈ 𝐼 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
8		kelac1.k	. . . . . . . . 9 ⊢ (𝜑 → (∏_t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∈ Comp)
9		cmptop 23338	. . . . . . . . 9 ⊢ ((∏_t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∈ Comp → (∏_t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∈ Top)
10		0ntop 22848	. . . . . . . . . . 11 ⊢ ¬ ∅ ∈ Top
11		fvprc 6824	. . . . . . . . . . . 12 ⊢ (¬ (𝑥 ∈ 𝐼 ↦ 𝐽) ∈ V → (∏_t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) = ∅)
12	11	eleq1d 2822	. . . . . . . . . . 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 7059	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ 𝐽):𝐼⟶Top)
18		dmfex 7847	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐼 ↦ 𝐽) ∈ V ∧ (𝑥 ∈ 𝐼 ↦ 𝐽):𝐼⟶Top) → 𝐼 ∈ V)
19	15, 17, 18	syl2anc 585	. . . . . . 7 ⊢ (𝜑 → 𝐼 ∈ V)
20	16	ralrimiva 3130	. . . . . . 7 ⊢ (𝜑 → ∀𝑥 ∈ 𝐼 𝐽 ∈ Top)
21		eqid 2737	. . . . . . . 8 ⊢ (∏_t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) = (∏_t‘(𝑥 ∈ 𝐼 ↦ 𝐽))
22	21	ptunimpt 23538	. . . . . . 7 ⊢ ((𝐼 ∈ V ∧ ∀𝑥 ∈ 𝐼 𝐽 ∈ Top) → X𝑥 ∈ 𝐼 ∪ 𝐽 = ∪ (∏_t‘(𝑥 ∈ 𝐼 ↦ 𝐽)))
23	19, 20, 22	syl2anc 585	. . . . . 6 ⊢ (𝜑 → X𝑥 ∈ 𝐼 ∪ 𝐽 = ∪ (∏_t‘(𝑥 ∈ 𝐼 ↦ 𝐽)))
24	23	ineq1d 4160	. . . . 5 ⊢ (𝜑 → (X𝑥 ∈ 𝐼 ∪ 𝐽 ∩ ∩ 𝑦 ∈ 𝐼 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) = (∪ (∏_t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∩ ∩ 𝑦 ∈ 𝐼 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
25		eqid 2737	. . . . . 6 ⊢ ∪ (∏_t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) = ∪ (∏_t‘(𝑥 ∈ 𝐼 ↦ 𝐽))
26	2	topcld 22978	. . . . . . . . . 10 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ (Clsd‘𝐽))
27	16, 26	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ∪ 𝐽 ∈ (Clsd‘𝐽))
28	1, 27	ifcld 4514	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) ∈ (Clsd‘𝐽))
29	19, 16, 28	ptcldmpt 23557	. . . . . . 7 ⊢ (𝜑 → X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) ∈ (Clsd‘(∏_t‘(𝑥 ∈ 𝐼 ↦ 𝐽))))
30	29	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) ∈ (Clsd‘(∏_t‘(𝑥 ∈ 𝐼 ↦ 𝐽))))
31		simprr 773	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) → 𝑧 ∈ Fin)
32		kelac1.b	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐵:𝑆–1-1-onto→𝐶)
33		f1ofo 6779	. . . . . . . . . . . . . . 15 ⊢ (𝐵:𝑆–1-1-onto→𝐶 → 𝐵:𝑆–onto→𝐶)
34		foima 6749	. . . . . . . . . . . . . . 15 ⊢ (𝐵:𝑆–onto→𝐶 → (𝐵 “ 𝑆) = 𝐶)
35	32, 33, 34	3syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐵 “ 𝑆) = 𝐶)
36	35	eqcomd 2743	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐶 = (𝐵 “ 𝑆))
37		kelac1.z	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑆 ≠ ∅)
38		f1ofn 6773	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵:𝑆–1-1-onto→𝐶 → 𝐵 Fn 𝑆)
39	32, 38	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐵 Fn 𝑆)
40		ssid 3945	. . . . . . . . . . . . . . . 16 ⊢ 𝑆 ⊆ 𝑆
41		fnimaeq0 6623	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 Fn 𝑆 ∧ 𝑆 ⊆ 𝑆) → ((𝐵 “ 𝑆) = ∅ ↔ 𝑆 = ∅))
42	39, 40, 41	sylancl 587	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐵 “ 𝑆) = ∅ ↔ 𝑆 = ∅))
43	42	necon3bid 2977	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐵 “ 𝑆) ≠ ∅ ↔ 𝑆 ≠ ∅))
44	37, 43	mpbird 257	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐵 “ 𝑆) ≠ ∅)
45	36, 44	eqnetrd 3000	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐶 ≠ ∅)
46		n0 4294	. . . . . . . . . . . 12 ⊢ (𝐶 ≠ ∅ ↔ ∃𝑤 𝑤 ∈ 𝐶)
47	45, 46	sylib 218	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ∃𝑤 𝑤 ∈ 𝐶)
48		rexv 3458	. . . . . . . . . . 11 ⊢ (∃𝑤 ∈ V 𝑤 ∈ 𝐶 ↔ ∃𝑤 𝑤 ∈ 𝐶)
49	47, 48	sylibr 234	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ∃𝑤 ∈ V 𝑤 ∈ 𝐶)
50	49	ralrimiva 3130	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑥 ∈ 𝐼 ∃𝑤 ∈ V 𝑤 ∈ 𝐶)
51		ssralv 3991	. . . . . . . . . 10 ⊢ (𝑧 ⊆ 𝐼 → (∀𝑥 ∈ 𝐼 ∃𝑤 ∈ V 𝑤 ∈ 𝐶 → ∀𝑥 ∈ 𝑧 ∃𝑤 ∈ V 𝑤 ∈ 𝐶))
52	51	adantr 480	. . . . . . . . 9 ⊢ ((𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin) → (∀𝑥 ∈ 𝐼 ∃𝑤 ∈ V 𝑤 ∈ 𝐶 → ∀𝑥 ∈ 𝑧 ∃𝑤 ∈ V 𝑤 ∈ 𝐶))
53	50, 52	mpan9 506	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) → ∀𝑥 ∈ 𝑧 ∃𝑤 ∈ V 𝑤 ∈ 𝐶)
54		eleq1 2825	. . . . . . . . 9 ⊢ (𝑤 = (𝑓‘𝑥) → (𝑤 ∈ 𝐶 ↔ (𝑓‘𝑥) ∈ 𝐶))
55	54	ac6sfi 9185	. . . . . . . 8 ⊢ ((𝑧 ∈ Fin ∧ ∀𝑥 ∈ 𝑧 ∃𝑤 ∈ V 𝑤 ∈ 𝐶) → ∃𝑓(𝑓:𝑧⟶V ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶))
56	31, 53, 55	syl2anc 585	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) → ∃𝑓(𝑓:𝑧⟶V ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶))
57	23	eqcomd 2743	. . . . . . . . . . 11 ⊢ (𝜑 → ∪ (∏_t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) = X𝑥 ∈ 𝐼 ∪ 𝐽)
58	57	ineq1d 4160	. . . . . . . . . 10 ⊢ (𝜑 → (∪ (∏_t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∩ ∩ 𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) = (X𝑥 ∈ 𝐼 ∪ 𝐽 ∩ ∩ 𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
59	58	ad2antrr 727	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → (∪ (∏_t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∩ ∩ 𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) = (X𝑥 ∈ 𝐼 ∪ 𝐽 ∩ ∩ 𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
60		iftrue 4473	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ 𝑧 → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) = (𝑓‘𝑥))
61	60	ad2antrl 729	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ (𝑥 ∈ 𝑧 ∧ (𝑓‘𝑥) ∈ 𝐶)) → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) = (𝑓‘𝑥))
62		simpll 767	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ 𝑥 ∈ 𝑧) → 𝜑)
63		simprl 771	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) → 𝑧 ⊆ 𝐼)
64	63	sselda 3922	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ 𝑥 ∈ 𝑧) → 𝑥 ∈ 𝐼)
65	62, 64, 4	syl2anc 585	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ 𝑥 ∈ 𝑧) → 𝐶 ⊆ ∪ 𝐽)
66	65	sseld 3921	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ 𝑥 ∈ 𝑧) → ((𝑓‘𝑥) ∈ 𝐶 → (𝑓‘𝑥) ∈ ∪ 𝐽))
67	66	impr 454	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ (𝑥 ∈ 𝑧 ∧ (𝑓‘𝑥) ∈ 𝐶)) → (𝑓‘𝑥) ∈ ∪ 𝐽)
68	61, 67	eqeltrd 2837	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ (𝑥 ∈ 𝑧 ∧ (𝑓‘𝑥) ∈ 𝐶)) → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽)
69	68	expr 456	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ 𝑥 ∈ 𝑧) → ((𝑓‘𝑥) ∈ 𝐶 → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽))
70	69	ralimdva 3150	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) → (∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶 → ∀𝑥 ∈ 𝑧 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽))
71	70	imp 406	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → ∀𝑥 ∈ 𝑧 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽)
72		eldifn 4073	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (𝐼 ∖ 𝑧) → ¬ 𝑥 ∈ 𝑧)
73	72	iffalsed 4478	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝐼 ∖ 𝑧) → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) = 𝑈)
74	73	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) = 𝑈)
75		eldifi 4072	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝐼 ∖ 𝑧) → 𝑥 ∈ 𝐼)
76		kelac1.u	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑈 ∈ ∪ 𝐽)
77	75, 76	sylan2 594	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → 𝑈 ∈ ∪ 𝐽)
78	74, 77	eqeltrd 2837	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽)
79	78	ralrimiva 3130	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∀𝑥 ∈ (𝐼 ∖ 𝑧)if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽)
80	79	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → ∀𝑥 ∈ (𝐼 ∖ 𝑧)if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽)
81		ralun 4139	. . . . . . . . . . . . . 14 ⊢ ((∀𝑥 ∈ 𝑧 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽 ∧ ∀𝑥 ∈ (𝐼 ∖ 𝑧)if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽) → ∀𝑥 ∈ (𝑧 ∪ (𝐼 ∖ 𝑧))if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽)
82	71, 80, 81	syl2anc 585	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → ∀𝑥 ∈ (𝑧 ∪ (𝐼 ∖ 𝑧))if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽)
83		undif 4423	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ⊆ 𝐼 ↔ (𝑧 ∪ (𝐼 ∖ 𝑧)) = 𝐼)
84	83	biimpi 216	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ⊆ 𝐼 → (𝑧 ∪ (𝐼 ∖ 𝑧)) = 𝐼)
85	84	ad2antrl 729	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) → (𝑧 ∪ (𝐼 ∖ 𝑧)) = 𝐼)
86	85	raleqdv 3296	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) → (∀𝑥 ∈ (𝑧 ∪ (𝐼 ∖ 𝑧))if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽 ↔ ∀𝑥 ∈ 𝐼 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽))
87	86	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → (∀𝑥 ∈ (𝑧 ∪ (𝐼 ∖ 𝑧))if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽 ↔ ∀𝑥 ∈ 𝐼 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽))
88	82, 87	mpbid 232	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → ∀𝑥 ∈ 𝐼 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽)
89	19	ad2antrr 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → 𝐼 ∈ V)
90		mptelixpg 8874	. . . . . . . . . . . . 13 ⊢ (𝐼 ∈ V → ((𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ X𝑥 ∈ 𝐼 ∪ 𝐽 ↔ ∀𝑥 ∈ 𝐼 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽))
91	89, 90	syl 17	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → ((𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ X𝑥 ∈ 𝐼 ∪ 𝐽 ↔ ∀𝑥 ∈ 𝐼 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽))
92	88, 91	mpbird 257	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ X𝑥 ∈ 𝐼 ∪ 𝐽)
93		eleq2 2826	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐶 = if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) → ((𝑓‘𝑥) ∈ 𝐶 ↔ (𝑓‘𝑥) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
94		eleq2 2826	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∪ 𝐽 = if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) → ((𝑓‘𝑥) ∈ ∪ 𝐽 ↔ (𝑓‘𝑥) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
95		simplrr 778	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ (𝑥 ∈ 𝑧 ∧ (𝑓‘𝑥) ∈ 𝐶)) ∧ 𝑥 = 𝑦) → (𝑓‘𝑥) ∈ 𝐶)
96	67	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ (𝑥 ∈ 𝑧 ∧ (𝑓‘𝑥) ∈ 𝐶)) ∧ ¬ 𝑥 = 𝑦) → (𝑓‘𝑥) ∈ ∪ 𝐽)
97	93, 94, 95, 96	ifbothda 4506	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ (𝑥 ∈ 𝑧 ∧ (𝑓‘𝑥) ∈ 𝐶)) → (𝑓‘𝑥) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
98	61, 97	eqeltrd 2837	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ (𝑥 ∈ 𝑧 ∧ (𝑓‘𝑥) ∈ 𝐶)) → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
99	98	expr 456	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ 𝑥 ∈ 𝑧) → ((𝑓‘𝑥) ∈ 𝐶 → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
100	99	ralimdva 3150	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) → (∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶 → ∀𝑥 ∈ 𝑧 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
101	100	imp 406	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → ∀𝑥 ∈ 𝑧 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
102	101	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) ∧ 𝑦 ∈ 𝑧) → ∀𝑥 ∈ 𝑧 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
103	77	adantlr 716	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑧) ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → 𝑈 ∈ ∪ 𝐽)
104	73	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑧) ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) = 𝑈)
105		disjdifr 4414	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐼 ∖ 𝑧) ∩ 𝑧) = ∅
106	105	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑧) ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → ((𝐼 ∖ 𝑧) ∩ 𝑧) = ∅)
107		simpr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑧) ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → 𝑥 ∈ (𝐼 ∖ 𝑧))
108		simplr 769	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑧) ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → 𝑦 ∈ 𝑧)
109		disjne 4396	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐼 ∖ 𝑧) ∩ 𝑧) = ∅ ∧ 𝑥 ∈ (𝐼 ∖ 𝑧) ∧ 𝑦 ∈ 𝑧) → 𝑥 ≠ 𝑦)
110	106, 107, 108, 109	syl3anc 1374	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑧) ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → 𝑥 ≠ 𝑦)
111	110	neneqd 2938	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑧) ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → ¬ 𝑥 = 𝑦)
112	111	iffalsed 4478	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑧) ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) = ∪ 𝐽)
113	103, 104, 112	3eltr4d 2852	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑧) ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
114	113	ralrimiva 3130	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑧) → ∀𝑥 ∈ (𝐼 ∖ 𝑧)if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
115	114	adantlr 716	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ 𝑦 ∈ 𝑧) → ∀𝑥 ∈ (𝐼 ∖ 𝑧)if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
116	115	adantlr 716	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) ∧ 𝑦 ∈ 𝑧) → ∀𝑥 ∈ (𝐼 ∖ 𝑧)if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
117		ralun 4139	. . . . . . . . . . . . . . . 16 ⊢ ((∀𝑥 ∈ 𝑧 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) ∧ ∀𝑥 ∈ (𝐼 ∖ 𝑧)if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) → ∀𝑥 ∈ (𝑧 ∪ (𝐼 ∖ 𝑧))if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
118	102, 116, 117	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) ∧ 𝑦 ∈ 𝑧) → ∀𝑥 ∈ (𝑧 ∪ (𝐼 ∖ 𝑧))if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
119	85	raleqdv 3296	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) → (∀𝑥 ∈ (𝑧 ∪ (𝐼 ∖ 𝑧))if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) ↔ ∀𝑥 ∈ 𝐼 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
120	119	ad2antrr 727	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) ∧ 𝑦 ∈ 𝑧) → (∀𝑥 ∈ (𝑧 ∪ (𝐼 ∖ 𝑧))if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) ↔ ∀𝑥 ∈ 𝐼 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
121	118, 120	mpbid 232	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) ∧ 𝑦 ∈ 𝑧) → ∀𝑥 ∈ 𝐼 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
122	19	ad3antrrr 731	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) ∧ 𝑦 ∈ 𝑧) → 𝐼 ∈ V)
123		mptelixpg 8874	. . . . . . . . . . . . . . 15 ⊢ (𝐼 ∈ V → ((𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) ↔ ∀𝑥 ∈ 𝐼 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
124	122, 123	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) ∧ 𝑦 ∈ 𝑧) → ((𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) ↔ ∀𝑥 ∈ 𝐼 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
125	121, 124	mpbird 257	. . . . . . . . . . . . 13 ⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) ∧ 𝑦 ∈ 𝑧) → (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
126	125	ralrimiva 3130	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → ∀𝑦 ∈ 𝑧 (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
127		mptexg 7167	. . . . . . . . . . . . . . 15 ⊢ (𝐼 ∈ V → (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ V)
128	19, 127	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ V)
129	128	ad2antrr 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ V)
130		eliin 4939	. . . . . . . . . . . . 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 257	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ ∩ 𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
133	92, 132	elind 4141	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ (X𝑥 ∈ 𝐼 ∪ 𝐽 ∩ ∩ 𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
134	133	ne0d 4283	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → (X𝑥 ∈ 𝐼 ∪ 𝐽 ∩ ∩ 𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) ≠ ∅)
135	59, 134	eqnetrd 3000	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → (∪ (∏_t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∩ ∩ 𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) ≠ ∅)
136	135	adantrl 717	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ (𝑓:𝑧⟶V ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶)) → (∪ (∏_t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∩ ∩ 𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) ≠ ∅)
137	56, 136	exlimddv 1937	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) → (∪ (∏_t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∩ ∩ 𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) ≠ ∅)
138	25, 8, 30, 137	cmpfiiin 43128	. . . . 5 ⊢ (𝜑 → (∪ (∏_t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∩ ∩ 𝑦 ∈ 𝐼 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) ≠ ∅)
139	24, 138	eqnetrd 3000	. . . 4 ⊢ (𝜑 → (X𝑥 ∈ 𝐼 ∪ 𝐽 ∩ ∩ 𝑦 ∈ 𝐼 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) ≠ ∅)
140	7, 139	eqnetrd 3000	. . 3 ⊢ (𝜑 → X𝑥 ∈ 𝐼 𝐶 ≠ ∅)
141		n0 4294	. . 3 ⊢ (X𝑥 ∈ 𝐼 𝐶 ≠ ∅ ↔ ∃𝑦 𝑦 ∈ X𝑥 ∈ 𝐼 𝐶)
142	140, 141	sylib 218	. 2 ⊢ (𝜑 → ∃𝑦 𝑦 ∈ X𝑥 ∈ 𝐼 𝐶)
143		elixp2 8840	. . . . . 6 ⊢ (𝑦 ∈ X𝑥 ∈ 𝐼 𝐶 ↔ (𝑦 ∈ V ∧ 𝑦 Fn 𝐼 ∧ ∀𝑥 ∈ 𝐼 (𝑦‘𝑥) ∈ 𝐶))
144	143	simp3bi 1148	. . . . 5 ⊢ (𝑦 ∈ X𝑥 ∈ 𝐼 𝐶 → ∀𝑥 ∈ 𝐼 (𝑦‘𝑥) ∈ 𝐶)
145		f1ocnv 6784	. . . . . . . 8 ⊢ (𝐵:𝑆–1-1-onto→𝐶 → ^◡𝐵:𝐶–1-1-onto→𝑆)
146		f1of 6772	. . . . . . . 8 ⊢ (^◡𝐵:𝐶–1-1-onto→𝑆 → ^◡𝐵:𝐶⟶𝑆)
147		ffvelcdm 7025	. . . . . . . . 9 ⊢ ((^◡𝐵:𝐶⟶𝑆 ∧ (𝑦‘𝑥) ∈ 𝐶) → (^◡𝐵‘(𝑦‘𝑥)) ∈ 𝑆)
148	147	ex 412	. . . . . . . 8 ⊢ (^◡𝐵:𝐶⟶𝑆 → ((𝑦‘𝑥) ∈ 𝐶 → (^◡𝐵‘(𝑦‘𝑥)) ∈ 𝑆))
149	32, 145, 146, 148	4syl 19	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑦‘𝑥) ∈ 𝐶 → (^◡𝐵‘(𝑦‘𝑥)) ∈ 𝑆))
150	149	ralimdva 3150	. . . . . 6 ⊢ (𝜑 → (∀𝑥 ∈ 𝐼 (𝑦‘𝑥) ∈ 𝐶 → ∀𝑥 ∈ 𝐼 (^◡𝐵‘(𝑦‘𝑥)) ∈ 𝑆))
151	150	imp 406	. . . . 5 ⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐼 (𝑦‘𝑥) ∈ 𝐶) → ∀𝑥 ∈ 𝐼 (^◡𝐵‘(𝑦‘𝑥)) ∈ 𝑆)
152	144, 151	sylan2 594	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ X𝑥 ∈ 𝐼 𝐶) → ∀𝑥 ∈ 𝐼 (^◡𝐵‘(𝑦‘𝑥)) ∈ 𝑆)
153		mptelixpg 8874	. . . . . 6 ⊢ (𝐼 ∈ V → ((𝑥 ∈ 𝐼 ↦ (^◡𝐵‘(𝑦‘𝑥))) ∈ X𝑥 ∈ 𝐼 𝑆 ↔ ∀𝑥 ∈ 𝐼 (^◡𝐵‘(𝑦‘𝑥)) ∈ 𝑆))
154	19, 153	syl 17	. . . . 5 ⊢ (𝜑 → ((𝑥 ∈ 𝐼 ↦ (^◡𝐵‘(𝑦‘𝑥))) ∈ X𝑥 ∈ 𝐼 𝑆 ↔ ∀𝑥 ∈ 𝐼 (^◡𝐵‘(𝑦‘𝑥)) ∈ 𝑆))
155	154	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ X𝑥 ∈ 𝐼 𝐶) → ((𝑥 ∈ 𝐼 ↦ (^◡𝐵‘(𝑦‘𝑥))) ∈ X𝑥 ∈ 𝐼 𝑆 ↔ ∀𝑥 ∈ 𝐼 (^◡𝐵‘(𝑦‘𝑥)) ∈ 𝑆))
156	152, 155	mpbird 257	. . 3 ⊢ ((𝜑 ∧ 𝑦 ∈ X𝑥 ∈ 𝐼 𝐶) → (𝑥 ∈ 𝐼 ↦ (^◡𝐵‘(𝑦‘𝑥))) ∈ X𝑥 ∈ 𝐼 𝑆)
157	156	ne0d 4283	. 2 ⊢ ((𝜑 ∧ 𝑦 ∈ X𝑥 ∈ 𝐼 𝐶) → X𝑥 ∈ 𝐼 𝑆 ≠ ∅)
158	142, 157	exlimddv 1937	1 ⊢ (𝜑 → X𝑥 ∈ 𝐼 𝑆 ≠ ∅)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1542 ∃wex 1781 ∈ wcel 2114 ≠ wne 2933 ∀wral 3052 ∃wrex 3062 Vcvv 3430 ∖ cdif 3887 ∪ cun 3888 ∩ cin 3889 ⊆ wss 3890 ∅c0 4274 ifcif 4467 ∪ cuni 4851 ∩ ciin 4935 ↦ cmpt 5167 ^◡ccnv 5621 “ cima 5625 Fn wfn 6485 ⟶wf 6486 –onto→wfo 6488 –1-1-onto→wf1o 6489 ‘cfv 6490 Xcixp 8836 Fincfn 8884 ∏_tcpt 17359 Topctop 22836 Clsdccld 22959 Compccmp 23329

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5300 ax-pr 5368 ax-un 7680

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-ral 3053 df-rex 3063 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-iin 4937 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5517 df-eprel 5522 df-po 5530 df-so 5531 df-fr 5575 df-we 5577 df-xp 5628 df-rel 5629 df-cnv 5630 df-co 5631 df-dm 5632 df-rn 5633 df-res 5634 df-ima 5635 df-ord 6318 df-on 6319 df-lim 6320 df-suc 6321 df-iota 6446 df-fun 6492 df-fn 6493 df-f 6494 df-f1 6495 df-fo 6496 df-f1o 6497 df-fv 6498 df-om 7809 df-1o 8396 df-2o 8397 df-ixp 8837 df-en 8885 df-dom 8886 df-fin 8888 df-fi 9315 df-topgen 17364 df-pt 17365 df-top 22837 df-bases 22889 df-cld 22962 df-cmp 23330

This theorem is referenced by: kelac2 43496

W3C validator