ptbasin - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ptbasin		Structured version Visualization version GIF version

Theorem ptbasin 22185

Description: The basis for a product topology is closed under intersections. (Contributed by Mario Carneiro, 3-Feb-2015.)

**Hypothesis**
Ref	Expression
ptbas.1	⊢ 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))}

**Assertion**
Ref	Expression
ptbasin	⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 ∩ 𝑌) ∈ 𝐵)

Distinct variable groups: 𝑥,𝑔,𝑦,𝑧,𝐴 𝑔,𝑌,𝑥 𝑔,𝐹,𝑥,𝑦,𝑧 𝑔,𝑋,𝑥,𝑧 𝑔,𝑉,𝑥,𝑦,𝑧 Allowed substitution hints: 𝐵(𝑥,𝑦,𝑧,𝑔) 𝑋(𝑦) 𝑌(𝑦,𝑧)

Proof of Theorem ptbasin Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑘 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ptbas.1	. . . . . 6 ⊢ 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))}
2	1	elpt 22180	. . . . 5 ⊢ (𝑋 ∈ 𝐵 ↔ ∃𝑎((𝑎 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑎‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑐 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑐)(𝑎‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑋 = X𝑦 ∈ 𝐴 (𝑎‘𝑦)))
3	1	elpt 22180	. . . . 5 ⊢ (𝑌 ∈ 𝐵 ↔ ∃𝑏((𝑏 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑏‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑑 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑑)(𝑏‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑌 = X𝑦 ∈ 𝐴 (𝑏‘𝑦)))
4	2, 3	anbi12i 628	. . . 4 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ↔ (∃𝑎((𝑎 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑎‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑐 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑐)(𝑎‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑋 = X𝑦 ∈ 𝐴 (𝑎‘𝑦)) ∧ ∃𝑏((𝑏 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑏‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑑 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑑)(𝑏‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑌 = X𝑦 ∈ 𝐴 (𝑏‘𝑦))))
5		exdistrv 1956	. . . 4 ⊢ (∃𝑎∃𝑏(((𝑎 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑎‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑐 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑐)(𝑎‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑋 = X𝑦 ∈ 𝐴 (𝑎‘𝑦)) ∧ ((𝑏 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑏‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑑 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑑)(𝑏‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑌 = X𝑦 ∈ 𝐴 (𝑏‘𝑦))) ↔ (∃𝑎((𝑎 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑎‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑐 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑐)(𝑎‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑋 = X𝑦 ∈ 𝐴 (𝑎‘𝑦)) ∧ ∃𝑏((𝑏 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑏‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑑 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑑)(𝑏‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑌 = X𝑦 ∈ 𝐴 (𝑏‘𝑦))))
6	4, 5	bitr4i 280	. . 3 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ↔ ∃𝑎∃𝑏(((𝑎 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑎‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑐 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑐)(𝑎‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑋 = X𝑦 ∈ 𝐴 (𝑎‘𝑦)) ∧ ((𝑏 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑏‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑑 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑑)(𝑏‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑌 = X𝑦 ∈ 𝐴 (𝑏‘𝑦))))
7		an4 654	. . . . 5 ⊢ ((((𝑎 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑎‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑐 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑐)(𝑎‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑋 = X𝑦 ∈ 𝐴 (𝑎‘𝑦)) ∧ ((𝑏 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑏‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑑 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑑)(𝑏‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑌 = X𝑦 ∈ 𝐴 (𝑏‘𝑦))) ↔ (((𝑎 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑎‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑐 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑐)(𝑎‘𝑦) = ∪ (𝐹‘𝑦)) ∧ (𝑏 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑏‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑑 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑑)(𝑏‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝑋 = X𝑦 ∈ 𝐴 (𝑎‘𝑦) ∧ 𝑌 = X𝑦 ∈ 𝐴 (𝑏‘𝑦))))
8		an6 1441	. . . . . . . . 9 ⊢ (((𝑎 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑎‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑐 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑐)(𝑎‘𝑦) = ∪ (𝐹‘𝑦)) ∧ (𝑏 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑏‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑑 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑑)(𝑏‘𝑦) = ∪ (𝐹‘𝑦))) ↔ ((𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴) ∧ (∀𝑦 ∈ 𝐴 (𝑎‘𝑦) ∈ (𝐹‘𝑦) ∧ ∀𝑦 ∈ 𝐴 (𝑏‘𝑦) ∈ (𝐹‘𝑦)) ∧ (∃𝑐 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑐)(𝑎‘𝑦) = ∪ (𝐹‘𝑦) ∧ ∃𝑑 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑑)(𝑏‘𝑦) = ∪ (𝐹‘𝑦))))
9		df-3an 1085	. . . . . . . . 9 ⊢ (((𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴) ∧ (∀𝑦 ∈ 𝐴 (𝑎‘𝑦) ∈ (𝐹‘𝑦) ∧ ∀𝑦 ∈ 𝐴 (𝑏‘𝑦) ∈ (𝐹‘𝑦)) ∧ (∃𝑐 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑐)(𝑎‘𝑦) = ∪ (𝐹‘𝑦) ∧ ∃𝑑 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑑)(𝑏‘𝑦) = ∪ (𝐹‘𝑦))) ↔ (((𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴) ∧ (∀𝑦 ∈ 𝐴 (𝑎‘𝑦) ∈ (𝐹‘𝑦) ∧ ∀𝑦 ∈ 𝐴 (𝑏‘𝑦) ∈ (𝐹‘𝑦))) ∧ (∃𝑐 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑐)(𝑎‘𝑦) = ∪ (𝐹‘𝑦) ∧ ∃𝑑 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑑)(𝑏‘𝑦) = ∪ (𝐹‘𝑦))))
10	8, 9	bitri 277	. . . . . . . 8 ⊢ (((𝑎 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑎‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑐 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑐)(𝑎‘𝑦) = ∪ (𝐹‘𝑦)) ∧ (𝑏 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑏‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑑 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑑)(𝑏‘𝑦) = ∪ (𝐹‘𝑦))) ↔ (((𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴) ∧ (∀𝑦 ∈ 𝐴 (𝑎‘𝑦) ∈ (𝐹‘𝑦) ∧ ∀𝑦 ∈ 𝐴 (𝑏‘𝑦) ∈ (𝐹‘𝑦))) ∧ (∃𝑐 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑐)(𝑎‘𝑦) = ∪ (𝐹‘𝑦) ∧ ∃𝑑 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑑)(𝑏‘𝑦) = ∪ (𝐹‘𝑦))))
11		reeanv 3367	. . . . . . . . . . 11 ⊢ (∃𝑐 ∈ Fin ∃𝑑 ∈ Fin (∀𝑦 ∈ (𝐴 ∖ 𝑐)(𝑎‘𝑦) = ∪ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑑)(𝑏‘𝑦) = ∪ (𝐹‘𝑦)) ↔ (∃𝑐 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑐)(𝑎‘𝑦) = ∪ (𝐹‘𝑦) ∧ ∃𝑑 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑑)(𝑏‘𝑦) = ∪ (𝐹‘𝑦)))
12		fveq2 6670	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑘 → (𝑎‘𝑦) = (𝑎‘𝑘))
13		fveq2 6670	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 = 𝑘 → (𝑏‘𝑦) = (𝑏‘𝑘))
14	12, 13	ineq12d 4190	. . . . . . . . . . . . . . 15 ⊢ (𝑦 = 𝑘 → ((𝑎‘𝑦) ∩ (𝑏‘𝑦)) = ((𝑎‘𝑘) ∩ (𝑏‘𝑘)))
15	14	cbvixpv 8479	. . . . . . . . . . . . . 14 ⊢ X𝑦 ∈ 𝐴 ((𝑎‘𝑦) ∩ (𝑏‘𝑦)) = X𝑘 ∈ 𝐴 ((𝑎‘𝑘) ∩ (𝑏‘𝑘))
16		simpl1l 1220	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴) ∧ (∀𝑦 ∈ 𝐴 (𝑎‘𝑦) ∈ (𝐹‘𝑦) ∧ ∀𝑦 ∈ 𝐴 (𝑏‘𝑦) ∈ (𝐹‘𝑦))) ∧ ((𝑐 ∈ Fin ∧ 𝑑 ∈ Fin) ∧ (∀𝑦 ∈ (𝐴 ∖ 𝑐)(𝑎‘𝑦) = ∪ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑑)(𝑏‘𝑦) = ∪ (𝐹‘𝑦)))) → 𝐴 ∈ 𝑉)
17		unfi 8785	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 ∈ Fin ∧ 𝑑 ∈ Fin) → (𝑐 ∪ 𝑑) ∈ Fin)
18	17	ad2antrl 726	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴) ∧ (∀𝑦 ∈ 𝐴 (𝑎‘𝑦) ∈ (𝐹‘𝑦) ∧ ∀𝑦 ∈ 𝐴 (𝑏‘𝑦) ∈ (𝐹‘𝑦))) ∧ ((𝑐 ∈ Fin ∧ 𝑑 ∈ Fin) ∧ (∀𝑦 ∈ (𝐴 ∖ 𝑐)(𝑎‘𝑦) = ∪ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑑)(𝑏‘𝑦) = ∪ (𝐹‘𝑦)))) → (𝑐 ∪ 𝑑) ∈ Fin)
19		simpl1r 1221	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴) ∧ (∀𝑦 ∈ 𝐴 (𝑎‘𝑦) ∈ (𝐹‘𝑦) ∧ ∀𝑦 ∈ 𝐴 (𝑏‘𝑦) ∈ (𝐹‘𝑦))) ∧ ((𝑐 ∈ Fin ∧ 𝑑 ∈ Fin) ∧ (∀𝑦 ∈ (𝐴 ∖ 𝑐)(𝑎‘𝑦) = ∪ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑑)(𝑏‘𝑦) = ∪ (𝐹‘𝑦)))) → 𝐹:𝐴⟶Top)
20	19	ffvelrnda 6851	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴) ∧ (∀𝑦 ∈ 𝐴 (𝑎‘𝑦) ∈ (𝐹‘𝑦) ∧ ∀𝑦 ∈ 𝐴 (𝑏‘𝑦) ∈ (𝐹‘𝑦))) ∧ ((𝑐 ∈ Fin ∧ 𝑑 ∈ Fin) ∧ (∀𝑦 ∈ (𝐴 ∖ 𝑐)(𝑎‘𝑦) = ∪ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑑)(𝑏‘𝑦) = ∪ (𝐹‘𝑦)))) ∧ 𝑘 ∈ 𝐴) → (𝐹‘𝑘) ∈ Top)
21		simpl3l 1224	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴) ∧ (∀𝑦 ∈ 𝐴 (𝑎‘𝑦) ∈ (𝐹‘𝑦) ∧ ∀𝑦 ∈ 𝐴 (𝑏‘𝑦) ∈ (𝐹‘𝑦))) ∧ ((𝑐 ∈ Fin ∧ 𝑑 ∈ Fin) ∧ (∀𝑦 ∈ (𝐴 ∖ 𝑐)(𝑎‘𝑦) = ∪ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑑)(𝑏‘𝑦) = ∪ (𝐹‘𝑦)))) → ∀𝑦 ∈ 𝐴 (𝑎‘𝑦) ∈ (𝐹‘𝑦))
22		fveq2 6670	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑘 → (𝐹‘𝑦) = (𝐹‘𝑘))
23	12, 22	eleq12d 2907	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑘 → ((𝑎‘𝑦) ∈ (𝐹‘𝑦) ↔ (𝑎‘𝑘) ∈ (𝐹‘𝑘)))
24	23	rspccva 3622	. . . . . . . . . . . . . . . . 17 ⊢ ((∀𝑦 ∈ 𝐴 (𝑎‘𝑦) ∈ (𝐹‘𝑦) ∧ 𝑘 ∈ 𝐴) → (𝑎‘𝑘) ∈ (𝐹‘𝑘))
25	21, 24	sylan 582	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴) ∧ (∀𝑦 ∈ 𝐴 (𝑎‘𝑦) ∈ (𝐹‘𝑦) ∧ ∀𝑦 ∈ 𝐴 (𝑏‘𝑦) ∈ (𝐹‘𝑦))) ∧ ((𝑐 ∈ Fin ∧ 𝑑 ∈ Fin) ∧ (∀𝑦 ∈ (𝐴 ∖ 𝑐)(𝑎‘𝑦) = ∪ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑑)(𝑏‘𝑦) = ∪ (𝐹‘𝑦)))) ∧ 𝑘 ∈ 𝐴) → (𝑎‘𝑘) ∈ (𝐹‘𝑘))
26		simpl3r 1225	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴) ∧ (∀𝑦 ∈ 𝐴 (𝑎‘𝑦) ∈ (𝐹‘𝑦) ∧ ∀𝑦 ∈ 𝐴 (𝑏‘𝑦) ∈ (𝐹‘𝑦))) ∧ ((𝑐 ∈ Fin ∧ 𝑑 ∈ Fin) ∧ (∀𝑦 ∈ (𝐴 ∖ 𝑐)(𝑎‘𝑦) = ∪ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑑)(𝑏‘𝑦) = ∪ (𝐹‘𝑦)))) → ∀𝑦 ∈ 𝐴 (𝑏‘𝑦) ∈ (𝐹‘𝑦))
27	13, 22	eleq12d 2907	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑘 → ((𝑏‘𝑦) ∈ (𝐹‘𝑦) ↔ (𝑏‘𝑘) ∈ (𝐹‘𝑘)))
28	27	rspccva 3622	. . . . . . . . . . . . . . . . 17 ⊢ ((∀𝑦 ∈ 𝐴 (𝑏‘𝑦) ∈ (𝐹‘𝑦) ∧ 𝑘 ∈ 𝐴) → (𝑏‘𝑘) ∈ (𝐹‘𝑘))
29	26, 28	sylan 582	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴) ∧ (∀𝑦 ∈ 𝐴 (𝑎‘𝑦) ∈ (𝐹‘𝑦) ∧ ∀𝑦 ∈ 𝐴 (𝑏‘𝑦) ∈ (𝐹‘𝑦))) ∧ ((𝑐 ∈ Fin ∧ 𝑑 ∈ Fin) ∧ (∀𝑦 ∈ (𝐴 ∖ 𝑐)(𝑎‘𝑦) = ∪ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑑)(𝑏‘𝑦) = ∪ (𝐹‘𝑦)))) ∧ 𝑘 ∈ 𝐴) → (𝑏‘𝑘) ∈ (𝐹‘𝑘))
30		inopn 21507	. . . . . . . . . . . . . . . 16 ⊢ (((𝐹‘𝑘) ∈ Top ∧ (𝑎‘𝑘) ∈ (𝐹‘𝑘) ∧ (𝑏‘𝑘) ∈ (𝐹‘𝑘)) → ((𝑎‘𝑘) ∩ (𝑏‘𝑘)) ∈ (𝐹‘𝑘))
31	20, 25, 29, 30	syl3anc 1367	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴) ∧ (∀𝑦 ∈ 𝐴 (𝑎‘𝑦) ∈ (𝐹‘𝑦) ∧ ∀𝑦 ∈ 𝐴 (𝑏‘𝑦) ∈ (𝐹‘𝑦))) ∧ ((𝑐 ∈ Fin ∧ 𝑑 ∈ Fin) ∧ (∀𝑦 ∈ (𝐴 ∖ 𝑐)(𝑎‘𝑦) = ∪ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑑)(𝑏‘𝑦) = ∪ (𝐹‘𝑦)))) ∧ 𝑘 ∈ 𝐴) → ((𝑎‘𝑘) ∩ (𝑏‘𝑘)) ∈ (𝐹‘𝑘))
32		simprrl 779	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴) ∧ (∀𝑦 ∈ 𝐴 (𝑎‘𝑦) ∈ (𝐹‘𝑦) ∧ ∀𝑦 ∈ 𝐴 (𝑏‘𝑦) ∈ (𝐹‘𝑦))) ∧ ((𝑐 ∈ Fin ∧ 𝑑 ∈ Fin) ∧ (∀𝑦 ∈ (𝐴 ∖ 𝑐)(𝑎‘𝑦) = ∪ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑑)(𝑏‘𝑦) = ∪ (𝐹‘𝑦)))) → ∀𝑦 ∈ (𝐴 ∖ 𝑐)(𝑎‘𝑦) = ∪ (𝐹‘𝑦))
33		ssun1 4148	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑐 ⊆ (𝑐 ∪ 𝑑)
34		sscon 4115	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 ⊆ (𝑐 ∪ 𝑑) → (𝐴 ∖ (𝑐 ∪ 𝑑)) ⊆ (𝐴 ∖ 𝑐))
35	33, 34	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∖ (𝑐 ∪ 𝑑)) ⊆ (𝐴 ∖ 𝑐)
36	35	sseli 3963	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (𝐴 ∖ (𝑐 ∪ 𝑑)) → 𝑘 ∈ (𝐴 ∖ 𝑐))
37	22	unieqd 4852	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = 𝑘 → ∪ (𝐹‘𝑦) = ∪ (𝐹‘𝑘))
38	12, 37	eqeq12d 2837	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑘 → ((𝑎‘𝑦) = ∪ (𝐹‘𝑦) ↔ (𝑎‘𝑘) = ∪ (𝐹‘𝑘)))
39	38	rspccva 3622	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑦 ∈ (𝐴 ∖ 𝑐)(𝑎‘𝑦) = ∪ (𝐹‘𝑦) ∧ 𝑘 ∈ (𝐴 ∖ 𝑐)) → (𝑎‘𝑘) = ∪ (𝐹‘𝑘))
40	32, 36, 39	syl2an 597	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴) ∧ (∀𝑦 ∈ 𝐴 (𝑎‘𝑦) ∈ (𝐹‘𝑦) ∧ ∀𝑦 ∈ 𝐴 (𝑏‘𝑦) ∈ (𝐹‘𝑦))) ∧ ((𝑐 ∈ Fin ∧ 𝑑 ∈ Fin) ∧ (∀𝑦 ∈ (𝐴 ∖ 𝑐)(𝑎‘𝑦) = ∪ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑑)(𝑏‘𝑦) = ∪ (𝐹‘𝑦)))) ∧ 𝑘 ∈ (𝐴 ∖ (𝑐 ∪ 𝑑))) → (𝑎‘𝑘) = ∪ (𝐹‘𝑘))
41		simprrr 780	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴) ∧ (∀𝑦 ∈ 𝐴 (𝑎‘𝑦) ∈ (𝐹‘𝑦) ∧ ∀𝑦 ∈ 𝐴 (𝑏‘𝑦) ∈ (𝐹‘𝑦))) ∧ ((𝑐 ∈ Fin ∧ 𝑑 ∈ Fin) ∧ (∀𝑦 ∈ (𝐴 ∖ 𝑐)(𝑎‘𝑦) = ∪ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑑)(𝑏‘𝑦) = ∪ (𝐹‘𝑦)))) → ∀𝑦 ∈ (𝐴 ∖ 𝑑)(𝑏‘𝑦) = ∪ (𝐹‘𝑦))
42		ssun2 4149	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑑 ⊆ (𝑐 ∪ 𝑑)
43		sscon 4115	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 ⊆ (𝑐 ∪ 𝑑) → (𝐴 ∖ (𝑐 ∪ 𝑑)) ⊆ (𝐴 ∖ 𝑑))
44	42, 43	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∖ (𝑐 ∪ 𝑑)) ⊆ (𝐴 ∖ 𝑑)
45	44	sseli 3963	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ (𝐴 ∖ (𝑐 ∪ 𝑑)) → 𝑘 ∈ (𝐴 ∖ 𝑑))
46	13, 37	eqeq12d 2837	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑘 → ((𝑏‘𝑦) = ∪ (𝐹‘𝑦) ↔ (𝑏‘𝑘) = ∪ (𝐹‘𝑘)))
47	46	rspccva 3622	. . . . . . . . . . . . . . . . . 18 ⊢ ((∀𝑦 ∈ (𝐴 ∖ 𝑑)(𝑏‘𝑦) = ∪ (𝐹‘𝑦) ∧ 𝑘 ∈ (𝐴 ∖ 𝑑)) → (𝑏‘𝑘) = ∪ (𝐹‘𝑘))
48	41, 45, 47	syl2an 597	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴) ∧ (∀𝑦 ∈ 𝐴 (𝑎‘𝑦) ∈ (𝐹‘𝑦) ∧ ∀𝑦 ∈ 𝐴 (𝑏‘𝑦) ∈ (𝐹‘𝑦))) ∧ ((𝑐 ∈ Fin ∧ 𝑑 ∈ Fin) ∧ (∀𝑦 ∈ (𝐴 ∖ 𝑐)(𝑎‘𝑦) = ∪ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑑)(𝑏‘𝑦) = ∪ (𝐹‘𝑦)))) ∧ 𝑘 ∈ (𝐴 ∖ (𝑐 ∪ 𝑑))) → (𝑏‘𝑘) = ∪ (𝐹‘𝑘))
49	40, 48	ineq12d 4190	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴) ∧ (∀𝑦 ∈ 𝐴 (𝑎‘𝑦) ∈ (𝐹‘𝑦) ∧ ∀𝑦 ∈ 𝐴 (𝑏‘𝑦) ∈ (𝐹‘𝑦))) ∧ ((𝑐 ∈ Fin ∧ 𝑑 ∈ Fin) ∧ (∀𝑦 ∈ (𝐴 ∖ 𝑐)(𝑎‘𝑦) = ∪ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑑)(𝑏‘𝑦) = ∪ (𝐹‘𝑦)))) ∧ 𝑘 ∈ (𝐴 ∖ (𝑐 ∪ 𝑑))) → ((𝑎‘𝑘) ∩ (𝑏‘𝑘)) = (∪ (𝐹‘𝑘) ∩ ∪ (𝐹‘𝑘)))
50		inidm 4195	. . . . . . . . . . . . . . . 16 ⊢ (∪ (𝐹‘𝑘) ∩ ∪ (𝐹‘𝑘)) = ∪ (𝐹‘𝑘)
51	49, 50	syl6eq 2872	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴) ∧ (∀𝑦 ∈ 𝐴 (𝑎‘𝑦) ∈ (𝐹‘𝑦) ∧ ∀𝑦 ∈ 𝐴 (𝑏‘𝑦) ∈ (𝐹‘𝑦))) ∧ ((𝑐 ∈ Fin ∧ 𝑑 ∈ Fin) ∧ (∀𝑦 ∈ (𝐴 ∖ 𝑐)(𝑎‘𝑦) = ∪ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑑)(𝑏‘𝑦) = ∪ (𝐹‘𝑦)))) ∧ 𝑘 ∈ (𝐴 ∖ (𝑐 ∪ 𝑑))) → ((𝑎‘𝑘) ∩ (𝑏‘𝑘)) = ∪ (𝐹‘𝑘))
52	1, 16, 18, 31, 51	elptr2 22182	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴) ∧ (∀𝑦 ∈ 𝐴 (𝑎‘𝑦) ∈ (𝐹‘𝑦) ∧ ∀𝑦 ∈ 𝐴 (𝑏‘𝑦) ∈ (𝐹‘𝑦))) ∧ ((𝑐 ∈ Fin ∧ 𝑑 ∈ Fin) ∧ (∀𝑦 ∈ (𝐴 ∖ 𝑐)(𝑎‘𝑦) = ∪ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑑)(𝑏‘𝑦) = ∪ (𝐹‘𝑦)))) → X𝑘 ∈ 𝐴 ((𝑎‘𝑘) ∩ (𝑏‘𝑘)) ∈ 𝐵)
53	15, 52	eqeltrid 2917	. . . . . . . . . . . . 13 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴) ∧ (∀𝑦 ∈ 𝐴 (𝑎‘𝑦) ∈ (𝐹‘𝑦) ∧ ∀𝑦 ∈ 𝐴 (𝑏‘𝑦) ∈ (𝐹‘𝑦))) ∧ ((𝑐 ∈ Fin ∧ 𝑑 ∈ Fin) ∧ (∀𝑦 ∈ (𝐴 ∖ 𝑐)(𝑎‘𝑦) = ∪ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑑)(𝑏‘𝑦) = ∪ (𝐹‘𝑦)))) → X𝑦 ∈ 𝐴 ((𝑎‘𝑦) ∩ (𝑏‘𝑦)) ∈ 𝐵)
54	53	expr 459	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴) ∧ (∀𝑦 ∈ 𝐴 (𝑎‘𝑦) ∈ (𝐹‘𝑦) ∧ ∀𝑦 ∈ 𝐴 (𝑏‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑐 ∈ Fin ∧ 𝑑 ∈ Fin)) → ((∀𝑦 ∈ (𝐴 ∖ 𝑐)(𝑎‘𝑦) = ∪ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑑)(𝑏‘𝑦) = ∪ (𝐹‘𝑦)) → X𝑦 ∈ 𝐴 ((𝑎‘𝑦) ∩ (𝑏‘𝑦)) ∈ 𝐵))
55	54	rexlimdvva 3294	. . . . . . . . . . 11 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴) ∧ (∀𝑦 ∈ 𝐴 (𝑎‘𝑦) ∈ (𝐹‘𝑦) ∧ ∀𝑦 ∈ 𝐴 (𝑏‘𝑦) ∈ (𝐹‘𝑦))) → (∃𝑐 ∈ Fin ∃𝑑 ∈ Fin (∀𝑦 ∈ (𝐴 ∖ 𝑐)(𝑎‘𝑦) = ∪ (𝐹‘𝑦) ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑑)(𝑏‘𝑦) = ∪ (𝐹‘𝑦)) → X𝑦 ∈ 𝐴 ((𝑎‘𝑦) ∩ (𝑏‘𝑦)) ∈ 𝐵))
56	11, 55	syl5bir 245	. . . . . . . . . 10 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴) ∧ (∀𝑦 ∈ 𝐴 (𝑎‘𝑦) ∈ (𝐹‘𝑦) ∧ ∀𝑦 ∈ 𝐴 (𝑏‘𝑦) ∈ (𝐹‘𝑦))) → ((∃𝑐 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑐)(𝑎‘𝑦) = ∪ (𝐹‘𝑦) ∧ ∃𝑑 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑑)(𝑏‘𝑦) = ∪ (𝐹‘𝑦)) → X𝑦 ∈ 𝐴 ((𝑎‘𝑦) ∩ (𝑏‘𝑦)) ∈ 𝐵))
57	56	3expb 1116	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ ((𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴) ∧ (∀𝑦 ∈ 𝐴 (𝑎‘𝑦) ∈ (𝐹‘𝑦) ∧ ∀𝑦 ∈ 𝐴 (𝑏‘𝑦) ∈ (𝐹‘𝑦)))) → ((∃𝑐 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑐)(𝑎‘𝑦) = ∪ (𝐹‘𝑦) ∧ ∃𝑑 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑑)(𝑏‘𝑦) = ∪ (𝐹‘𝑦)) → X𝑦 ∈ 𝐴 ((𝑎‘𝑦) ∩ (𝑏‘𝑦)) ∈ 𝐵))
58	57	impr 457	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (((𝑎 Fn 𝐴 ∧ 𝑏 Fn 𝐴) ∧ (∀𝑦 ∈ 𝐴 (𝑎‘𝑦) ∈ (𝐹‘𝑦) ∧ ∀𝑦 ∈ 𝐴 (𝑏‘𝑦) ∈ (𝐹‘𝑦))) ∧ (∃𝑐 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑐)(𝑎‘𝑦) = ∪ (𝐹‘𝑦) ∧ ∃𝑑 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑑)(𝑏‘𝑦) = ∪ (𝐹‘𝑦)))) → X𝑦 ∈ 𝐴 ((𝑎‘𝑦) ∩ (𝑏‘𝑦)) ∈ 𝐵)
59	10, 58	sylan2b 595	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ ((𝑎 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑎‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑐 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑐)(𝑎‘𝑦) = ∪ (𝐹‘𝑦)) ∧ (𝑏 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑏‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑑 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑑)(𝑏‘𝑦) = ∪ (𝐹‘𝑦)))) → X𝑦 ∈ 𝐴 ((𝑎‘𝑦) ∩ (𝑏‘𝑦)) ∈ 𝐵)
60		ineq12 4184	. . . . . . . . 9 ⊢ ((𝑋 = X𝑦 ∈ 𝐴 (𝑎‘𝑦) ∧ 𝑌 = X𝑦 ∈ 𝐴 (𝑏‘𝑦)) → (𝑋 ∩ 𝑌) = (X𝑦 ∈ 𝐴 (𝑎‘𝑦) ∩ X𝑦 ∈ 𝐴 (𝑏‘𝑦)))
61		ixpin 8487	. . . . . . . . 9 ⊢ X𝑦 ∈ 𝐴 ((𝑎‘𝑦) ∩ (𝑏‘𝑦)) = (X𝑦 ∈ 𝐴 (𝑎‘𝑦) ∩ X𝑦 ∈ 𝐴 (𝑏‘𝑦))
62	60, 61	syl6eqr 2874	. . . . . . . 8 ⊢ ((𝑋 = X𝑦 ∈ 𝐴 (𝑎‘𝑦) ∧ 𝑌 = X𝑦 ∈ 𝐴 (𝑏‘𝑦)) → (𝑋 ∩ 𝑌) = X𝑦 ∈ 𝐴 ((𝑎‘𝑦) ∩ (𝑏‘𝑦)))
63	62	eleq1d 2897	. . . . . . 7 ⊢ ((𝑋 = X𝑦 ∈ 𝐴 (𝑎‘𝑦) ∧ 𝑌 = X𝑦 ∈ 𝐴 (𝑏‘𝑦)) → ((𝑋 ∩ 𝑌) ∈ 𝐵 ↔ X𝑦 ∈ 𝐴 ((𝑎‘𝑦) ∩ (𝑏‘𝑦)) ∈ 𝐵))
64	59, 63	syl5ibrcom 249	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ ((𝑎 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑎‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑐 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑐)(𝑎‘𝑦) = ∪ (𝐹‘𝑦)) ∧ (𝑏 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑏‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑑 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑑)(𝑏‘𝑦) = ∪ (𝐹‘𝑦)))) → ((𝑋 = X𝑦 ∈ 𝐴 (𝑎‘𝑦) ∧ 𝑌 = X𝑦 ∈ 𝐴 (𝑏‘𝑦)) → (𝑋 ∩ 𝑌) ∈ 𝐵))
65	64	expimpd 456	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ((((𝑎 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑎‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑐 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑐)(𝑎‘𝑦) = ∪ (𝐹‘𝑦)) ∧ (𝑏 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑏‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑑 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑑)(𝑏‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝑋 = X𝑦 ∈ 𝐴 (𝑎‘𝑦) ∧ 𝑌 = X𝑦 ∈ 𝐴 (𝑏‘𝑦))) → (𝑋 ∩ 𝑌) ∈ 𝐵))
66	7, 65	syl5bi 244	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ((((𝑎 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑎‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑐 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑐)(𝑎‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑋 = X𝑦 ∈ 𝐴 (𝑎‘𝑦)) ∧ ((𝑏 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑏‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑑 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑑)(𝑏‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑌 = X𝑦 ∈ 𝐴 (𝑏‘𝑦))) → (𝑋 ∩ 𝑌) ∈ 𝐵))
67	66	exlimdvv 1935	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (∃𝑎∃𝑏(((𝑎 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑎‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑐 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑐)(𝑎‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑋 = X𝑦 ∈ 𝐴 (𝑎‘𝑦)) ∧ ((𝑏 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑏‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑑 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑑)(𝑏‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑌 = X𝑦 ∈ 𝐴 (𝑏‘𝑦))) → (𝑋 ∩ 𝑌) ∈ 𝐵))
68	6, 67	syl5bi 244	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ((𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∩ 𝑌) ∈ 𝐵))
69	68	imp 409	1 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 ∩ 𝑌) ∈ 𝐵)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 398 ∧ w3a 1083 = wceq 1537 ∃wex 1780 ∈ wcel 2114 {cab 2799 ∀wral 3138 ∃wrex 3139 ∖ cdif 3933 ∪ cun 3934 ∩ cin 3935 ⊆ wss 3936 ∪ cuni 4838 Fn wfn 6350 ⟶wf 6351 ‘cfv 6355 Xcixp 8461 Fincfn 8509 Topctop 21501

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-rep 5190 ax-sep 5203 ax-nul 5210 ax-pow 5266 ax-pr 5330 ax-un 7461

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-ral 3143 df-rex 3144 df-reu 3145 df-rab 3147 df-v 3496 df-sbc 3773 df-csb 3884 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-pss 3954 df-nul 4292 df-if 4468 df-pw 4541 df-sn 4568 df-pr 4570 df-tp 4572 df-op 4574 df-uni 4839 df-int 4877 df-iun 4921 df-br 5067 df-opab 5129 df-mpt 5147 df-tr 5173 df-id 5460 df-eprel 5465 df-po 5474 df-so 5475 df-fr 5514 df-we 5516 df-xp 5561 df-rel 5562 df-cnv 5563 df-co 5564 df-dm 5565 df-rn 5566 df-res 5567 df-ima 5568 df-pred 6148 df-ord 6194 df-on 6195 df-lim 6196 df-suc 6197 df-iota 6314 df-fun 6357 df-fn 6358 df-f 6359 df-f1 6360 df-fo 6361 df-f1o 6362 df-fv 6363 df-ov 7159 df-oprab 7160 df-mpo 7161 df-om 7581 df-wrecs 7947 df-recs 8008 df-rdg 8046 df-oadd 8106 df-er 8289 df-ixp 8462 df-en 8510 df-fin 8513 df-top 21502

This theorem is referenced by: ptbasin2 22186

W3C validator