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 22183

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 22174	. . . 4 ⊢ (𝑠 ∈ 𝐵 ↔ ∃ℎ((ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑠 = X𝑦 ∈ 𝐴 (ℎ‘𝑦)))
3		df-3an 1085	. . . . . . . 8 ⊢ ((ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦)) ↔ ((ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦)) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦)))
4		simprr 771	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))
5		disjdif2 4428	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∩ 𝑚) = ∅ → (𝐴 ∖ 𝑚) = 𝐴)
6	5	raleqdv 3416	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∩ 𝑚) = ∅ → (∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦) ↔ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) = ∪ (𝐹‘𝑦)))
7	6	biimpac 481	. . . . . . . . . . . . . . . 16 ⊢ ((∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦) ∧ (𝐴 ∩ 𝑚) = ∅) → ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) = ∪ (𝐹‘𝑦))
8		ixpeq2 8469	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑦 ∈ 𝐴 (ℎ‘𝑦) = ∪ (𝐹‘𝑦) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) = X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦))
9	7, 8	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦) ∧ (𝐴 ∩ 𝑚) = ∅) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) = X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦))
10		ptbasfi.2	. . . . . . . . . . . . . . . 16 ⊢ 𝑋 = X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛)
11		fveq2 6665	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑦 → (𝐹‘𝑛) = (𝐹‘𝑦))
12	11	unieqd 4842	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑦 → ∪ (𝐹‘𝑛) = ∪ (𝐹‘𝑦))
13	12	cbvixpv 8473	. . . . . . . . . . . . . . . 16 ⊢ X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) = X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦)
14	10, 13	eqtri 2844	. . . . . . . . . . . . . . 15 ⊢ 𝑋 = X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦)
15	9, 14	syl6eqr 2874	. . . . . . . . . . . . . 14 ⊢ ((∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦) ∧ (𝐴 ∩ 𝑚) = ∅) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) = 𝑋)
16	4, 15	sylan 582	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) = ∅) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) = 𝑋)
17		ssv 3991	. . . . . . . . . . . . . . . 16 ⊢ 𝑋 ⊆ V
18		iineq1 4929	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∩ 𝑚) = ∅ → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) = ∩ 𝑛 ∈ ∅ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
19		0iin 4980	. . . . . . . . . . . . . . . . 17 ⊢ ∩ 𝑛 ∈ ∅ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) = V
20	18, 19	syl6eq 2872	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∩ 𝑚) = ∅ → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) = V)
21	17, 20	sseqtrrid 4020	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∩ 𝑚) = ∅ → 𝑋 ⊆ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
22	21	adantl 484	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) = ∅) → 𝑋 ⊆ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
23		df-ss 3952	. . . . . . . . . . . . . 14 ⊢ (𝑋 ⊆ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ↔ (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) = 𝑋)
24	22, 23	sylib 220	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) = ∅) → (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) = 𝑋)
25	16, 24	eqtr4d 2859	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) = ∅) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) = (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))))
26		simplll 773	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top))
27		inss1 4205	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∩ 𝑚) ⊆ 𝐴
28		simpr 487	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → 𝑛 ∈ (𝐴 ∩ 𝑚))
29	27, 28	sseldi 3965	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → 𝑛 ∈ 𝐴)
30		fveq2 6665	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑛 → (ℎ‘𝑦) = (ℎ‘𝑛))
31		fveq2 6665	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑛 → (𝐹‘𝑦) = (𝐹‘𝑛))
32	30, 31	eleq12d 2907	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑛 → ((ℎ‘𝑦) ∈ (𝐹‘𝑦) ↔ (ℎ‘𝑛) ∈ (𝐹‘𝑛)))
33		simprr 771	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) → ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))
34	33	ad2antrr 724	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))
35	32, 34, 29	rspcdva 3625	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (ℎ‘𝑛) ∈ (𝐹‘𝑛))
36	14	ptpjpre1 22173	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (𝑛 ∈ 𝐴 ∧ (ℎ‘𝑛) ∈ (𝐹‘𝑛))) → (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) = X𝑦 ∈ 𝐴 if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
37	26, 29, 35, 36	syl12anc 834	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) = X𝑦 ∈ 𝐴 if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
38	37	adantlr 713	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) = X𝑦 ∈ 𝐴 if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
39	38	iineq2dv 4937	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)X𝑦 ∈ 𝐴 if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
40		simpr 487	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → (𝐴 ∩ 𝑚) ≠ ∅)
41		cnvimass 5944	. . . . . . . . . . . . . . . . . . . 20 ⊢ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ dom (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛))
42		eqid 2821	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) = (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛))
43	42	dmmptss 6090	. . . . . . . . . . . . . . . . . . . 20 ⊢ dom (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) ⊆ 𝑋
44	41, 43	sstri 3976	. . . . . . . . . . . . . . . . . . 19 ⊢ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ 𝑋
45	44, 14	sseqtri 4003	. . . . . . . . . . . . . . . . . 18 ⊢ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦)
46	45	rgenw 3150	. . . . . . . . . . . . . . . . 17 ⊢ ∀𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦)
47		r19.2z 4440	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∩ 𝑚) ≠ ∅ ∧ ∀𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦)) → ∃𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦))
48	40, 46, 47	sylancl 588	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → ∃𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦))
49		iinss 4973	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦))
50	48, 49	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦))
51	50, 14	sseqtrrdi 4018	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ 𝑋)
52		sseqin2 4192	. . . . . . . . . . . . . 14 ⊢ (∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ 𝑋 ↔ (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
53	51, 52	sylib 220	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
54	33	ad2antrr 724	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))
55		ssralv 4033	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∩ 𝑚) ⊆ 𝐴 → (∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦) → ∀𝑦 ∈ (𝐴 ∩ 𝑚)(ℎ‘𝑦) ∈ (𝐹‘𝑦)))
56	27, 55	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦) → ∀𝑦 ∈ (𝐴 ∩ 𝑚)(ℎ‘𝑦) ∈ (𝐹‘𝑦))
57		elssuni 4861	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((ℎ‘𝑦) ∈ (𝐹‘𝑦) → (ℎ‘𝑦) ⊆ ∪ (𝐹‘𝑦))
58		iffalse 4476	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (¬ 𝑦 = 𝑛 → if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) = ∪ (𝐹‘𝑦))
59	58	sseq2d 3999	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ 𝑦 = 𝑛 → ((ℎ‘𝑦) ⊆ if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ↔ (ℎ‘𝑦) ⊆ ∪ (𝐹‘𝑦)))
60	57, 59	syl5ibrcom 249	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ℎ‘𝑦) ∈ (𝐹‘𝑦) → (¬ 𝑦 = 𝑛 → (ℎ‘𝑦) ⊆ if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦))))
61		ssid 3989	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ℎ‘𝑦) ⊆ (ℎ‘𝑦)
62		iftrue 4473	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = 𝑛 → if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) = (ℎ‘𝑛))
63	62, 30	eqtr4d 2859	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = 𝑛 → if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) = (ℎ‘𝑦))
64	61, 63	sseqtrrid 4020	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = 𝑛 → (ℎ‘𝑦) ⊆ if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
65	60, 64	pm2.61d2 183	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℎ‘𝑦) ∈ (𝐹‘𝑦) → (ℎ‘𝑦) ⊆ if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
66	65	ralrimivw 3183	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℎ‘𝑦) ∈ (𝐹‘𝑦) → ∀𝑛 ∈ (𝐴 ∩ 𝑚)(ℎ‘𝑦) ⊆ if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
67		ssiin 4972	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℎ‘𝑦) ⊆ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ↔ ∀𝑛 ∈ (𝐴 ∩ 𝑚)(ℎ‘𝑦) ⊆ if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
68	66, 67	sylibr 236	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ‘𝑦) ∈ (𝐹‘𝑦) → (ℎ‘𝑦) ⊆ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
69	68	adantl 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ (𝐴 ∩ 𝑚) ∧ (ℎ‘𝑦) ∈ (𝐹‘𝑦)) → (ℎ‘𝑦) ⊆ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
70	62	equcoms 2023	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 = 𝑦 → if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) = (ℎ‘𝑛))
71		fveq2 6665	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 = 𝑦 → (ℎ‘𝑛) = (ℎ‘𝑦))
72	70, 71	eqtrd 2856	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑦 → if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) = (ℎ‘𝑦))
73	72	sseq1d 3998	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑦 → (if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ⊆ (ℎ‘𝑦) ↔ (ℎ‘𝑦) ⊆ (ℎ‘𝑦)))
74	73	rspcev 3623	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑦 ∈ (𝐴 ∩ 𝑚) ∧ (ℎ‘𝑦) ⊆ (ℎ‘𝑦)) → ∃𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ⊆ (ℎ‘𝑦))
75	61, 74	mpan2 689	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ (𝐴 ∩ 𝑚) → ∃𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ⊆ (ℎ‘𝑦))
76		iinss 4973	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ⊆ (ℎ‘𝑦) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ⊆ (ℎ‘𝑦))
77	75, 76	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ (𝐴 ∩ 𝑚) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ⊆ (ℎ‘𝑦))
78	77	adantr 483	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ (𝐴 ∩ 𝑚) ∧ (ℎ‘𝑦) ∈ (𝐹‘𝑦)) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ⊆ (ℎ‘𝑦))
79	69, 78	eqssd 3984	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ (𝐴 ∩ 𝑚) ∧ (ℎ‘𝑦) ∈ (𝐹‘𝑦)) → (ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
80	79	ralimiaa 3159	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑦 ∈ (𝐴 ∩ 𝑚)(ℎ‘𝑦) ∈ (𝐹‘𝑦) → ∀𝑦 ∈ (𝐴 ∩ 𝑚)(ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
81	54, 56, 80	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → ∀𝑦 ∈ (𝐴 ∩ 𝑚)(ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
82		eldifn 4104	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ (𝐴 ∖ 𝑚) → ¬ 𝑦 ∈ 𝑚)
83	82	ad2antlr 725	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ∩ 𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴 ∖ 𝑚)) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → ¬ 𝑦 ∈ 𝑚)
84		inss2 4206	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐴 ∩ 𝑚) ⊆ 𝑚
85		simpr 487	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐴 ∩ 𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴 ∖ 𝑚)) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → 𝑛 ∈ (𝐴 ∩ 𝑚))
86	84, 85	sseldi 3965	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐴 ∩ 𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴 ∖ 𝑚)) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → 𝑛 ∈ 𝑚)
87		eleq1 2900	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = 𝑛 → (𝑦 ∈ 𝑚 ↔ 𝑛 ∈ 𝑚))
88	86, 87	syl5ibrcom 249	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ∩ 𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴 ∖ 𝑚)) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (𝑦 = 𝑛 → 𝑦 ∈ 𝑚))
89	83, 88	mtod 200	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∩ 𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴 ∖ 𝑚)) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → ¬ 𝑦 = 𝑛)
90	89, 58	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∩ 𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴 ∖ 𝑚)) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) = ∪ (𝐹‘𝑦))
91	90	iineq2dv 4937	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∩ 𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴 ∖ 𝑚)) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)∪ (𝐹‘𝑦))
92		iinconst 4922	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∩ 𝑚) ≠ ∅ → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)∪ (𝐹‘𝑦) = ∪ (𝐹‘𝑦))
93	92	adantr 483	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∩ 𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴 ∖ 𝑚)) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)∪ (𝐹‘𝑦) = ∪ (𝐹‘𝑦))
94	91, 93	eqtr2d 2857	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∩ 𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴 ∖ 𝑚)) → ∪ (𝐹‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
95		eqeq1 2825	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℎ‘𝑦) = ∪ (𝐹‘𝑦) → ((ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ↔ ∪ (𝐹‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦))))
96	94, 95	syl5ibrcom 249	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∩ 𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴 ∖ 𝑚)) → ((ℎ‘𝑦) = ∪ (𝐹‘𝑦) → (ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦))))
97	96	ralimdva 3177	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∩ 𝑚) ≠ ∅ → (∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦) → ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦))))
98	4, 97	mpan9 509	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
99		inundif 4427	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∩ 𝑚) ∪ (𝐴 ∖ 𝑚)) = 𝐴
100	99	raleqi 3414	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑦 ∈ ((𝐴 ∩ 𝑚) ∪ (𝐴 ∖ 𝑚))(ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ↔ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
101		ralunb 4167	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑦 ∈ ((𝐴 ∩ 𝑚) ∪ (𝐴 ∖ 𝑚))(ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ↔ (∀𝑦 ∈ (𝐴 ∩ 𝑚)(ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦))))
102	100, 101	bitr3i 279	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑦 ∈ 𝐴 (ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ↔ (∀𝑦 ∈ (𝐴 ∩ 𝑚)(ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦))))
103	81, 98, 102	sylanbrc 585	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
104		ixpeq2 8469	. . . . . . . . . . . . . . 15 ⊢ (∀𝑦 ∈ 𝐴 (ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) = X𝑦 ∈ 𝐴 ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
105	103, 104	syl 17	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) = X𝑦 ∈ 𝐴 ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
106		ixpiin 8482	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∩ 𝑚) ≠ ∅ → X𝑦 ∈ 𝐴 ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)X𝑦 ∈ 𝐴 if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
107	106	adantl 484	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → X𝑦 ∈ 𝐴 ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)X𝑦 ∈ 𝐴 if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
108	105, 107	eqtrd 2856	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)X𝑦 ∈ 𝐴 if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
109	39, 53, 108	3eqtr4rd 2867	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) = (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))))
110	25, 109	pm2.61dane 3104	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) = (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))))
111		ixpexg 8480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∀𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) ∈ V → X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) ∈ V)
112		fvex 6678	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐹‘𝑛) ∈ V
113	112	uniex 7461	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ∪ (𝐹‘𝑛) ∈ V
114	113	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 ∈ 𝐴 → ∪ (𝐹‘𝑛) ∈ V)
115	111, 114	mprg 3152	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) ∈ V
116	10, 115	eqeltri 2909	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑋 ∈ V
117	116	mptex 6980	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) ∈ V
118	117	cnvex 7624	. . . . . . . . . . . . . . . . . . . 20 ⊢ ^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) ∈ V
119	118	imaex 7615	. . . . . . . . . . . . . . . . . . 19 ⊢ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ∈ V
120	119	dfiin2 4952	. . . . . . . . . . . . . . . . . 18 ⊢ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) = ∩ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))}
121		inteq 4872	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} = ∅ → ∩ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} = ∩ ∅)
122	120, 121	syl5eq 2868	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} = ∅ → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) = ∩ ∅)
123		int0 4883	. . . . . . . . . . . . . . . . 17 ⊢ ∩ ∅ = V
124	122, 123	syl6eq 2872	. . . . . . . . . . . . . . . 16 ⊢ ({𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} = ∅ → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) = V)
125	124	ineq2d 4189	. . . . . . . . . . . . . . 15 ⊢ ({𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} = ∅ → (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) = (𝑋 ∩ V))
126		inv1 4348	. . . . . . . . . . . . . . 15 ⊢ (𝑋 ∩ V) = 𝑋
127	125, 126	syl6eq 2872	. . . . . . . . . . . . . 14 ⊢ ({𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} = ∅ → (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) = 𝑋)
128	127	adantl 484	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} = ∅) → (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) = 𝑋)
129		snex 5324	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑋} ∈ V
130	1	ptbas 22181	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝐵 ∈ TopBases)
131	1, 10	ptpjpre2 22182	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (𝑘 ∈ 𝐴 ∧ 𝑢 ∈ (𝐹‘𝑘))) → (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝐵)
132	131	ralrimivva 3191	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ∀𝑘 ∈ 𝐴 ∀𝑢 ∈ (𝐹‘𝑘)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝐵)
133		eqid 2821	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) = (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))
134	133	fmpox 7759	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑘 ∈ 𝐴 ∀𝑢 ∈ (𝐹‘𝑘)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝐵 ↔ (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)):∪ 𝑘 ∈ 𝐴 ({𝑘} × (𝐹‘𝑘))⟶𝐵)
135	132, 134	sylib 220	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)):∪ 𝑘 ∈ 𝐴 ({𝑘} × (𝐹‘𝑘))⟶𝐵)
136	135	frnd 6516	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) ⊆ 𝐵)
137	130, 136	ssexd 5221	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) ∈ V)
138		unexg 7466	. . . . . . . . . . . . . . . . . 18 ⊢ (({𝑋} ∈ V ∧ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) ∈ V) → ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ∈ V)
139	129, 137, 138	sylancr 589	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ∈ V)
140		ssfii 8877	. . . . . . . . . . . . . . . . 17 ⊢ (({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ∈ V → ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ⊆ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
141	139, 140	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ⊆ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
142	141	ad2antrr 724	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ⊆ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
143		ssun1 4148	. . . . . . . . . . . . . . . . 17 ⊢ {𝑋} ⊆ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))
144	116	snss 4712	. . . . . . . . . . . . . . . . 17 ⊢ (𝑋 ∈ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ↔ {𝑋} ⊆ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))
145	143, 144	mpbir 233	. . . . . . . . . . . . . . . 16 ⊢ 𝑋 ∈ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))
146	145	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → 𝑋 ∈ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))
147	142, 146	sseldd 3968	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → 𝑋 ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
148	147	adantr 483	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} = ∅) → 𝑋 ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
149	128, 148	eqeltrd 2913	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} = ∅) → (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
150	139	ad3antrrr 728	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ∈ V)
151		nfv 1911	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑛(((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦)))
152		nfcv 2977	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑛𝐴
153		nfcv 2977	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑛(𝐹‘𝑘)
154		nfixp1 8476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ Ⅎ𝑛X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛)
155	10, 154	nfcxfr 2975	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ Ⅎ𝑛𝑋
156		nfcv 2977	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ Ⅎ𝑛(𝑤‘𝑘)
157	155, 156	nfmpt 5156	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ Ⅎ𝑛(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘))
158	157	nfcnv 5744	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑛^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘))
159		nfcv 2977	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑛𝑢
160	158, 159	nfima 5932	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑛(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)
161	152, 153, 160	nfmpo 7230	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑛(𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))
162	161	nfrn 5819	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑛ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))
163	162	nfcri 2971	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑛 𝑧 ∈ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))
164		df-ov 7153	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑛(𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))(ℎ‘𝑛)) = ((𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))‘⟨𝑛, (ℎ‘𝑛)⟩)
165	119	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ∈ V)
166		fveq2 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑘 = 𝑛 → (𝑤‘𝑘) = (𝑤‘𝑛))
167	166	mpteq2dv 5155	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑘 = 𝑛 → (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) = (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)))
168	167	cnveqd 5741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑘 = 𝑛 → ^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) = ^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)))
169	168	imaeq1d 5923	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑘 = 𝑛 → (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ 𝑢))
170		imaeq2 5920	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑢 = (ℎ‘𝑛) → (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ 𝑢) = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
171	169, 170	sylan9eq 2876	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑘 = 𝑛 ∧ 𝑢 = (ℎ‘𝑛)) → (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
172		fveq2 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑘 = 𝑛 → (𝐹‘𝑘) = (𝐹‘𝑛))
173	171, 172, 133	ovmpox 7297	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑛 ∈ 𝐴 ∧ (ℎ‘𝑛) ∈ (𝐹‘𝑛) ∧ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ∈ V) → (𝑛(𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))(ℎ‘𝑛)) = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
174	29, 35, 165, 173	syl3anc 1367	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (𝑛(𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))(ℎ‘𝑛)) = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
175	164, 174	syl5eqr 2870	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → ((𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))‘⟨𝑛, (ℎ‘𝑛)⟩) = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
176	135	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)):∪ 𝑘 ∈ 𝐴 ({𝑘} × (𝐹‘𝑘))⟶𝐵)
177	176	ffnd 6510	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) Fn ∪ 𝑘 ∈ 𝐴 ({𝑘} × (𝐹‘𝑘)))
178		opeliunxp 5614	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (⟨𝑛, (ℎ‘𝑛)⟩ ∈ ∪ 𝑛 ∈ 𝐴 ({𝑛} × (𝐹‘𝑛)) ↔ (𝑛 ∈ 𝐴 ∧ (ℎ‘𝑛) ∈ (𝐹‘𝑛)))
179	29, 35, 178	sylanbrc 585	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → ⟨𝑛, (ℎ‘𝑛)⟩ ∈ ∪ 𝑛 ∈ 𝐴 ({𝑛} × (𝐹‘𝑛)))
180		sneq 4571	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑛 = 𝑘 → {𝑛} = {𝑘})
181		fveq2 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑛 = 𝑘 → (𝐹‘𝑛) = (𝐹‘𝑘))
182	180, 181	xpeq12d 5581	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑛 = 𝑘 → ({𝑛} × (𝐹‘𝑛)) = ({𝑘} × (𝐹‘𝑘)))
183	182	cbviunv 4958	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ∪ 𝑛 ∈ 𝐴 ({𝑛} × (𝐹‘𝑛)) = ∪ 𝑘 ∈ 𝐴 ({𝑘} × (𝐹‘𝑘))
184	179, 183	eleqtrdi 2923	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → ⟨𝑛, (ℎ‘𝑛)⟩ ∈ ∪ 𝑘 ∈ 𝐴 ({𝑘} × (𝐹‘𝑘)))
185		fnfvelrn 6843	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) Fn ∪ 𝑘 ∈ 𝐴 ({𝑘} × (𝐹‘𝑘)) ∧ ⟨𝑛, (ℎ‘𝑛)⟩ ∈ ∪ 𝑘 ∈ 𝐴 ({𝑘} × (𝐹‘𝑘))) → ((𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))‘⟨𝑛, (ℎ‘𝑛)⟩) ∈ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))
186	177, 184, 185	syl2anc 586	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → ((𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))‘⟨𝑛, (ℎ‘𝑛)⟩) ∈ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))
187	175, 186	eqeltrrd 2914	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ∈ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))
188		eleq1 2900	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) → (𝑧 ∈ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) ↔ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ∈ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))
189	187, 188	syl5ibrcom 249	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) → 𝑧 ∈ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))
190	189	ex 415	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → (𝑛 ∈ (𝐴 ∩ 𝑚) → (𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) → 𝑧 ∈ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
191	151, 163, 190	rexlimd 3317	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → (∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) → 𝑧 ∈ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))
192	191	abssdv 4045	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ⊆ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))
193		ssun2 4149	. . . . . . . . . . . . . . . . . . . 20 ⊢ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) ⊆ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))
194	192, 193	sstrdi 3979	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ⊆ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))
195	194	adantr 483	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ⊆ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))
196		simpr 487	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅)
197		simplrl 775	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → 𝑚 ∈ Fin)
198		ssfi 8732	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑚 ∈ Fin ∧ (𝐴 ∩ 𝑚) ⊆ 𝑚) → (𝐴 ∩ 𝑚) ∈ Fin)
199	197, 84, 198	sylancl 588	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → (𝐴 ∩ 𝑚) ∈ Fin)
200		abrexfi 8818	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∩ 𝑚) ∈ Fin → {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ∈ Fin)
201	199, 200	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ∈ Fin)
202		elfir 8873	. . . . . . . . . . . . . . . . . 18 ⊢ ((({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ∈ V ∧ ({𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ⊆ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅ ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ∈ Fin)) → ∩ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
203	150, 195, 196, 201, 202	syl13anc 1368	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → ∩ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
204	120, 203	eqeltrid 2917	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
205		elssuni 4861	. . . . . . . . . . . . . . . 16 ⊢ (∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ ∪ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
206	204, 205	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ ∪ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
207		fiuni 8886	. . . . . . . . . . . . . . . . . 18 ⊢ (({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ∈ V → ∪ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) = ∪ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
208	139, 207	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ∪ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) = ∪ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
209	116	pwid 4558	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑋 ∈ 𝒫 𝑋
210	209	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝑋 ∈ 𝒫 𝑋)
211	210	snssd 4736	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → {𝑋} ⊆ 𝒫 𝑋)
212	1	ptuni2 22178	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) = ∪ 𝐵)
213	10, 212	syl5eq 2868	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝑋 = ∪ 𝐵)
214		eqimss2 4024	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑋 = ∪ 𝐵 → ∪ 𝐵 ⊆ 𝑋)
215	213, 214	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ∪ 𝐵 ⊆ 𝑋)
216		sspwuni 5015	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐵 ⊆ 𝒫 𝑋 ↔ ∪ 𝐵 ⊆ 𝑋)
217	215, 216	sylibr 236	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝐵 ⊆ 𝒫 𝑋)
218	136, 217	sstrd 3977	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) ⊆ 𝒫 𝑋)
219	211, 218	unssd 4162	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ⊆ 𝒫 𝑋)
220		sspwuni 5015	. . . . . . . . . . . . . . . . . . 19 ⊢ (({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ⊆ 𝒫 𝑋 ↔ ∪ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ⊆ 𝑋)
221	219, 220	sylib 220	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ∪ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ⊆ 𝑋)
222		elssuni 4861	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑋 ∈ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) → 𝑋 ⊆ ∪ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))
223	145, 222	mp1i 13	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝑋 ⊆ ∪ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))
224	221, 223	eqssd 3984	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ∪ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) = 𝑋)
225	208, 224	eqtr3d 2858	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ∪ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))) = 𝑋)
226	225	ad3antrrr 728	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → ∪ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))) = 𝑋)
227	206, 226	sseqtrd 4007	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ 𝑋)
228	227, 52	sylib 220	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
229	228, 204	eqeltrd 2913	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
230	149, 229	pm2.61dane 3104	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
231	110, 230	eqeltrd 2913	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
232	231	rexlimdvaa 3285	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) → (∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))))
233	232	impr 457	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ ((ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦)) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
234	3, 233	sylan2b 595	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
235		eleq1 2900	. . . . . . 7 ⊢ (𝑠 = X𝑦 ∈ 𝐴 (ℎ‘𝑦) → (𝑠 ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))) ↔ X𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))))
236	234, 235	syl5ibrcom 249	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → (𝑠 = X𝑦 ∈ 𝐴 (ℎ‘𝑦) → 𝑠 ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))))
237	236	expimpd 456	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (((ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑠 = X𝑦 ∈ 𝐴 (ℎ‘𝑦)) → 𝑠 ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))))
238	237	exlimdv 1930	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (∃ℎ((ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑠 = X𝑦 ∈ 𝐴 (ℎ‘𝑦)) → 𝑠 ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))))
239	2, 238	syl5bi 244	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (𝑠 ∈ 𝐵 → 𝑠 ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))))
240	239	ssrdv 3973	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝐵 ⊆ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
241	1	ptbasid 22177	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) ∈ 𝐵)
242	10, 241	eqeltrid 2917	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝑋 ∈ 𝐵)
243	242	snssd 4736	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → {𝑋} ⊆ 𝐵)
244	243, 136	unssd 4162	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ⊆ 𝐵)
245		fiss 8882	. . . 4 ⊢ ((𝐵 ∈ TopBases ∧ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ⊆ 𝐵) → (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))) ⊆ (fi‘𝐵))
246	130, 244, 245	syl2anc 586	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))) ⊆ (fi‘𝐵))
247	1	ptbasin2 22180	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (fi‘𝐵) = 𝐵)
248	246, 247	sseqtrd 4007	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))) ⊆ 𝐵)
249	240, 248	eqssd 3984	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝐵 = (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 398 ∧ w3a 1083 = wceq 1533 ∃wex 1776 ∈ wcel 2110 {cab 2799 ≠ wne 3016 ∀wral 3138 ∃wrex 3139 Vcvv 3495 ∖ cdif 3933 ∪ cun 3934 ∩ cin 3935 ⊆ wss 3936 ∅c0 4291 ifcif 4467 𝒫 cpw 4539 {csn 4561 ⟨cop 4567 ∪ cuni 4832 ∩ cint 4869 ∪ ciun 4912 ∩ ciin 4913 ↦ cmpt 5139 × cxp 5548 ^◡ccnv 5549 dom cdm 5550 ran crn 5551 “ cima 5553 Fn wfn 6345 ⟶wf 6346 ‘cfv 6350 (class class class)co 7150 ∈ cmpo 7152 Xcixp 8455 Fincfn 8503 ficfi 8868 Topctop 21495 TopBasesctb 21547

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2156 ax-12 2172 ax-ext 2793 ax-rep 5183 ax-sep 5196 ax-nul 5203 ax-pow 5259 ax-pr 5322 ax-un 7455

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-mo 2618 df-eu 2650 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 3497 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 4562 df-pr 4564 df-tp 4566 df-op 4568 df-uni 4833 df-int 4870 df-iun 4914 df-iin 4915 df-br 5060 df-opab 5122 df-mpt 5140 df-tr 5166 df-id 5455 df-eprel 5460 df-po 5469 df-so 5470 df-fr 5509 df-we 5511 df-xp 5556 df-rel 5557 df-cnv 5558 df-co 5559 df-dm 5560 df-rn 5561 df-res 5562 df-ima 5563 df-pred 6143 df-ord 6189 df-on 6190 df-lim 6191 df-suc 6192 df-iota 6309 df-fun 6352 df-fn 6353 df-f 6354 df-f1 6355 df-fo 6356 df-f1o 6357 df-fv 6358 df-ov 7153 df-oprab 7154 df-mpo 7155 df-om 7575 df-1st 7683 df-2nd 7684 df-wrecs 7941 df-recs 8002 df-rdg 8040 df-1o 8096 df-oadd 8100 df-er 8283 df-ixp 8456 df-en 8504 df-dom 8505 df-fin 8507 df-fi 8869 df-top 21496 df-bases 21548

This theorem is referenced by: ptval2 22203 xkoptsub 22256 ptcmplem1 22654 prdsxmslem2 23133

W3C validator