ptbasfi - Metamath Proof Explorer

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

Theorem ptbasfi 23537

Description: The basis for the product topology can also be written as the set of finite intersections of "cylinder sets", the preimages of projections into one factor from open sets in the factor. (We have to add 𝑋 itself to the list because if 𝐴 is empty we get (fi‘∅) = ∅ while 𝐵 = {∅}.) (Contributed by Mario Carneiro, 3-Feb-2015.)

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

**Assertion**
Ref	Expression
ptbasfi	⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝐵 = (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))

Distinct variable groups: 𝑘,𝑛,𝑢,𝐵 𝑤,𝑔,𝑥,𝑦,𝑛,𝑘,𝑢,𝑧,𝐴 𝑔,𝐹,𝑘,𝑛,𝑢,𝑤,𝑥,𝑦,𝑧 𝑔,𝑋,𝑘,𝑢,𝑤,𝑥,𝑧 𝑔,𝑉,𝑘,𝑛,𝑢,𝑤,𝑥,𝑦,𝑧 Allowed substitution hints: 𝐵(𝑥,𝑦,𝑧,𝑤,𝑔) 𝑋(𝑦,𝑛)

Proof of Theorem ptbasfi Dummy variables 𝑠 ℎ 𝑚 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ptbas.1	. . . . 5 ⊢ 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑧)(𝑔‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑥 = X𝑦 ∈ 𝐴 (𝑔‘𝑦))}
2	1	elpt 23528	. . . 4 ⊢ (𝑠 ∈ 𝐵 ↔ ∃ℎ((ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑠 = X𝑦 ∈ 𝐴 (ℎ‘𝑦)))
3		df-3an 1089	. . . . . . . 8 ⊢ ((ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦)) ↔ ((ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦)) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦)))
4		simprr 773	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))
5		disjdif2 4434	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∩ 𝑚) = ∅ → (𝐴 ∖ 𝑚) = 𝐴)
6	5	raleqdv 3298	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∩ 𝑚) = ∅ → (∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦) ↔ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) = ∪ (𝐹‘𝑦)))
7	6	biimpac 478	. . . . . . . . . . . . . . . 16 ⊢ ((∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦) ∧ (𝐴 ∩ 𝑚) = ∅) → ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) = ∪ (𝐹‘𝑦))
8		ixpeq2 8861	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑦 ∈ 𝐴 (ℎ‘𝑦) = ∪ (𝐹‘𝑦) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) = X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦))
9	7, 8	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦) ∧ (𝐴 ∩ 𝑚) = ∅) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) = X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦))
10		ptbasfi.2	. . . . . . . . . . . . . . . 16 ⊢ 𝑋 = X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛)
11		fveq2 6842	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑦 → (𝐹‘𝑛) = (𝐹‘𝑦))
12	11	unieqd 4878	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑦 → ∪ (𝐹‘𝑛) = ∪ (𝐹‘𝑦))
13	12	cbvixpv 8865	. . . . . . . . . . . . . . . 16 ⊢ X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) = X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦)
14	10, 13	eqtri 2760	. . . . . . . . . . . . . . 15 ⊢ 𝑋 = X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦)
15	9, 14	eqtr4di 2790	. . . . . . . . . . . . . 14 ⊢ ((∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦) ∧ (𝐴 ∩ 𝑚) = ∅) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) = 𝑋)
16	4, 15	sylan 581	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) = ∅) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) = 𝑋)
17		ssv 3960	. . . . . . . . . . . . . . . 16 ⊢ 𝑋 ⊆ V
18		iineq1 4966	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∩ 𝑚) = ∅ → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) = ∩ 𝑛 ∈ ∅ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
19		0iin 5021	. . . . . . . . . . . . . . . . 17 ⊢ ∩ 𝑛 ∈ ∅ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) = V
20	18, 19	eqtrdi 2788	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∩ 𝑚) = ∅ → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) = V)
21	17, 20	sseqtrrid 3979	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∩ 𝑚) = ∅ → 𝑋 ⊆ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
22	21	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) = ∅) → 𝑋 ⊆ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
23		dfss2 3921	. . . . . . . . . . . . . 14 ⊢ (𝑋 ⊆ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ↔ (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) = 𝑋)
24	22, 23	sylib 218	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) = ∅) → (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) = 𝑋)
25	16, 24	eqtr4d 2775	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) = ∅) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) = (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))))
26		simplll 775	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top))
27		inss1 4191	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∩ 𝑚) ⊆ 𝐴
28		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → 𝑛 ∈ (𝐴 ∩ 𝑚))
29	27, 28	sselid 3933	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → 𝑛 ∈ 𝐴)
30		fveq2 6842	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑛 → (ℎ‘𝑦) = (ℎ‘𝑛))
31		fveq2 6842	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑛 → (𝐹‘𝑦) = (𝐹‘𝑛))
32	30, 31	eleq12d 2831	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑛 → ((ℎ‘𝑦) ∈ (𝐹‘𝑦) ↔ (ℎ‘𝑛) ∈ (𝐹‘𝑛)))
33		simprr 773	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) → ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))
34	33	ad2antrr 727	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))
35	32, 34, 29	rspcdva 3579	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (ℎ‘𝑛) ∈ (𝐹‘𝑛))
36	14	ptpjpre1 23527	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (𝑛 ∈ 𝐴 ∧ (ℎ‘𝑛) ∈ (𝐹‘𝑛))) → (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) = X𝑦 ∈ 𝐴 if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
37	26, 29, 35, 36	syl12anc 837	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) = X𝑦 ∈ 𝐴 if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
38	37	adantlr 716	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) = X𝑦 ∈ 𝐴 if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
39	38	iineq2dv 4974	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)X𝑦 ∈ 𝐴 if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
40		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → (𝐴 ∩ 𝑚) ≠ ∅)
41		cnvimass 6049	. . . . . . . . . . . . . . . . . . . 20 ⊢ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ dom (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛))
42		eqid 2737	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) = (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛))
43	42	dmmptss 6207	. . . . . . . . . . . . . . . . . . . 20 ⊢ dom (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) ⊆ 𝑋
44	41, 43	sstri 3945	. . . . . . . . . . . . . . . . . . 19 ⊢ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ 𝑋
45	44, 14	sseqtri 3984	. . . . . . . . . . . . . . . . . 18 ⊢ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦)
46	45	rgenw 3056	. . . . . . . . . . . . . . . . 17 ⊢ ∀𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦)
47		r19.2z 4454	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∩ 𝑚) ≠ ∅ ∧ ∀𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦)) → ∃𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦))
48	40, 46, 47	sylancl 587	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → ∃𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦))
49		iinss 5014	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦))
50	48, 49	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦))
51	50, 14	sseqtrrdi 3977	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ 𝑋)
52		sseqin2 4177	. . . . . . . . . . . . . 14 ⊢ (∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ 𝑋 ↔ (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
53	51, 52	sylib 218	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
54	33	ad2antrr 727	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))
55		ssralv 4004	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∩ 𝑚) ⊆ 𝐴 → (∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦) → ∀𝑦 ∈ (𝐴 ∩ 𝑚)(ℎ‘𝑦) ∈ (𝐹‘𝑦)))
56	27, 55	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦) → ∀𝑦 ∈ (𝐴 ∩ 𝑚)(ℎ‘𝑦) ∈ (𝐹‘𝑦))
57		elssuni 4896	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((ℎ‘𝑦) ∈ (𝐹‘𝑦) → (ℎ‘𝑦) ⊆ ∪ (𝐹‘𝑦))
58		iffalse 4490	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (¬ 𝑦 = 𝑛 → if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) = ∪ (𝐹‘𝑦))
59	58	sseq2d 3968	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ 𝑦 = 𝑛 → ((ℎ‘𝑦) ⊆ if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ↔ (ℎ‘𝑦) ⊆ ∪ (𝐹‘𝑦)))
60	57, 59	syl5ibrcom 247	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ℎ‘𝑦) ∈ (𝐹‘𝑦) → (¬ 𝑦 = 𝑛 → (ℎ‘𝑦) ⊆ if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦))))
61		ssid 3958	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ℎ‘𝑦) ⊆ (ℎ‘𝑦)
62		iftrue 4487	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = 𝑛 → if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) = (ℎ‘𝑛))
63	62, 30	eqtr4d 2775	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = 𝑛 → if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) = (ℎ‘𝑦))
64	61, 63	sseqtrrid 3979	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = 𝑛 → (ℎ‘𝑦) ⊆ if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
65	60, 64	pm2.61d2 181	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℎ‘𝑦) ∈ (𝐹‘𝑦) → (ℎ‘𝑦) ⊆ if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
66	65	ralrimivw 3134	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℎ‘𝑦) ∈ (𝐹‘𝑦) → ∀𝑛 ∈ (𝐴 ∩ 𝑚)(ℎ‘𝑦) ⊆ if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
67		ssiin 5013	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℎ‘𝑦) ⊆ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ↔ ∀𝑛 ∈ (𝐴 ∩ 𝑚)(ℎ‘𝑦) ⊆ if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
68	66, 67	sylibr 234	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ‘𝑦) ∈ (𝐹‘𝑦) → (ℎ‘𝑦) ⊆ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
69	68	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ (𝐴 ∩ 𝑚) ∧ (ℎ‘𝑦) ∈ (𝐹‘𝑦)) → (ℎ‘𝑦) ⊆ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
70	62	equcoms 2022	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 = 𝑦 → if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) = (ℎ‘𝑛))
71		fveq2 6842	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 = 𝑦 → (ℎ‘𝑛) = (ℎ‘𝑦))
72	70, 71	eqtrd 2772	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑦 → if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) = (ℎ‘𝑦))
73	72	sseq1d 3967	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑦 → (if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ⊆ (ℎ‘𝑦) ↔ (ℎ‘𝑦) ⊆ (ℎ‘𝑦)))
74	73	rspcev 3578	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑦 ∈ (𝐴 ∩ 𝑚) ∧ (ℎ‘𝑦) ⊆ (ℎ‘𝑦)) → ∃𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ⊆ (ℎ‘𝑦))
75	61, 74	mpan2 692	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ (𝐴 ∩ 𝑚) → ∃𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ⊆ (ℎ‘𝑦))
76		iinss 5014	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ⊆ (ℎ‘𝑦) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ⊆ (ℎ‘𝑦))
77	75, 76	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ (𝐴 ∩ 𝑚) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ⊆ (ℎ‘𝑦))
78	77	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ (𝐴 ∩ 𝑚) ∧ (ℎ‘𝑦) ∈ (𝐹‘𝑦)) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ⊆ (ℎ‘𝑦))
79	69, 78	eqssd 3953	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ (𝐴 ∩ 𝑚) ∧ (ℎ‘𝑦) ∈ (𝐹‘𝑦)) → (ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
80	79	ralimiaa 3074	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑦 ∈ (𝐴 ∩ 𝑚)(ℎ‘𝑦) ∈ (𝐹‘𝑦) → ∀𝑦 ∈ (𝐴 ∩ 𝑚)(ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
81	54, 56, 80	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → ∀𝑦 ∈ (𝐴 ∩ 𝑚)(ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
82		eldifn 4086	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ (𝐴 ∖ 𝑚) → ¬ 𝑦 ∈ 𝑚)
83	82	ad2antlr 728	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ∩ 𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴 ∖ 𝑚)) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → ¬ 𝑦 ∈ 𝑚)
84		inss2 4192	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐴 ∩ 𝑚) ⊆ 𝑚
85		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐴 ∩ 𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴 ∖ 𝑚)) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → 𝑛 ∈ (𝐴 ∩ 𝑚))
86	84, 85	sselid 3933	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐴 ∩ 𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴 ∖ 𝑚)) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → 𝑛 ∈ 𝑚)
87		eleq1 2825	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = 𝑛 → (𝑦 ∈ 𝑚 ↔ 𝑛 ∈ 𝑚))
88	86, 87	syl5ibrcom 247	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ∩ 𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴 ∖ 𝑚)) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (𝑦 = 𝑛 → 𝑦 ∈ 𝑚))
89	83, 88	mtod 198	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∩ 𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴 ∖ 𝑚)) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → ¬ 𝑦 = 𝑛)
90	89, 58	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∩ 𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴 ∖ 𝑚)) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) = ∪ (𝐹‘𝑦))
91	90	iineq2dv 4974	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∩ 𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴 ∖ 𝑚)) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)∪ (𝐹‘𝑦))
92		iinconst 4959	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∩ 𝑚) ≠ ∅ → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)∪ (𝐹‘𝑦) = ∪ (𝐹‘𝑦))
93	92	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∩ 𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴 ∖ 𝑚)) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)∪ (𝐹‘𝑦) = ∪ (𝐹‘𝑦))
94	91, 93	eqtr2d 2773	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∩ 𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴 ∖ 𝑚)) → ∪ (𝐹‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
95		eqeq1 2741	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℎ‘𝑦) = ∪ (𝐹‘𝑦) → ((ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ↔ ∪ (𝐹‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦))))
96	94, 95	syl5ibrcom 247	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∩ 𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴 ∖ 𝑚)) → ((ℎ‘𝑦) = ∪ (𝐹‘𝑦) → (ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦))))
97	96	ralimdva 3150	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∩ 𝑚) ≠ ∅ → (∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦) → ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦))))
98	4, 97	mpan9 506	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
99		inundif 4433	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∩ 𝑚) ∪ (𝐴 ∖ 𝑚)) = 𝐴
100	99	raleqi 3296	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑦 ∈ ((𝐴 ∩ 𝑚) ∪ (𝐴 ∖ 𝑚))(ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ↔ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
101		ralunb 4151	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑦 ∈ ((𝐴 ∩ 𝑚) ∪ (𝐴 ∖ 𝑚))(ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ↔ (∀𝑦 ∈ (𝐴 ∩ 𝑚)(ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦))))
102	100, 101	bitr3i 277	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑦 ∈ 𝐴 (ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ↔ (∀𝑦 ∈ (𝐴 ∩ 𝑚)(ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦))))
103	81, 98, 102	sylanbrc 584	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
104		ixpeq2 8861	. . . . . . . . . . . . . . 15 ⊢ (∀𝑦 ∈ 𝐴 (ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) = X𝑦 ∈ 𝐴 ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
105	103, 104	syl 17	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) = X𝑦 ∈ 𝐴 ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
106		ixpiin 8874	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∩ 𝑚) ≠ ∅ → X𝑦 ∈ 𝐴 ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)X𝑦 ∈ 𝐴 if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
107	106	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → X𝑦 ∈ 𝐴 ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)X𝑦 ∈ 𝐴 if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
108	105, 107	eqtrd 2772	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)X𝑦 ∈ 𝐴 if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
109	39, 53, 108	3eqtr4rd 2783	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) = (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))))
110	25, 109	pm2.61dane 3020	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) = (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))))
111		ixpexg 8872	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∀𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) ∈ V → X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) ∈ V)
112		fvex 6855	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐹‘𝑛) ∈ V
113	112	uniex 7696	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ∪ (𝐹‘𝑛) ∈ V
114	113	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 ∈ 𝐴 → ∪ (𝐹‘𝑛) ∈ V)
115	111, 114	mprg 3058	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) ∈ V
116	10, 115	eqeltri 2833	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑋 ∈ V
117	116	mptex 7179	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) ∈ V
118	117	cnvex 7877	. . . . . . . . . . . . . . . . . . . 20 ⊢ ^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) ∈ V
119	118	imaex 7866	. . . . . . . . . . . . . . . . . . 19 ⊢ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ∈ V
120	119	dfiin2 4990	. . . . . . . . . . . . . . . . . 18 ⊢ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) = ∩ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))}
121		inteq 4907	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} = ∅ → ∩ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} = ∩ ∅)
122	120, 121	eqtrid 2784	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} = ∅ → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) = ∩ ∅)
123		int0 4919	. . . . . . . . . . . . . . . . 17 ⊢ ∩ ∅ = V
124	122, 123	eqtrdi 2788	. . . . . . . . . . . . . . . 16 ⊢ ({𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} = ∅ → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) = V)
125	124	ineq2d 4174	. . . . . . . . . . . . . . 15 ⊢ ({𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} = ∅ → (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) = (𝑋 ∩ V))
126		inv1 4352	. . . . . . . . . . . . . . 15 ⊢ (𝑋 ∩ V) = 𝑋
127	125, 126	eqtrdi 2788	. . . . . . . . . . . . . 14 ⊢ ({𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} = ∅ → (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) = 𝑋)
128	127	adantl 481	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} = ∅) → (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) = 𝑋)
129		snex 5385	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑋} ∈ V
130	1	ptbas 23535	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝐵 ∈ TopBases)
131	1, 10	ptpjpre2 23536	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (𝑘 ∈ 𝐴 ∧ 𝑢 ∈ (𝐹‘𝑘))) → (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝐵)
132	131	ralrimivva 3181	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ∀𝑘 ∈ 𝐴 ∀𝑢 ∈ (𝐹‘𝑘)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝐵)
133		eqid 2737	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) = (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))
134	133	fmpox 8021	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑘 ∈ 𝐴 ∀𝑢 ∈ (𝐹‘𝑘)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝐵 ↔ (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)):∪ 𝑘 ∈ 𝐴 ({𝑘} × (𝐹‘𝑘))⟶𝐵)
135	132, 134	sylib 218	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)):∪ 𝑘 ∈ 𝐴 ({𝑘} × (𝐹‘𝑘))⟶𝐵)
136	135	frnd 6678	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) ⊆ 𝐵)
137	130, 136	ssexd 5271	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) ∈ V)
138		unexg 7698	. . . . . . . . . . . . . . . . . 18 ⊢ (({𝑋} ∈ V ∧ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) ∈ V) → ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ∈ V)
139	129, 137, 138	sylancr 588	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ∈ V)
140		ssfii 9334	. . . . . . . . . . . . . . . . 17 ⊢ (({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ∈ V → ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ⊆ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
141	139, 140	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ⊆ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
142	141	ad2antrr 727	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ⊆ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
143		ssun1 4132	. . . . . . . . . . . . . . . . 17 ⊢ {𝑋} ⊆ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))
144	116	snss 4743	. . . . . . . . . . . . . . . . 17 ⊢ (𝑋 ∈ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ↔ {𝑋} ⊆ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))
145	143, 144	mpbir 231	. . . . . . . . . . . . . . . 16 ⊢ 𝑋 ∈ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))
146	145	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → 𝑋 ∈ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))
147	142, 146	sseldd 3936	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → 𝑋 ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
148	147	adantr 480	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} = ∅) → 𝑋 ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
149	128, 148	eqeltrd 2837	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} = ∅) → (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
150	139	ad3antrrr 731	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ∈ V)
151		nfv 1916	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑛(((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦)))
152		nfcv 2899	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑛𝐴
153		nfcv 2899	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑛(𝐹‘𝑘)
154		nfixp1 8868	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ Ⅎ𝑛X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛)
155	10, 154	nfcxfr 2897	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ Ⅎ𝑛𝑋
156		nfcv 2899	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ Ⅎ𝑛(𝑤‘𝑘)
157	155, 156	nfmpt 5198	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ Ⅎ𝑛(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘))
158	157	nfcnv 5835	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑛^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘))
159		nfcv 2899	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑛𝑢
160	158, 159	nfima 6035	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑛(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)
161	152, 153, 160	nfmpo 7450	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑛(𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))
162	161	nfrn 5909	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑛ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))
163	162	nfcri 2891	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑛 𝑧 ∈ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))
164		df-ov 7371	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑛(𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))(ℎ‘𝑛)) = ((𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))‘⟨𝑛, (ℎ‘𝑛)⟩)
165	119	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ∈ V)
166		fveq2 6842	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑘 = 𝑛 → (𝑤‘𝑘) = (𝑤‘𝑛))
167	166	mpteq2dv 5194	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑘 = 𝑛 → (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) = (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)))
168	167	cnveqd 5832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑘 = 𝑛 → ^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) = ^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)))
169	168	imaeq1d 6026	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑘 = 𝑛 → (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ 𝑢))
170		imaeq2 6023	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑢 = (ℎ‘𝑛) → (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ 𝑢) = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
171	169, 170	sylan9eq 2792	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑘 = 𝑛 ∧ 𝑢 = (ℎ‘𝑛)) → (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
172		fveq2 6842	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑘 = 𝑛 → (𝐹‘𝑘) = (𝐹‘𝑛))
173	171, 172, 133	ovmpox 7521	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑛 ∈ 𝐴 ∧ (ℎ‘𝑛) ∈ (𝐹‘𝑛) ∧ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ∈ V) → (𝑛(𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))(ℎ‘𝑛)) = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
174	29, 35, 165, 173	syl3anc 1374	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (𝑛(𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))(ℎ‘𝑛)) = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
175	164, 174	eqtr3id 2786	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → ((𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))‘⟨𝑛, (ℎ‘𝑛)⟩) = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
176	135	ad3antrrr 731	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)):∪ 𝑘 ∈ 𝐴 ({𝑘} × (𝐹‘𝑘))⟶𝐵)
177	176	ffnd 6671	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) Fn ∪ 𝑘 ∈ 𝐴 ({𝑘} × (𝐹‘𝑘)))
178		opeliunxp 5699	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (⟨𝑛, (ℎ‘𝑛)⟩ ∈ ∪ 𝑛 ∈ 𝐴 ({𝑛} × (𝐹‘𝑛)) ↔ (𝑛 ∈ 𝐴 ∧ (ℎ‘𝑛) ∈ (𝐹‘𝑛)))
179	29, 35, 178	sylanbrc 584	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → ⟨𝑛, (ℎ‘𝑛)⟩ ∈ ∪ 𝑛 ∈ 𝐴 ({𝑛} × (𝐹‘𝑛)))
180		sneq 4592	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑛 = 𝑘 → {𝑛} = {𝑘})
181		fveq2 6842	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑛 = 𝑘 → (𝐹‘𝑛) = (𝐹‘𝑘))
182	180, 181	xpeq12d 5663	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑛 = 𝑘 → ({𝑛} × (𝐹‘𝑛)) = ({𝑘} × (𝐹‘𝑘)))
183	182	cbviunv 4996	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ∪ 𝑛 ∈ 𝐴 ({𝑛} × (𝐹‘𝑛)) = ∪ 𝑘 ∈ 𝐴 ({𝑘} × (𝐹‘𝑘))
184	179, 183	eleqtrdi 2847	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → ⟨𝑛, (ℎ‘𝑛)⟩ ∈ ∪ 𝑘 ∈ 𝐴 ({𝑘} × (𝐹‘𝑘)))
185		fnfvelrn 7034	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) Fn ∪ 𝑘 ∈ 𝐴 ({𝑘} × (𝐹‘𝑘)) ∧ ⟨𝑛, (ℎ‘𝑛)⟩ ∈ ∪ 𝑘 ∈ 𝐴 ({𝑘} × (𝐹‘𝑘))) → ((𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))‘⟨𝑛, (ℎ‘𝑛)⟩) ∈ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))
186	177, 184, 185	syl2anc 585	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → ((𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))‘⟨𝑛, (ℎ‘𝑛)⟩) ∈ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))
187	175, 186	eqeltrrd 2838	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ∈ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))
188		eleq1 2825	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) → (𝑧 ∈ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) ↔ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ∈ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))
189	187, 188	syl5ibrcom 247	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) → 𝑧 ∈ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))
190	189	ex 412	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → (𝑛 ∈ (𝐴 ∩ 𝑚) → (𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) → 𝑧 ∈ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
191	151, 163, 190	rexlimd 3245	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → (∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) → 𝑧 ∈ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))
192	191	abssdv 4021	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ⊆ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))
193		ssun2 4133	. . . . . . . . . . . . . . . . . . . 20 ⊢ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) ⊆ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))
194	192, 193	sstrdi 3948	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ⊆ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))
195	194	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ⊆ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))
196		simpr 484	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅)
197		simplrl 777	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → 𝑚 ∈ Fin)
198		ssfi 9109	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑚 ∈ Fin ∧ (𝐴 ∩ 𝑚) ⊆ 𝑚) → (𝐴 ∩ 𝑚) ∈ Fin)
199	197, 84, 198	sylancl 587	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → (𝐴 ∩ 𝑚) ∈ Fin)
200		abrexfi 9264	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∩ 𝑚) ∈ Fin → {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ∈ Fin)
201	199, 200	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ∈ Fin)
202		elfir 9330	. . . . . . . . . . . . . . . . . 18 ⊢ ((({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ∈ V ∧ ({𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ⊆ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅ ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ∈ Fin)) → ∩ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
203	150, 195, 196, 201, 202	syl13anc 1375	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → ∩ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
204	120, 203	eqeltrid 2841	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
205		elssuni 4896	. . . . . . . . . . . . . . . 16 ⊢ (∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ ∪ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
206	204, 205	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ ∪ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
207		fiuni 9343	. . . . . . . . . . . . . . . . . 18 ⊢ (({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ∈ V → ∪ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) = ∪ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
208	139, 207	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ∪ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) = ∪ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
209	116	pwid 4578	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑋 ∈ 𝒫 𝑋
210	209	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝑋 ∈ 𝒫 𝑋)
211	210	snssd 4767	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → {𝑋} ⊆ 𝒫 𝑋)
212	1	ptuni2 23532	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) = ∪ 𝐵)
213	10, 212	eqtrid 2784	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝑋 = ∪ 𝐵)
214		eqimss2 3995	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑋 = ∪ 𝐵 → ∪ 𝐵 ⊆ 𝑋)
215	213, 214	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ∪ 𝐵 ⊆ 𝑋)
216		sspwuni 5057	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐵 ⊆ 𝒫 𝑋 ↔ ∪ 𝐵 ⊆ 𝑋)
217	215, 216	sylibr 234	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝐵 ⊆ 𝒫 𝑋)
218	136, 217	sstrd 3946	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) ⊆ 𝒫 𝑋)
219	211, 218	unssd 4146	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ⊆ 𝒫 𝑋)
220		sspwuni 5057	. . . . . . . . . . . . . . . . . . 19 ⊢ (({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ⊆ 𝒫 𝑋 ↔ ∪ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ⊆ 𝑋)
221	219, 220	sylib 218	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ∪ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ⊆ 𝑋)
222		elssuni 4896	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑋 ∈ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) → 𝑋 ⊆ ∪ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))
223	145, 222	mp1i 13	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝑋 ⊆ ∪ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))
224	221, 223	eqssd 3953	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ∪ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) = 𝑋)
225	208, 224	eqtr3d 2774	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ∪ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))) = 𝑋)
226	225	ad3antrrr 731	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → ∪ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))) = 𝑋)
227	206, 226	sseqtrd 3972	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ 𝑋)
228	227, 52	sylib 218	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
229	228, 204	eqeltrd 2837	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
230	149, 229	pm2.61dane 3020	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
231	110, 230	eqeltrd 2837	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
232	231	rexlimdvaa 3140	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) → (∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))))
233	232	impr 454	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ ((ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦)) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
234	3, 233	sylan2b 595	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
235		eleq1 2825	. . . . . . 7 ⊢ (𝑠 = X𝑦 ∈ 𝐴 (ℎ‘𝑦) → (𝑠 ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))) ↔ X𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))))
236	234, 235	syl5ibrcom 247	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → (𝑠 = X𝑦 ∈ 𝐴 (ℎ‘𝑦) → 𝑠 ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))))
237	236	expimpd 453	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (((ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑠 = X𝑦 ∈ 𝐴 (ℎ‘𝑦)) → 𝑠 ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))))
238	237	exlimdv 1935	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (∃ℎ((ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑠 = X𝑦 ∈ 𝐴 (ℎ‘𝑦)) → 𝑠 ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))))
239	2, 238	biimtrid 242	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (𝑠 ∈ 𝐵 → 𝑠 ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))))
240	239	ssrdv 3941	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝐵 ⊆ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
241	1	ptbasid 23531	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) ∈ 𝐵)
242	10, 241	eqeltrid 2841	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝑋 ∈ 𝐵)
243	242	snssd 4767	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → {𝑋} ⊆ 𝐵)
244	243, 136	unssd 4146	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ⊆ 𝐵)
245		fiss 9339	. . . 4 ⊢ ((𝐵 ∈ TopBases ∧ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ⊆ 𝐵) → (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))) ⊆ (fi‘𝐵))
246	130, 244, 245	syl2anc 585	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))) ⊆ (fi‘𝐵))
247	1	ptbasin2 23534	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (fi‘𝐵) = 𝐵)
248	246, 247	sseqtrd 3972	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))) ⊆ 𝐵)
249	240, 248	eqssd 3953	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝐵 = (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∃wex 1781 ∈ wcel 2114 {cab 2715 ≠ wne 2933 ∀wral 3052 ∃wrex 3062 Vcvv 3442 ∖ cdif 3900 ∪ cun 3901 ∩ cin 3902 ⊆ wss 3903 ∅c0 4287 ifcif 4481 𝒫 cpw 4556 {csn 4582 ⟨cop 4588 ∪ cuni 4865 ∩ cint 4904 ∪ ciun 4948 ∩ ciin 4949 ↦ cmpt 5181 × cxp 5630 ^◡ccnv 5631 dom cdm 5632 ran crn 5633 “ cima 5635 Fn wfn 6495 ⟶wf 6496 ‘cfv 6500 (class class class)co 7368 ∈ cmpo 7370 Xcixp 8847 Fincfn 8895 ficfi 9325 Topctop 22849 TopBasesctb 22901

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 5226 ax-sep 5243 ax-nul 5253 ax-pow 5312 ax-pr 5379 ax-un 7690

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 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-int 4905 df-iun 4950 df-iin 4951 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5527 df-eprel 5532 df-po 5540 df-so 5541 df-fr 5585 df-we 5587 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-ord 6328 df-on 6329 df-lim 6330 df-suc 6331 df-iota 6456 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-ov 7371 df-oprab 7372 df-mpo 7373 df-om 7819 df-1st 7943 df-2nd 7944 df-1o 8407 df-2o 8408 df-ixp 8848 df-en 8896 df-dom 8897 df-fin 8899 df-fi 9326 df-top 22850 df-bases 22902

This theorem is referenced by: ptval2 23557 xkoptsub 23610 ptcmplem1 24008 prdsxmslem2 24485

W3C validator