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 23955

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 23946	. . . 4 ⊢ (𝑠 ∈ 𝐵 ↔ ∃ℎ((ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑠 = X𝑦 ∈ 𝐴 (ℎ‘𝑦)))
3		df-3an 1105	. . . . . . . 8 ⊢ ((ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦)) ↔ ((ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦)) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦)))
4		simprr 785	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))
5		disjdif2 4439	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∩ 𝑚) = ∅ → (𝐴 ∖ 𝑚) = 𝐴)
6	5	raleqdv 3323	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∩ 𝑚) = ∅ → (∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦) ↔ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) = ∪ (𝐹‘𝑦)))
7	6	biimpac 484	. . . . . . . . . . . . . . . 16 ⊢ ((∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦) ∧ (𝐴 ∩ 𝑚) = ∅) → ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) = ∪ (𝐹‘𝑦))
8		ixpeq2 8977	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑦 ∈ 𝐴 (ℎ‘𝑦) = ∪ (𝐹‘𝑦) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) = X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦))
9	7, 8	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦) ∧ (𝐴 ∩ 𝑚) = ∅) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) = X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦))
10		ptbasfi.2	. . . . . . . . . . . . . . . 16 ⊢ 𝑋 = X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛)
11		fveq2 6916	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑦 → (𝐹‘𝑛) = (𝐹‘𝑦))
12	11	unieqd 4885	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑦 → ∪ (𝐹‘𝑛) = ∪ (𝐹‘𝑦))
13	12	cbvixpv 8981	. . . . . . . . . . . . . . . 16 ⊢ X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) = X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦)
14	10, 13	eqtri 2786	. . . . . . . . . . . . . . 15 ⊢ 𝑋 = X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦)
15	9, 14	eqtr4di 2816	. . . . . . . . . . . . . 14 ⊢ ((∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦) ∧ (𝐴 ∩ 𝑚) = ∅) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) = 𝑋)
16	4, 15	sylan 592	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) = ∅) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) = 𝑋)
17		ssv 3937	. . . . . . . . . . . . . . . 16 ⊢ 𝑋 ⊆ V
18		iineq1 4974	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∩ 𝑚) = ∅ → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) = ∩ 𝑛 ∈ ∅ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
19		0iin 5027	. . . . . . . . . . . . . . . . 17 ⊢ ∩ 𝑛 ∈ ∅ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) = V
20	18, 19	eqtrdi 2814	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∩ 𝑚) = ∅ → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) = V)
21	17, 20	sseqtrrid 3956	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∩ 𝑚) = ∅ → 𝑋 ⊆ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
22	21	adantl 487	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) = ∅) → 𝑋 ⊆ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
23		dfss2 4097	. . . . . . . . . . . . . 14 ⊢ (𝑋 ⊆ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ↔ (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) = 𝑋)
24	22, 23	sylib 221	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) = ∅) → (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) = 𝑋)
25	16, 24	eqtr4d 2801	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) = ∅) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) = (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))))
26		simplll 787	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top))
27		inss1 4136	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∩ 𝑚) ⊆ 𝐴
28		simpr 490	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → 𝑛 ∈ (𝐴 ∩ 𝑚))
29	27, 28	sselid 3911	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → 𝑛 ∈ 𝐴)
30		fveq2 6916	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑛 → (ℎ‘𝑦) = (ℎ‘𝑛))
31		fveq2 6916	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑛 → (𝐹‘𝑦) = (𝐹‘𝑛))
32	30, 31	eleq12d 2858	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑛 → ((ℎ‘𝑦) ∈ (𝐹‘𝑦) ↔ (ℎ‘𝑛) ∈ (𝐹‘𝑛)))
33		simprr 785	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) → ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))
34	33	ad2antrr 739	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))
35	32, 34, 29	rspcdva 3581	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (ℎ‘𝑛) ∈ (𝐹‘𝑛))
36	14	ptpjpre1 23945	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (𝑛 ∈ 𝐴 ∧ (ℎ‘𝑛) ∈ (𝐹‘𝑛))) → (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) = X𝑦 ∈ 𝐴 if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
37	26, 29, 35, 36	syl12anc 850	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) = X𝑦 ∈ 𝐴 if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
38	37	adantlr 728	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) = X𝑦 ∈ 𝐴 if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
39	38	iineq2dv 4982	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)X𝑦 ∈ 𝐴 if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
40		simpr 490	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → (𝐴 ∩ 𝑚) ≠ ∅)
41		cnvimass 6217	. . . . . . . . . . . . . . . . . . . 20 ⊢ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ dom (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛))
42		eqid 2763	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) = (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛))
43	42	dmmptss 6261	. . . . . . . . . . . . . . . . . . . 20 ⊢ dom (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) ⊆ 𝑋
44	41, 43	sstri 3922	. . . . . . . . . . . . . . . . . . 19 ⊢ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ 𝑋
45	44, 14	sseqtri 3961	. . . . . . . . . . . . . . . . . 18 ⊢ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦)
46	45	rgenw 3084	. . . . . . . . . . . . . . . . 17 ⊢ ∀𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦)
47		r19.2z 4458	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∩ 𝑚) ≠ ∅ ∧ ∀𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦)) → ∃𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦))
48	40, 46, 47	sylancl 598	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → ∃𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦))
49		iinss 5020	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦))
50	48, 49	syl 18	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦))
51	50, 14	sseqtrrdi 3954	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ 𝑋)
52		sseqin2 4123	. . . . . . . . . . . . . 14 ⊢ (∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ 𝑋 ↔ (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
53	51, 52	sylib 221	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
54	33	ad2antrr 739	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))
55		ssralv 3982	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∩ 𝑚) ⊆ 𝐴 → (∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦) → ∀𝑦 ∈ (𝐴 ∩ 𝑚)(ℎ‘𝑦) ∈ (𝐹‘𝑦)))
56	27, 55	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦) → ∀𝑦 ∈ (𝐴 ∩ 𝑚)(ℎ‘𝑦) ∈ (𝐹‘𝑦))
57		elssuni 4904	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((ℎ‘𝑦) ∈ (𝐹‘𝑦) → (ℎ‘𝑦) ⊆ ∪ (𝐹‘𝑦))
58		iffalse 4494	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (¬ 𝑦 = 𝑛 → if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) = ∪ (𝐹‘𝑦))
59	58	sseq2d 3945	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ 𝑦 = 𝑛 → ((ℎ‘𝑦) ⊆ if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ↔ (ℎ‘𝑦) ⊆ ∪ (𝐹‘𝑦)))
60	57, 59	syl5ibrcom 250	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ℎ‘𝑦) ∈ (𝐹‘𝑦) → (¬ 𝑦 = 𝑛 → (ℎ‘𝑦) ⊆ if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦))))
61		ssid 3935	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ℎ‘𝑦) ⊆ (ℎ‘𝑦)
62		iftrue 4491	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = 𝑛 → if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) = (ℎ‘𝑛))
63	62, 30	eqtr4d 2801	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = 𝑛 → if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) = (ℎ‘𝑦))
64	61, 63	sseqtrrid 3956	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = 𝑛 → (ℎ‘𝑦) ⊆ if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
65	60, 64	pm2.61d2 183	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℎ‘𝑦) ∈ (𝐹‘𝑦) → (ℎ‘𝑦) ⊆ if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
66	65	ralrimivw 3162	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℎ‘𝑦) ∈ (𝐹‘𝑦) → ∀𝑛 ∈ (𝐴 ∩ 𝑚)(ℎ‘𝑦) ⊆ if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
67		ssiin 5019	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℎ‘𝑦) ⊆ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ↔ ∀𝑛 ∈ (𝐴 ∩ 𝑚)(ℎ‘𝑦) ⊆ if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
68	66, 67	sylibr 237	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ‘𝑦) ∈ (𝐹‘𝑦) → (ℎ‘𝑦) ⊆ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
69	68	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ (𝐴 ∩ 𝑚) ∧ (ℎ‘𝑦) ∈ (𝐹‘𝑦)) → (ℎ‘𝑦) ⊆ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
70	62	equcoms 2055	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 = 𝑦 → if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) = (ℎ‘𝑛))
71		fveq2 6916	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 = 𝑦 → (ℎ‘𝑛) = (ℎ‘𝑦))
72	70, 71	eqtrd 2798	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑦 → if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) = (ℎ‘𝑦))
73	72	sseq1d 3944	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑦 → (if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ⊆ (ℎ‘𝑦) ↔ (ℎ‘𝑦) ⊆ (ℎ‘𝑦)))
74	73	rspcev 3580	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑦 ∈ (𝐴 ∩ 𝑚) ∧ (ℎ‘𝑦) ⊆ (ℎ‘𝑦)) → ∃𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ⊆ (ℎ‘𝑦))
75	61, 74	mpan2 704	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ (𝐴 ∩ 𝑚) → ∃𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ⊆ (ℎ‘𝑦))
76		iinss 5020	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ⊆ (ℎ‘𝑦) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ⊆ (ℎ‘𝑦))
77	75, 76	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ (𝐴 ∩ 𝑚) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ⊆ (ℎ‘𝑦))
78	77	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ (𝐴 ∩ 𝑚) ∧ (ℎ‘𝑦) ∈ (𝐹‘𝑦)) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ⊆ (ℎ‘𝑦))
79	69, 78	eqssd 3930	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ (𝐴 ∩ 𝑚) ∧ (ℎ‘𝑦) ∈ (𝐹‘𝑦)) → (ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
80	79	ralimiaa 3102	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑦 ∈ (𝐴 ∩ 𝑚)(ℎ‘𝑦) ∈ (𝐹‘𝑦) → ∀𝑦 ∈ (𝐴 ∩ 𝑚)(ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
81	54, 56, 80	3syl 19	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → ∀𝑦 ∈ (𝐴 ∩ 𝑚)(ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
82		eldifn 4071	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ (𝐴 ∖ 𝑚) → ¬ 𝑦 ∈ 𝑚)
83	82	ad2antlr 740	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ∩ 𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴 ∖ 𝑚)) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → ¬ 𝑦 ∈ 𝑚)
84		inss2 4137	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐴 ∩ 𝑚) ⊆ 𝑚
85		simpr 490	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐴 ∩ 𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴 ∖ 𝑚)) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → 𝑛 ∈ (𝐴 ∩ 𝑚))
86	84, 85	sselid 3911	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐴 ∩ 𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴 ∖ 𝑚)) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → 𝑛 ∈ 𝑚)
87		eleq1 2852	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = 𝑛 → (𝑦 ∈ 𝑚 ↔ 𝑛 ∈ 𝑚))
88	86, 87	syl5ibrcom 250	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ∩ 𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴 ∖ 𝑚)) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (𝑦 = 𝑛 → 𝑦 ∈ 𝑚))
89	83, 88	mtod 201	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∩ 𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴 ∖ 𝑚)) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → ¬ 𝑦 = 𝑛)
90	89, 58	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∩ 𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴 ∖ 𝑚)) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) = ∪ (𝐹‘𝑦))
91	90	iineq2dv 4982	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∩ 𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴 ∖ 𝑚)) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)∪ (𝐹‘𝑦))
92		iinconst 4967	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∩ 𝑚) ≠ ∅ → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)∪ (𝐹‘𝑦) = ∪ (𝐹‘𝑦))
93	92	adantr 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∩ 𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴 ∖ 𝑚)) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)∪ (𝐹‘𝑦) = ∪ (𝐹‘𝑦))
94	91, 93	eqtr2d 2799	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∩ 𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴 ∖ 𝑚)) → ∪ (𝐹‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
95		eqeq1 2767	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℎ‘𝑦) = ∪ (𝐹‘𝑦) → ((ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ↔ ∪ (𝐹‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦))))
96	94, 95	syl5ibrcom 250	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∩ 𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴 ∖ 𝑚)) → ((ℎ‘𝑦) = ∪ (𝐹‘𝑦) → (ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦))))
97	96	ralimdva 3178	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∩ 𝑚) ≠ ∅ → (∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦) → ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦))))
98	4, 97	mpan9 516	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
99		inundif 4438	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∩ 𝑚) ∪ (𝐴 ∖ 𝑚)) = 𝐴
100	99	raleqi 3321	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑦 ∈ ((𝐴 ∩ 𝑚) ∪ (𝐴 ∖ 𝑚))(ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ↔ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
101		ralunb 4198	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑦 ∈ ((𝐴 ∩ 𝑚) ∪ (𝐴 ∖ 𝑚))(ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ↔ (∀𝑦 ∈ (𝐴 ∩ 𝑚)(ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦))))
102	100, 101	bitr3i 280	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑦 ∈ 𝐴 (ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ↔ (∀𝑦 ∈ (𝐴 ∩ 𝑚)(ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦))))
103	81, 98, 102	sylanbrc 595	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
104		ixpeq2 8977	. . . . . . . . . . . . . . 15 ⊢ (∀𝑦 ∈ 𝐴 (ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) = X𝑦 ∈ 𝐴 ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
105	103, 104	syl 18	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) = X𝑦 ∈ 𝐴 ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
106		ixpiin 8990	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∩ 𝑚) ≠ ∅ → X𝑦 ∈ 𝐴 ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)X𝑦 ∈ 𝐴 if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
107	106	adantl 487	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → X𝑦 ∈ 𝐴 ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)X𝑦 ∈ 𝐴 if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
108	105, 107	eqtrd 2798	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)X𝑦 ∈ 𝐴 if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
109	39, 53, 108	3eqtr4rd 2809	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) = (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))))
110	25, 109	pm2.61dane 3046	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) = (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))))
111		ixpexg 8988	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∀𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) ∈ V → X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) ∈ V)
112		fvex 6929	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐹‘𝑛) ∈ V
113	112	uniex 7790	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ∪ (𝐹‘𝑛) ∈ V
114	113	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 ∈ 𝐴 → ∪ (𝐹‘𝑛) ∈ V)
115	111, 114	mprg 3086	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) ∈ V
116	10, 115	eqeltri 2860	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑋 ∈ V
117	116	mptex 7260	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) ∈ V
118	117	cnvex 7971	. . . . . . . . . . . . . . . . . . . 20 ⊢ ^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) ∈ V
119	118	imaex 7960	. . . . . . . . . . . . . . . . . . 19 ⊢ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ∈ V
120	119	dfiin2 4996	. . . . . . . . . . . . . . . . . 18 ⊢ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) = ∩ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))}
121		inteq 4915	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} = ∅ → ∩ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} = ∩ ∅)
122	120, 121	eqtrid 2810	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} = ∅ → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) = ∩ ∅)
123		int0 4927	. . . . . . . . . . . . . . . . 17 ⊢ ∩ ∅ = V
124	122, 123	eqtrdi 2814	. . . . . . . . . . . . . . . 16 ⊢ ({𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} = ∅ → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) = V)
125	124	ineq2d 4120	. . . . . . . . . . . . . . 15 ⊢ ({𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} = ∅ → (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) = (𝑋 ∩ V))
126		inv1 4351	. . . . . . . . . . . . . . 15 ⊢ (𝑋 ∩ V) = 𝑋
127	125, 126	eqtrdi 2814	. . . . . . . . . . . . . 14 ⊢ ({𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} = ∅ → (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) = 𝑋)
128	127	adantl 487	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} = ∅) → (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) = 𝑋)
129		snex 5404	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑋} ∈ V
130	1	ptbas 23953	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝐵 ∈ TopBases)
131	1, 10	ptpjpre2 23954	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (𝑘 ∈ 𝐴 ∧ 𝑢 ∈ (𝐹‘𝑘))) → (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝐵)
132	131	ralrimivva 3209	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ∀𝑘 ∈ 𝐴 ∀𝑢 ∈ (𝐹‘𝑘)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝐵)
133		eqid 2763	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) = (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))
134	133	fmpox 8113	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑘 ∈ 𝐴 ∀𝑢 ∈ (𝐹‘𝑘)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝐵 ↔ (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)):∪ 𝑘 ∈ 𝐴 ({𝑘} × (𝐹‘𝑘))⟶𝐵)
135	132, 134	sylib 221	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)):∪ 𝑘 ∈ 𝐴 ({𝑘} × (𝐹‘𝑘))⟶𝐵)
136	135	frnd 6748	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) ⊆ 𝐵)
137	130, 136	ssexd 5293	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) ∈ V)
138		unexg 7792	. . . . . . . . . . . . . . . . . 18 ⊢ (({𝑋} ∈ V ∧ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) ∈ V) → ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ∈ V)
139	129, 137, 138	sylancr 599	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ∈ V)
140		ssfii 9448	. . . . . . . . . . . . . . . . 17 ⊢ (({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ∈ V → ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ⊆ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
141	139, 140	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ⊆ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
142	141	ad2antrr 739	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ⊆ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
143		ssun1 4179	. . . . . . . . . . . . . . . . 17 ⊢ {𝑋} ⊆ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))
144	116	snss 4747	. . . . . . . . . . . . . . . . 17 ⊢ (𝑋 ∈ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ↔ {𝑋} ⊆ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))
145	143, 144	mpbir 234	. . . . . . . . . . . . . . . 16 ⊢ 𝑋 ∈ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))
146	145	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → 𝑋 ∈ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))
147	142, 146	sseldd 3914	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → 𝑋 ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
148	147	adantr 486	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} = ∅) → 𝑋 ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
149	128, 148	eqeltrd 2864	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} = ∅) → (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
150	139	ad3antrrr 743	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ∈ V)
151		nfv 1949	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑛(((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦)))
152		nfcv 2926	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑛𝐴
153		nfcv 2926	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑛(𝐹‘𝑘)
154		nfixp1 8984	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ Ⅎ𝑛X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛)
155	10, 154	nfcxfr 2924	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ Ⅎ𝑛𝑋
156		nfcv 2926	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ Ⅎ𝑛(𝑤‘𝑘)
157	155, 156	nfmpt 5209	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ Ⅎ𝑛(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘))
158	157	nfcnv 5868	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑛^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘))
159		nfcv 2926	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑛𝑢
160	158, 159	nfima 6082	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑛(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)
161	152, 153, 160	nfmpo 7533	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑛(𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))
162	161	nfrn 5946	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑛ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))
163	162	nfcri 2918	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑛 𝑧 ∈ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))
164		df-ov 7454	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑛(𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))(ℎ‘𝑛)) = ((𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))‘⟨𝑛, (ℎ‘𝑛)⟩)
165	119	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ∈ V)
166		fveq2 6916	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑘 = 𝑛 → (𝑤‘𝑘) = (𝑤‘𝑛))
167	166	mpteq2dv 5205	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑘 = 𝑛 → (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) = (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)))
168	167	cnveqd 5865	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑘 = 𝑛 → ^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) = ^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)))
169	168	imaeq1d 6069	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑘 = 𝑛 → (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ 𝑢))
170		imaeq2 6066	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑢 = (ℎ‘𝑛) → (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ 𝑢) = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
171	169, 170	sylan9eq 2818	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑘 = 𝑛 ∧ 𝑢 = (ℎ‘𝑛)) → (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
172		fveq2 6916	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑘 = 𝑛 → (𝐹‘𝑘) = (𝐹‘𝑛))
173	171, 172, 133	ovmpox 7605	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑛 ∈ 𝐴 ∧ (ℎ‘𝑛) ∈ (𝐹‘𝑛) ∧ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ∈ V) → (𝑛(𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))(ℎ‘𝑛)) = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
174	29, 35, 165, 173	syl3anc 1399	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (𝑛(𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))(ℎ‘𝑛)) = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
175	164, 174	eqtr3id 2812	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → ((𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))‘⟨𝑛, (ℎ‘𝑛)⟩) = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
176	135	ad3antrrr 743	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)):∪ 𝑘 ∈ 𝐴 ({𝑘} × (𝐹‘𝑘))⟶𝐵)
177	176	ffnd 6740	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) Fn ∪ 𝑘 ∈ 𝐴 ({𝑘} × (𝐹‘𝑘)))
178		opeliunxp 5725	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (⟨𝑛, (ℎ‘𝑛)⟩ ∈ ∪ 𝑛 ∈ 𝐴 ({𝑛} × (𝐹‘𝑛)) ↔ (𝑛 ∈ 𝐴 ∧ (ℎ‘𝑛) ∈ (𝐹‘𝑛)))
179	29, 35, 178	sylanbrc 595	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → ⟨𝑛, (ℎ‘𝑛)⟩ ∈ ∪ 𝑛 ∈ 𝐴 ({𝑛} × (𝐹‘𝑛)))
180		sneq 4594	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑛 = 𝑘 → {𝑛} = {𝑘})
181		fveq2 6916	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑛 = 𝑘 → (𝐹‘𝑛) = (𝐹‘𝑘))
182	180, 181	xpeq12d 5689	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑛 = 𝑘 → ({𝑛} × (𝐹‘𝑛)) = ({𝑘} × (𝐹‘𝑘)))
183	182	cbviunv 5002	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ∪ 𝑛 ∈ 𝐴 ({𝑛} × (𝐹‘𝑛)) = ∪ 𝑘 ∈ 𝐴 ({𝑘} × (𝐹‘𝑘))
184	179, 183	eleqtrdi 2874	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → ⟨𝑛, (ℎ‘𝑛)⟩ ∈ ∪ 𝑘 ∈ 𝐴 ({𝑘} × (𝐹‘𝑘)))
185		fnfvelrn 7112	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) Fn ∪ 𝑘 ∈ 𝐴 ({𝑘} × (𝐹‘𝑘)) ∧ ⟨𝑛, (ℎ‘𝑛)⟩ ∈ ∪ 𝑘 ∈ 𝐴 ({𝑘} × (𝐹‘𝑘))) → ((𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))‘⟨𝑛, (ℎ‘𝑛)⟩) ∈ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))
186	177, 184, 185	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → ((𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))‘⟨𝑛, (ℎ‘𝑛)⟩) ∈ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))
187	175, 186	eqeltrrd 2865	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ∈ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))
188		eleq1 2852	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) → (𝑧 ∈ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) ↔ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ∈ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))
189	187, 188	syl5ibrcom 250	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) → 𝑧 ∈ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))
190	189	ex 418	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → (𝑛 ∈ (𝐴 ∩ 𝑚) → (𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) → 𝑧 ∈ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
191	151, 163, 190	rexlimd 3273	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → (∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) → 𝑧 ∈ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))
192	191	abssdv 3995	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ⊆ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))
193		ssun2 4180	. . . . . . . . . . . . . . . . . . . 20 ⊢ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) ⊆ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))
194	192, 193	sstrdi 3925	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ⊆ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))
195	194	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ⊆ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))
196		simpr 490	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅)
197		simplrl 789	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → 𝑚 ∈ Fin)
198		ssfi 9226	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑚 ∈ Fin ∧ (𝐴 ∩ 𝑚) ⊆ 𝑚) → (𝐴 ∩ 𝑚) ∈ Fin)
199	197, 84, 198	sylancl 598	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → (𝐴 ∩ 𝑚) ∈ Fin)
200		abrexfi 9379	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∩ 𝑚) ∈ Fin → {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ∈ Fin)
201	199, 200	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ∈ Fin)
202		elfir 9444	. . . . . . . . . . . . . . . . . 18 ⊢ ((({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ∈ V ∧ ({𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ⊆ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅ ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ∈ Fin)) → ∩ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
203	150, 195, 196, 201, 202	syl13anc 1400	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → ∩ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
204	120, 203	eqeltrid 2868	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
205		elssuni 4904	. . . . . . . . . . . . . . . 16 ⊢ (∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ ∪ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
206	204, 205	syl 18	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ ∪ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
207		fiuni 9457	. . . . . . . . . . . . . . . . . 18 ⊢ (({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ∈ V → ∪ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) = ∪ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
208	139, 207	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ∪ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) = ∪ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
209	116	pwid 4584	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑋 ∈ 𝒫 𝑋
210	209	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝑋 ∈ 𝒫 𝑋)
211	210	snssd 4749	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → {𝑋} ⊆ 𝒫 𝑋)
212	1	ptuni2 23950	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) = ∪ 𝐵)
213	10, 212	eqtrid 2810	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝑋 = ∪ 𝐵)
214		eqimss2 3972	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑋 = ∪ 𝐵 → ∪ 𝐵 ⊆ 𝑋)
215	213, 214	syl 18	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ∪ 𝐵 ⊆ 𝑋)
216		sspwuni 5065	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐵 ⊆ 𝒫 𝑋 ↔ ∪ 𝐵 ⊆ 𝑋)
217	215, 216	sylibr 237	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝐵 ⊆ 𝒫 𝑋)
218	136, 217	sstrd 3923	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) ⊆ 𝒫 𝑋)
219	211, 218	unssd 4193	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ⊆ 𝒫 𝑋)
220		sspwuni 5065	. . . . . . . . . . . . . . . . . . 19 ⊢ (({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ⊆ 𝒫 𝑋 ↔ ∪ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ⊆ 𝑋)
221	219, 220	sylib 221	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ∪ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ⊆ 𝑋)
222		elssuni 4904	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑋 ∈ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) → 𝑋 ⊆ ∪ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))
223	145, 222	mp1i 14	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝑋 ⊆ ∪ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))
224	221, 223	eqssd 3930	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ∪ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) = 𝑋)
225	208, 224	eqtr3d 2800	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ∪ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))) = 𝑋)
226	225	ad3antrrr 743	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → ∪ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))) = 𝑋)
227	206, 226	sseqtrd 3949	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ 𝑋)
228	227, 52	sylib 221	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
229	228, 204	eqeltrd 2864	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
230	149, 229	pm2.61dane 3046	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
231	110, 230	eqeltrd 2864	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
232	231	rexlimdvaa 3168	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) → (∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))))
233	232	impr 460	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ ((ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦)) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
234	3, 233	sylan2b 606	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
235		eleq1 2852	. . . . . . 7 ⊢ (𝑠 = X𝑦 ∈ 𝐴 (ℎ‘𝑦) → (𝑠 ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))) ↔ X𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))))
236	234, 235	syl5ibrcom 250	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → (𝑠 = X𝑦 ∈ 𝐴 (ℎ‘𝑦) → 𝑠 ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))))
237	236	expimpd 459	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (((ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑠 = X𝑦 ∈ 𝐴 (ℎ‘𝑦)) → 𝑠 ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))))
238	237	exlimdv 1968	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (∃ℎ((ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑠 = X𝑦 ∈ 𝐴 (ℎ‘𝑦)) → 𝑠 ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))))
239	2, 238	biimtrid 245	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (𝑠 ∈ 𝐵 → 𝑠 ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))))
240	239	ssrdv 3919	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝐵 ⊆ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
241	1	ptbasid 23949	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) ∈ 𝐵)
242	10, 241	eqeltrid 2868	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝑋 ∈ 𝐵)
243	242	snssd 4749	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → {𝑋} ⊆ 𝐵)
244	243, 136	unssd 4193	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ⊆ 𝐵)
245		fiss 9453	. . . 4 ⊢ ((𝐵 ∈ TopBases ∧ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ⊆ 𝐵) → (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))) ⊆ (fi‘𝐵))
246	130, 244, 245	syl2anc 596	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))) ⊆ (fi‘𝐵))
247	1	ptbasin2 23952	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (fi‘𝐵) = 𝐵)
248	246, 247	sseqtrd 3949	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))) ⊆ 𝐵)
249	240, 248	eqssd 3930	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝐵 = (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∃wex 1812 ∈ wcel 2147 {cab 2741 ≠ wne 2959 ∀wral 3080 ∃wrex 3090 Vcvv 3454 ⊆ wss 3900 ∖ cdif 4048 ∩ cin 4092 ∪ cun 4152 ∅c0 4281 ifcif 4485 𝒫 cpw 4560 {csn 4588 ⟨cop 4840 ∪ cuni 4872 ∩ cint 4912 ∪ ciun 4956 ∩ ciin 4957 ↦ cmpt 5192 × cxp 5656 ^◡ccnv 5657 dom cdm 5658 ran crn 5659 “ cima 5661 Fn wfn 6561 ⟶wf 6562 ‘cfv 6566 (class class class)co 7451 ∈ cmpo 7453 Xcixp 8963 Fincfn 9011 ficfi 9439 Topctop 23266 TopBasesctb 23318

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5238 ax-sep 5255 ax-nul 5266 ax-pow 5334 ax-pr 5398 ax-un 7783

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-ral 3081 df-rex 3091 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4841 df-uni 4873 df-int 4913 df-iun 4958 df-iin 4959 df-br 5109 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-we 5613 df-xp 5664 df-rel 5665 df-cnv 5666 df-co 5667 df-dm 5668 df-rn 5669 df-res 5670 df-ima 5671 df-ord 6391 df-on 6392 df-lim 6393 df-suc 6394 df-iota 6520 df-fun 6568 df-fn 6569 df-f 6570 df-f1 6571 df-fo 6572 df-f1o 6573 df-fv 6574 df-ov 7454 df-oprab 7455 df-mpo 7456 df-om 7912 df-1st 8035 df-2nd 8036 df-1o 8514 df-2o 8515 df-ixp 8964 df-en 9012 df-dom 9013 df-fin 9015 df-fi 9440 df-top 23267 df-bases 23319

This theorem is used by: ptval2 23975 xkoptsub 24028 ptcmplem1 24426 prdsxmslem2 24903

W3C validator