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 41790

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 2732	. . . . . . . 8 ⊢ ∪ 𝐽 = ∪ 𝐽
3	2	cldss 22524	. . . . . . 7 ⊢ (𝐶 ∈ (Clsd‘𝐽) → 𝐶 ⊆ ∪ 𝐽)
4	1, 3	syl 17	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐶 ⊆ ∪ 𝐽)
5	4	ralrimiva 3146	. . . . 5 ⊢ (𝜑 → ∀𝑥 ∈ 𝐼 𝐶 ⊆ ∪ 𝐽)
6		boxriin 8930	. . . . 5 ⊢ (∀𝑥 ∈ 𝐼 𝐶 ⊆ ∪ 𝐽 → X𝑥 ∈ 𝐼 𝐶 = (X𝑥 ∈ 𝐼 ∪ 𝐽 ∩ ∩ 𝑦 ∈ 𝐼 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
7	5, 6	syl 17	. . . 4 ⊢ (𝜑 → X𝑥 ∈ 𝐼 𝐶 = (X𝑥 ∈ 𝐼 ∪ 𝐽 ∩ ∩ 𝑦 ∈ 𝐼 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
8		kelac1.k	. . . . . . . . 9 ⊢ (𝜑 → (∏_t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∈ Comp)
9		cmptop 22890	. . . . . . . . 9 ⊢ ((∏_t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∈ Comp → (∏_t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∈ Top)
10		0ntop 22398	. . . . . . . . . . 11 ⊢ ¬ ∅ ∈ Top
11		fvprc 6880	. . . . . . . . . . . 12 ⊢ (¬ (𝑥 ∈ 𝐼 ↦ 𝐽) ∈ V → (∏_t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) = ∅)
12	11	eleq1d 2818	. . . . . . . . . . 11 ⊢ (¬ (𝑥 ∈ 𝐼 ↦ 𝐽) ∈ V → ((∏_t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∈ Top ↔ ∅ ∈ Top))
13	10, 12	mtbiri 326	. . . . . . . . . 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 7111	. . . . . . . 8 ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ 𝐽):𝐼⟶Top)
18		dmfex 7894	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐼 ↦ 𝐽) ∈ V ∧ (𝑥 ∈ 𝐼 ↦ 𝐽):𝐼⟶Top) → 𝐼 ∈ V)
19	15, 17, 18	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → 𝐼 ∈ V)
20	16	ralrimiva 3146	. . . . . . 7 ⊢ (𝜑 → ∀𝑥 ∈ 𝐼 𝐽 ∈ Top)
21		eqid 2732	. . . . . . . 8 ⊢ (∏_t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) = (∏_t‘(𝑥 ∈ 𝐼 ↦ 𝐽))
22	21	ptunimpt 23090	. . . . . . 7 ⊢ ((𝐼 ∈ V ∧ ∀𝑥 ∈ 𝐼 𝐽 ∈ Top) → X𝑥 ∈ 𝐼 ∪ 𝐽 = ∪ (∏_t‘(𝑥 ∈ 𝐼 ↦ 𝐽)))
23	19, 20, 22	syl2anc 584	. . . . . 6 ⊢ (𝜑 → X𝑥 ∈ 𝐼 ∪ 𝐽 = ∪ (∏_t‘(𝑥 ∈ 𝐼 ↦ 𝐽)))
24	23	ineq1d 4210	. . . . 5 ⊢ (𝜑 → (X𝑥 ∈ 𝐼 ∪ 𝐽 ∩ ∩ 𝑦 ∈ 𝐼 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) = (∪ (∏_t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∩ ∩ 𝑦 ∈ 𝐼 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
25		eqid 2732	. . . . . 6 ⊢ ∪ (∏_t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) = ∪ (∏_t‘(𝑥 ∈ 𝐼 ↦ 𝐽))
26	2	topcld 22530	. . . . . . . . . 10 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ (Clsd‘𝐽))
27	16, 26	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ∪ 𝐽 ∈ (Clsd‘𝐽))
28	1, 27	ifcld 4573	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) ∈ (Clsd‘𝐽))
29	19, 16, 28	ptcldmpt 23109	. . . . . . 7 ⊢ (𝜑 → X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) ∈ (Clsd‘(∏_t‘(𝑥 ∈ 𝐼 ↦ 𝐽))))
30	29	adantr 481	. . . . . 6 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐼) → X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) ∈ (Clsd‘(∏_t‘(𝑥 ∈ 𝐼 ↦ 𝐽))))
31		simprr 771	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) → 𝑧 ∈ Fin)
32		kelac1.b	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐵:𝑆–1-1-onto→𝐶)
33		f1ofo 6837	. . . . . . . . . . . . . . 15 ⊢ (𝐵:𝑆–1-1-onto→𝐶 → 𝐵:𝑆–onto→𝐶)
34		foima 6807	. . . . . . . . . . . . . . 15 ⊢ (𝐵:𝑆–onto→𝐶 → (𝐵 “ 𝑆) = 𝐶)
35	32, 33, 34	3syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐵 “ 𝑆) = 𝐶)
36	35	eqcomd 2738	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐶 = (𝐵 “ 𝑆))
37		kelac1.z	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑆 ≠ ∅)
38		f1ofn 6831	. . . . . . . . . . . . . . . . 17 ⊢ (𝐵:𝑆–1-1-onto→𝐶 → 𝐵 Fn 𝑆)
39	32, 38	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐵 Fn 𝑆)
40		ssid 4003	. . . . . . . . . . . . . . . 16 ⊢ 𝑆 ⊆ 𝑆
41		fnimaeq0 6680	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 Fn 𝑆 ∧ 𝑆 ⊆ 𝑆) → ((𝐵 “ 𝑆) = ∅ ↔ 𝑆 = ∅))
42	39, 40, 41	sylancl 586	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐵 “ 𝑆) = ∅ ↔ 𝑆 = ∅))
43	42	necon3bid 2985	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝐵 “ 𝑆) ≠ ∅ ↔ 𝑆 ≠ ∅))
44	37, 43	mpbird 256	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝐵 “ 𝑆) ≠ ∅)
45	36, 44	eqnetrd 3008	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝐶 ≠ ∅)
46		n0 4345	. . . . . . . . . . . 12 ⊢ (𝐶 ≠ ∅ ↔ ∃𝑤 𝑤 ∈ 𝐶)
47	45, 46	sylib 217	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ∃𝑤 𝑤 ∈ 𝐶)
48		rexv 3499	. . . . . . . . . . 11 ⊢ (∃𝑤 ∈ V 𝑤 ∈ 𝐶 ↔ ∃𝑤 𝑤 ∈ 𝐶)
49	47, 48	sylibr 233	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ∃𝑤 ∈ V 𝑤 ∈ 𝐶)
50	49	ralrimiva 3146	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑥 ∈ 𝐼 ∃𝑤 ∈ V 𝑤 ∈ 𝐶)
51		ssralv 4049	. . . . . . . . . 10 ⊢ (𝑧 ⊆ 𝐼 → (∀𝑥 ∈ 𝐼 ∃𝑤 ∈ V 𝑤 ∈ 𝐶 → ∀𝑥 ∈ 𝑧 ∃𝑤 ∈ V 𝑤 ∈ 𝐶))
52	51	adantr 481	. . . . . . . . 9 ⊢ ((𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin) → (∀𝑥 ∈ 𝐼 ∃𝑤 ∈ V 𝑤 ∈ 𝐶 → ∀𝑥 ∈ 𝑧 ∃𝑤 ∈ V 𝑤 ∈ 𝐶))
53	50, 52	mpan9 507	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) → ∀𝑥 ∈ 𝑧 ∃𝑤 ∈ V 𝑤 ∈ 𝐶)
54		eleq1 2821	. . . . . . . . 9 ⊢ (𝑤 = (𝑓‘𝑥) → (𝑤 ∈ 𝐶 ↔ (𝑓‘𝑥) ∈ 𝐶))
55	54	ac6sfi 9283	. . . . . . . 8 ⊢ ((𝑧 ∈ Fin ∧ ∀𝑥 ∈ 𝑧 ∃𝑤 ∈ V 𝑤 ∈ 𝐶) → ∃𝑓(𝑓:𝑧⟶V ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶))
56	31, 53, 55	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) → ∃𝑓(𝑓:𝑧⟶V ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶))
57	23	eqcomd 2738	. . . . . . . . . . 11 ⊢ (𝜑 → ∪ (∏_t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) = X𝑥 ∈ 𝐼 ∪ 𝐽)
58	57	ineq1d 4210	. . . . . . . . . 10 ⊢ (𝜑 → (∪ (∏_t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∩ ∩ 𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) = (X𝑥 ∈ 𝐼 ∪ 𝐽 ∩ ∩ 𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
59	58	ad2antrr 724	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → (∪ (∏_t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∩ ∩ 𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) = (X𝑥 ∈ 𝐼 ∪ 𝐽 ∩ ∩ 𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
60		iftrue 4533	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ 𝑧 → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) = (𝑓‘𝑥))
61	60	ad2antrl 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ (𝑥 ∈ 𝑧 ∧ (𝑓‘𝑥) ∈ 𝐶)) → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) = (𝑓‘𝑥))
62		simpll 765	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ 𝑥 ∈ 𝑧) → 𝜑)
63		simprl 769	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) → 𝑧 ⊆ 𝐼)
64	63	sselda 3981	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ 𝑥 ∈ 𝑧) → 𝑥 ∈ 𝐼)
65	62, 64, 4	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ 𝑥 ∈ 𝑧) → 𝐶 ⊆ ∪ 𝐽)
66	65	sseld 3980	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ 𝑥 ∈ 𝑧) → ((𝑓‘𝑥) ∈ 𝐶 → (𝑓‘𝑥) ∈ ∪ 𝐽))
67	66	impr 455	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ (𝑥 ∈ 𝑧 ∧ (𝑓‘𝑥) ∈ 𝐶)) → (𝑓‘𝑥) ∈ ∪ 𝐽)
68	61, 67	eqeltrd 2833	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ (𝑥 ∈ 𝑧 ∧ (𝑓‘𝑥) ∈ 𝐶)) → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽)
69	68	expr 457	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ 𝑥 ∈ 𝑧) → ((𝑓‘𝑥) ∈ 𝐶 → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽))
70	69	ralimdva 3167	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) → (∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶 → ∀𝑥 ∈ 𝑧 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽))
71	70	imp 407	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → ∀𝑥 ∈ 𝑧 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽)
72		eldifn 4126	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (𝐼 ∖ 𝑧) → ¬ 𝑥 ∈ 𝑧)
73	72	iffalsed 4538	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝐼 ∖ 𝑧) → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) = 𝑈)
74	73	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) = 𝑈)
75		eldifi 4125	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝐼 ∖ 𝑧) → 𝑥 ∈ 𝐼)
76		kelac1.u	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑈 ∈ ∪ 𝐽)
77	75, 76	sylan2 593	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → 𝑈 ∈ ∪ 𝐽)
78	74, 77	eqeltrd 2833	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽)
79	78	ralrimiva 3146	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ∀𝑥 ∈ (𝐼 ∖ 𝑧)if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽)
80	79	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → ∀𝑥 ∈ (𝐼 ∖ 𝑧)if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽)
81		ralun 4191	. . . . . . . . . . . . . 14 ⊢ ((∀𝑥 ∈ 𝑧 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽 ∧ ∀𝑥 ∈ (𝐼 ∖ 𝑧)if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽) → ∀𝑥 ∈ (𝑧 ∪ (𝐼 ∖ 𝑧))if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽)
82	71, 80, 81	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → ∀𝑥 ∈ (𝑧 ∪ (𝐼 ∖ 𝑧))if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽)
83		undif 4480	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ⊆ 𝐼 ↔ (𝑧 ∪ (𝐼 ∖ 𝑧)) = 𝐼)
84	83	biimpi 215	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ⊆ 𝐼 → (𝑧 ∪ (𝐼 ∖ 𝑧)) = 𝐼)
85	84	ad2antrl 726	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) → (𝑧 ∪ (𝐼 ∖ 𝑧)) = 𝐼)
86	85	raleqdv 3325	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) → (∀𝑥 ∈ (𝑧 ∪ (𝐼 ∖ 𝑧))if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽 ↔ ∀𝑥 ∈ 𝐼 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽))
87	86	adantr 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → (∀𝑥 ∈ (𝑧 ∪ (𝐼 ∖ 𝑧))if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽 ↔ ∀𝑥 ∈ 𝐼 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽))
88	82, 87	mpbid 231	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → ∀𝑥 ∈ 𝐼 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ ∪ 𝐽)
89	19	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → 𝐼 ∈ V)
90		mptelixpg 8925	. . . . . . . . . . . . 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 2822	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐶 = if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) → ((𝑓‘𝑥) ∈ 𝐶 ↔ (𝑓‘𝑥) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
94		eleq2 2822	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∪ 𝐽 = if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) → ((𝑓‘𝑥) ∈ ∪ 𝐽 ↔ (𝑓‘𝑥) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
95		simplrr 776	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ (𝑥 ∈ 𝑧 ∧ (𝑓‘𝑥) ∈ 𝐶)) ∧ 𝑥 = 𝑦) → (𝑓‘𝑥) ∈ 𝐶)
96	67	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ (𝑥 ∈ 𝑧 ∧ (𝑓‘𝑥) ∈ 𝐶)) ∧ ¬ 𝑥 = 𝑦) → (𝑓‘𝑥) ∈ ∪ 𝐽)
97	93, 94, 95, 96	ifbothda 4565	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ (𝑥 ∈ 𝑧 ∧ (𝑓‘𝑥) ∈ 𝐶)) → (𝑓‘𝑥) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
98	61, 97	eqeltrd 2833	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ (𝑥 ∈ 𝑧 ∧ (𝑓‘𝑥) ∈ 𝐶)) → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
99	98	expr 457	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ 𝑥 ∈ 𝑧) → ((𝑓‘𝑥) ∈ 𝐶 → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
100	99	ralimdva 3167	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) → (∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶 → ∀𝑥 ∈ 𝑧 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
101	100	imp 407	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → ∀𝑥 ∈ 𝑧 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
102	101	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) ∧ 𝑦 ∈ 𝑧) → ∀𝑥 ∈ 𝑧 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
103	77	adantlr 713	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑧) ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → 𝑈 ∈ ∪ 𝐽)
104	73	adantl 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑧) ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) = 𝑈)
105		disjdifr 4471	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐼 ∖ 𝑧) ∩ 𝑧) = ∅
106	105	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑧) ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → ((𝐼 ∖ 𝑧) ∩ 𝑧) = ∅)
107		simpr 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑧) ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → 𝑥 ∈ (𝐼 ∖ 𝑧))
108		simplr 767	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑧) ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → 𝑦 ∈ 𝑧)
109		disjne 4453	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐼 ∖ 𝑧) ∩ 𝑧) = ∅ ∧ 𝑥 ∈ (𝐼 ∖ 𝑧) ∧ 𝑦 ∈ 𝑧) → 𝑥 ≠ 𝑦)
110	106, 107, 108, 109	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑧) ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → 𝑥 ≠ 𝑦)
111	110	neneqd 2945	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑧) ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → ¬ 𝑥 = 𝑦)
112	111	iffalsed 4538	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑧) ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) = ∪ 𝐽)
113	103, 104, 112	3eltr4d 2848	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑧) ∧ 𝑥 ∈ (𝐼 ∖ 𝑧)) → if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
114	113	ralrimiva 3146	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑧) → ∀𝑥 ∈ (𝐼 ∖ 𝑧)if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
115	114	adantlr 713	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ 𝑦 ∈ 𝑧) → ∀𝑥 ∈ (𝐼 ∖ 𝑧)if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
116	115	adantlr 713	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) ∧ 𝑦 ∈ 𝑧) → ∀𝑥 ∈ (𝐼 ∖ 𝑧)if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
117		ralun 4191	. . . . . . . . . . . . . . . 16 ⊢ ((∀𝑥 ∈ 𝑧 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) ∧ ∀𝑥 ∈ (𝐼 ∖ 𝑧)if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) → ∀𝑥 ∈ (𝑧 ∪ (𝐼 ∖ 𝑧))if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
118	102, 116, 117	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) ∧ 𝑦 ∈ 𝑧) → ∀𝑥 ∈ (𝑧 ∪ (𝐼 ∖ 𝑧))if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
119	85	raleqdv 3325	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) → (∀𝑥 ∈ (𝑧 ∪ (𝐼 ∖ 𝑧))if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) ↔ ∀𝑥 ∈ 𝐼 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
120	119	ad2antrr 724	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) ∧ 𝑦 ∈ 𝑧) → (∀𝑥 ∈ (𝑧 ∪ (𝐼 ∖ 𝑧))if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽) ↔ ∀𝑥 ∈ 𝐼 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
121	118, 120	mpbid 231	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) ∧ 𝑦 ∈ 𝑧) → ∀𝑥 ∈ 𝐼 if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈) ∈ if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
122	19	ad3antrrr 728	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) ∧ 𝑦 ∈ 𝑧) → 𝐼 ∈ V)
123		mptelixpg 8925	. . . . . . . . . . . . . . 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 3146	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → ∀𝑦 ∈ 𝑧 (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽))
127		mptexg 7219	. . . . . . . . . . . . . . 15 ⊢ (𝐼 ∈ V → (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ V)
128	19, 127	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ V)
129	128	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ V)
130		eliin 5001	. . . . . . . . . . . . 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 4193	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝑧, (𝑓‘𝑥), 𝑈)) ∈ (X𝑥 ∈ 𝐼 ∪ 𝐽 ∩ ∩ 𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)))
134	133	ne0d 4334	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → (X𝑥 ∈ 𝐼 ∪ 𝐽 ∩ ∩ 𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) ≠ ∅)
135	59, 134	eqnetrd 3008	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶) → (∪ (∏_t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∩ ∩ 𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) ≠ ∅)
136	135	adantrl 714	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) ∧ (𝑓:𝑧⟶V ∧ ∀𝑥 ∈ 𝑧 (𝑓‘𝑥) ∈ 𝐶)) → (∪ (∏_t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∩ ∩ 𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) ≠ ∅)
137	56, 136	exlimddv 1938	. . . . . 6 ⊢ ((𝜑 ∧ (𝑧 ⊆ 𝐼 ∧ 𝑧 ∈ Fin)) → (∪ (∏_t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∩ ∩ 𝑦 ∈ 𝑧 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) ≠ ∅)
138	25, 8, 30, 137	cmpfiiin 41420	. . . . 5 ⊢ (𝜑 → (∪ (∏_t‘(𝑥 ∈ 𝐼 ↦ 𝐽)) ∩ ∩ 𝑦 ∈ 𝐼 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) ≠ ∅)
139	24, 138	eqnetrd 3008	. . . 4 ⊢ (𝜑 → (X𝑥 ∈ 𝐼 ∪ 𝐽 ∩ ∩ 𝑦 ∈ 𝐼 X𝑥 ∈ 𝐼 if(𝑥 = 𝑦, 𝐶, ∪ 𝐽)) ≠ ∅)
140	7, 139	eqnetrd 3008	. . 3 ⊢ (𝜑 → X𝑥 ∈ 𝐼 𝐶 ≠ ∅)
141		n0 4345	. . 3 ⊢ (X𝑥 ∈ 𝐼 𝐶 ≠ ∅ ↔ ∃𝑦 𝑦 ∈ X𝑥 ∈ 𝐼 𝐶)
142	140, 141	sylib 217	. 2 ⊢ (𝜑 → ∃𝑦 𝑦 ∈ X𝑥 ∈ 𝐼 𝐶)
143		elixp2 8891	. . . . . 6 ⊢ (𝑦 ∈ X𝑥 ∈ 𝐼 𝐶 ↔ (𝑦 ∈ V ∧ 𝑦 Fn 𝐼 ∧ ∀𝑥 ∈ 𝐼 (𝑦‘𝑥) ∈ 𝐶))
144	143	simp3bi 1147	. . . . 5 ⊢ (𝑦 ∈ X𝑥 ∈ 𝐼 𝐶 → ∀𝑥 ∈ 𝐼 (𝑦‘𝑥) ∈ 𝐶)
145		f1ocnv 6842	. . . . . . . 8 ⊢ (𝐵:𝑆–1-1-onto→𝐶 → ^◡𝐵:𝐶–1-1-onto→𝑆)
146		f1of 6830	. . . . . . . 8 ⊢ (^◡𝐵:𝐶–1-1-onto→𝑆 → ^◡𝐵:𝐶⟶𝑆)
147		ffvelcdm 7080	. . . . . . . . 9 ⊢ ((^◡𝐵:𝐶⟶𝑆 ∧ (𝑦‘𝑥) ∈ 𝐶) → (^◡𝐵‘(𝑦‘𝑥)) ∈ 𝑆)
148	147	ex 413	. . . . . . . 8 ⊢ (^◡𝐵:𝐶⟶𝑆 → ((𝑦‘𝑥) ∈ 𝐶 → (^◡𝐵‘(𝑦‘𝑥)) ∈ 𝑆))
149	32, 145, 146, 148	4syl 19	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → ((𝑦‘𝑥) ∈ 𝐶 → (^◡𝐵‘(𝑦‘𝑥)) ∈ 𝑆))
150	149	ralimdva 3167	. . . . . 6 ⊢ (𝜑 → (∀𝑥 ∈ 𝐼 (𝑦‘𝑥) ∈ 𝐶 → ∀𝑥 ∈ 𝐼 (^◡𝐵‘(𝑦‘𝑥)) ∈ 𝑆))
151	150	imp 407	. . . . 5 ⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐼 (𝑦‘𝑥) ∈ 𝐶) → ∀𝑥 ∈ 𝐼 (^◡𝐵‘(𝑦‘𝑥)) ∈ 𝑆)
152	144, 151	sylan2 593	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ X𝑥 ∈ 𝐼 𝐶) → ∀𝑥 ∈ 𝐼 (^◡𝐵‘(𝑦‘𝑥)) ∈ 𝑆)
153		mptelixpg 8925	. . . . . 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 4334	. 2 ⊢ ((𝜑 ∧ 𝑦 ∈ X𝑥 ∈ 𝐼 𝐶) → X𝑥 ∈ 𝐼 𝑆 ≠ ∅)
158	142, 157	exlimddv 1938	1 ⊢ (𝜑 → X𝑥 ∈ 𝐼 𝑆 ≠ ∅)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1541 ∃wex 1781 ∈ wcel 2106 ≠ wne 2940 ∀wral 3061 ∃wrex 3070 Vcvv 3474 ∖ cdif 3944 ∪ cun 3945 ∩ cin 3946 ⊆ wss 3947 ∅c0 4321 ifcif 4527 ∪ cuni 4907 ∩ ciin 4997 ↦ cmpt 5230 ^◡ccnv 5674 “ cima 5678 Fn wfn 6535 ⟶wf 6536 –onto→wfo 6538 –1-1-onto→wf1o 6539 ‘cfv 6540 Xcixp 8887 Fincfn 8935 ∏_tcpt 17380 Topctop 22386 Clsdccld 22511 Compccmp 22881

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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-rep 5284 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7721

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-ral 3062 df-rex 3071 df-reu 3377 df-rab 3433 df-v 3476 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-int 4950 df-iun 4998 df-iin 4999 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5573 df-eprel 5579 df-po 5587 df-so 5588 df-fr 5630 df-we 5632 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6492 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-om 7852 df-1o 8462 df-er 8699 df-ixp 8888 df-en 8936 df-fin 8939 df-fi 9402 df-topgen 17385 df-pt 17386 df-top 22387 df-bases 22440 df-cld 22514 df-cmp 22882

This theorem is referenced by: kelac2 41792

W3C validator