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 22932

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 22923	. . . 4 ⊢ (𝑠 ∈ 𝐵 ↔ ∃ℎ((ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑠 = X𝑦 ∈ 𝐴 (ℎ‘𝑦)))
3		df-3an 1089	. . . . . . . 8 ⊢ ((ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦)) ↔ ((ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦)) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦)))
4		simprr 771	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))
5		disjdif2 4439	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∩ 𝑚) = ∅ → (𝐴 ∖ 𝑚) = 𝐴)
6	5	raleqdv 3313	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∩ 𝑚) = ∅ → (∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦) ↔ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) = ∪ (𝐹‘𝑦)))
7	6	biimpac 479	. . . . . . . . . . . . . . . 16 ⊢ ((∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦) ∧ (𝐴 ∩ 𝑚) = ∅) → ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) = ∪ (𝐹‘𝑦))
8		ixpeq2 8849	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑦 ∈ 𝐴 (ℎ‘𝑦) = ∪ (𝐹‘𝑦) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) = X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦))
9	7, 8	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦) ∧ (𝐴 ∩ 𝑚) = ∅) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) = X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦))
10		ptbasfi.2	. . . . . . . . . . . . . . . 16 ⊢ 𝑋 = X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛)
11		fveq2 6842	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑦 → (𝐹‘𝑛) = (𝐹‘𝑦))
12	11	unieqd 4879	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑦 → ∪ (𝐹‘𝑛) = ∪ (𝐹‘𝑦))
13	12	cbvixpv 8853	. . . . . . . . . . . . . . . 16 ⊢ X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) = X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦)
14	10, 13	eqtri 2764	. . . . . . . . . . . . . . 15 ⊢ 𝑋 = X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦)
15	9, 14	eqtr4di 2794	. . . . . . . . . . . . . 14 ⊢ ((∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦) ∧ (𝐴 ∩ 𝑚) = ∅) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) = 𝑋)
16	4, 15	sylan 580	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) = ∅) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) = 𝑋)
17		ssv 3968	. . . . . . . . . . . . . . . 16 ⊢ 𝑋 ⊆ V
18		iineq1 4971	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∩ 𝑚) = ∅ → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) = ∩ 𝑛 ∈ ∅ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
19		0iin 5024	. . . . . . . . . . . . . . . . 17 ⊢ ∩ 𝑛 ∈ ∅ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) = V
20	18, 19	eqtrdi 2792	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∩ 𝑚) = ∅ → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) = V)
21	17, 20	sseqtrrid 3997	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∩ 𝑚) = ∅ → 𝑋 ⊆ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
22	21	adantl 482	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) = ∅) → 𝑋 ⊆ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
23		df-ss 3927	. . . . . . . . . . . . . 14 ⊢ (𝑋 ⊆ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ↔ (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) = 𝑋)
24	22, 23	sylib 217	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) = ∅) → (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) = 𝑋)
25	16, 24	eqtr4d 2779	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) = ∅) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) = (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))))
26		simplll 773	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top))
27		inss1 4188	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∩ 𝑚) ⊆ 𝐴
28		simpr 485	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → 𝑛 ∈ (𝐴 ∩ 𝑚))
29	27, 28	sselid 3942	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → 𝑛 ∈ 𝐴)
30		fveq2 6842	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑛 → (ℎ‘𝑦) = (ℎ‘𝑛))
31		fveq2 6842	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑛 → (𝐹‘𝑦) = (𝐹‘𝑛))
32	30, 31	eleq12d 2832	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 = 𝑛 → ((ℎ‘𝑦) ∈ (𝐹‘𝑦) ↔ (ℎ‘𝑛) ∈ (𝐹‘𝑛)))
33		simprr 771	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) → ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))
34	33	ad2antrr 724	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))
35	32, 34, 29	rspcdva 3582	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (ℎ‘𝑛) ∈ (𝐹‘𝑛))
36	14	ptpjpre1 22922	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (𝑛 ∈ 𝐴 ∧ (ℎ‘𝑛) ∈ (𝐹‘𝑛))) → (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) = X𝑦 ∈ 𝐴 if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
37	26, 29, 35, 36	syl12anc 835	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) = X𝑦 ∈ 𝐴 if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
38	37	adantlr 713	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) = X𝑦 ∈ 𝐴 if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
39	38	iineq2dv 4979	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)X𝑦 ∈ 𝐴 if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
40		simpr 485	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → (𝐴 ∩ 𝑚) ≠ ∅)
41		cnvimass 6033	. . . . . . . . . . . . . . . . . . . 20 ⊢ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ dom (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛))
42		eqid 2736	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) = (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛))
43	42	dmmptss 6193	. . . . . . . . . . . . . . . . . . . 20 ⊢ dom (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) ⊆ 𝑋
44	41, 43	sstri 3953	. . . . . . . . . . . . . . . . . . 19 ⊢ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ 𝑋
45	44, 14	sseqtri 3980	. . . . . . . . . . . . . . . . . 18 ⊢ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦)
46	45	rgenw 3068	. . . . . . . . . . . . . . . . 17 ⊢ ∀𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦)
47		r19.2z 4452	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∩ 𝑚) ≠ ∅ ∧ ∀𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦)) → ∃𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦))
48	40, 46, 47	sylancl 586	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → ∃𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦))
49		iinss 5016	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦))
50	48, 49	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦))
51	50, 14	sseqtrrdi 3995	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ 𝑋)
52		sseqin2 4175	. . . . . . . . . . . . . 14 ⊢ (∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ 𝑋 ↔ (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
53	51, 52	sylib 217	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
54	33	ad2antrr 724	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))
55		ssralv 4010	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∩ 𝑚) ⊆ 𝐴 → (∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦) → ∀𝑦 ∈ (𝐴 ∩ 𝑚)(ℎ‘𝑦) ∈ (𝐹‘𝑦)))
56	27, 55	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦) → ∀𝑦 ∈ (𝐴 ∩ 𝑚)(ℎ‘𝑦) ∈ (𝐹‘𝑦))
57		elssuni 4898	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((ℎ‘𝑦) ∈ (𝐹‘𝑦) → (ℎ‘𝑦) ⊆ ∪ (𝐹‘𝑦))
58		iffalse 4495	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (¬ 𝑦 = 𝑛 → if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) = ∪ (𝐹‘𝑦))
59	58	sseq2d 3976	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ 𝑦 = 𝑛 → ((ℎ‘𝑦) ⊆ if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ↔ (ℎ‘𝑦) ⊆ ∪ (𝐹‘𝑦)))
60	57, 59	syl5ibrcom 246	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ℎ‘𝑦) ∈ (𝐹‘𝑦) → (¬ 𝑦 = 𝑛 → (ℎ‘𝑦) ⊆ if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦))))
61		ssid 3966	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ℎ‘𝑦) ⊆ (ℎ‘𝑦)
62		iftrue 4492	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = 𝑛 → if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) = (ℎ‘𝑛))
63	62, 30	eqtr4d 2779	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = 𝑛 → if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) = (ℎ‘𝑦))
64	61, 63	sseqtrrid 3997	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = 𝑛 → (ℎ‘𝑦) ⊆ if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
65	60, 64	pm2.61d2 181	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℎ‘𝑦) ∈ (𝐹‘𝑦) → (ℎ‘𝑦) ⊆ if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
66	65	ralrimivw 3147	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℎ‘𝑦) ∈ (𝐹‘𝑦) → ∀𝑛 ∈ (𝐴 ∩ 𝑚)(ℎ‘𝑦) ⊆ if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
67		ssiin 5015	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℎ‘𝑦) ⊆ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ↔ ∀𝑛 ∈ (𝐴 ∩ 𝑚)(ℎ‘𝑦) ⊆ if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
68	66, 67	sylibr 233	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ‘𝑦) ∈ (𝐹‘𝑦) → (ℎ‘𝑦) ⊆ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
69	68	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ (𝐴 ∩ 𝑚) ∧ (ℎ‘𝑦) ∈ (𝐹‘𝑦)) → (ℎ‘𝑦) ⊆ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
70	62	equcoms 2023	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 = 𝑦 → if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) = (ℎ‘𝑛))
71		fveq2 6842	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 = 𝑦 → (ℎ‘𝑛) = (ℎ‘𝑦))
72	70, 71	eqtrd 2776	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑦 → if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) = (ℎ‘𝑦))
73	72	sseq1d 3975	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑦 → (if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ⊆ (ℎ‘𝑦) ↔ (ℎ‘𝑦) ⊆ (ℎ‘𝑦)))
74	73	rspcev 3581	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑦 ∈ (𝐴 ∩ 𝑚) ∧ (ℎ‘𝑦) ⊆ (ℎ‘𝑦)) → ∃𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ⊆ (ℎ‘𝑦))
75	61, 74	mpan2 689	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ (𝐴 ∩ 𝑚) → ∃𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ⊆ (ℎ‘𝑦))
76		iinss 5016	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ⊆ (ℎ‘𝑦) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ⊆ (ℎ‘𝑦))
77	75, 76	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ (𝐴 ∩ 𝑚) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ⊆ (ℎ‘𝑦))
78	77	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ (𝐴 ∩ 𝑚) ∧ (ℎ‘𝑦) ∈ (𝐹‘𝑦)) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ⊆ (ℎ‘𝑦))
79	69, 78	eqssd 3961	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ (𝐴 ∩ 𝑚) ∧ (ℎ‘𝑦) ∈ (𝐹‘𝑦)) → (ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
80	79	ralimiaa 3085	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑦 ∈ (𝐴 ∩ 𝑚)(ℎ‘𝑦) ∈ (𝐹‘𝑦) → ∀𝑦 ∈ (𝐴 ∩ 𝑚)(ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
81	54, 56, 80	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → ∀𝑦 ∈ (𝐴 ∩ 𝑚)(ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
82		eldifn 4087	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ (𝐴 ∖ 𝑚) → ¬ 𝑦 ∈ 𝑚)
83	82	ad2antlr 725	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ∩ 𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴 ∖ 𝑚)) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → ¬ 𝑦 ∈ 𝑚)
84		inss2 4189	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐴 ∩ 𝑚) ⊆ 𝑚
85		simpr 485	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐴 ∩ 𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴 ∖ 𝑚)) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → 𝑛 ∈ (𝐴 ∩ 𝑚))
86	84, 85	sselid 3942	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐴 ∩ 𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴 ∖ 𝑚)) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → 𝑛 ∈ 𝑚)
87		eleq1 2825	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = 𝑛 → (𝑦 ∈ 𝑚 ↔ 𝑛 ∈ 𝑚))
88	86, 87	syl5ibrcom 246	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ∩ 𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴 ∖ 𝑚)) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (𝑦 = 𝑛 → 𝑦 ∈ 𝑚))
89	83, 88	mtod 197	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∩ 𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴 ∖ 𝑚)) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → ¬ 𝑦 = 𝑛)
90	89, 58	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∩ 𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴 ∖ 𝑚)) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) = ∪ (𝐹‘𝑦))
91	90	iineq2dv 4979	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∩ 𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴 ∖ 𝑚)) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)∪ (𝐹‘𝑦))
92		iinconst 4964	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∩ 𝑚) ≠ ∅ → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)∪ (𝐹‘𝑦) = ∪ (𝐹‘𝑦))
93	92	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∩ 𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴 ∖ 𝑚)) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)∪ (𝐹‘𝑦) = ∪ (𝐹‘𝑦))
94	91, 93	eqtr2d 2777	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∩ 𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴 ∖ 𝑚)) → ∪ (𝐹‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
95		eqeq1 2740	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℎ‘𝑦) = ∪ (𝐹‘𝑦) → ((ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ↔ ∪ (𝐹‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦))))
96	94, 95	syl5ibrcom 246	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∩ 𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴 ∖ 𝑚)) → ((ℎ‘𝑦) = ∪ (𝐹‘𝑦) → (ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦))))
97	96	ralimdva 3164	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∩ 𝑚) ≠ ∅ → (∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦) → ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦))))
98	4, 97	mpan9 507	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
99		inundif 4438	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∩ 𝑚) ∪ (𝐴 ∖ 𝑚)) = 𝐴
100	99	raleqi 3311	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑦 ∈ ((𝐴 ∩ 𝑚) ∪ (𝐴 ∖ 𝑚))(ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ↔ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
101		ralunb 4151	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑦 ∈ ((𝐴 ∩ 𝑚) ∪ (𝐴 ∖ 𝑚))(ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ↔ (∀𝑦 ∈ (𝐴 ∩ 𝑚)(ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦))))
102	100, 101	bitr3i 276	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑦 ∈ 𝐴 (ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ↔ (∀𝑦 ∈ (𝐴 ∩ 𝑚)(ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦))))
103	81, 98, 102	sylanbrc 583	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
104		ixpeq2 8849	. . . . . . . . . . . . . . 15 ⊢ (∀𝑦 ∈ 𝐴 (ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) = X𝑦 ∈ 𝐴 ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
105	103, 104	syl 17	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) = X𝑦 ∈ 𝐴 ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
106		ixpiin 8862	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∩ 𝑚) ≠ ∅ → X𝑦 ∈ 𝐴 ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)X𝑦 ∈ 𝐴 if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
107	106	adantl 482	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → X𝑦 ∈ 𝐴 ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)X𝑦 ∈ 𝐴 if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
108	105, 107	eqtrd 2776	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)X𝑦 ∈ 𝐴 if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
109	39, 53, 108	3eqtr4rd 2787	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) = (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))))
110	25, 109	pm2.61dane 3032	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) = (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))))
111		ixpexg 8860	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∀𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) ∈ V → X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) ∈ V)
112		fvex 6855	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐹‘𝑛) ∈ V
113	112	uniex 7678	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ∪ (𝐹‘𝑛) ∈ V
114	113	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 ∈ 𝐴 → ∪ (𝐹‘𝑛) ∈ V)
115	111, 114	mprg 3070	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) ∈ V
116	10, 115	eqeltri 2834	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑋 ∈ V
117	116	mptex 7173	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) ∈ V
118	117	cnvex 7862	. . . . . . . . . . . . . . . . . . . 20 ⊢ ^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) ∈ V
119	118	imaex 7853	. . . . . . . . . . . . . . . . . . 19 ⊢ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ∈ V
120	119	dfiin2 4994	. . . . . . . . . . . . . . . . . 18 ⊢ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) = ∩ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))}
121		inteq 4910	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} = ∅ → ∩ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} = ∩ ∅)
122	120, 121	eqtrid 2788	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} = ∅ → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) = ∩ ∅)
123		int0 4923	. . . . . . . . . . . . . . . . 17 ⊢ ∩ ∅ = V
124	122, 123	eqtrdi 2792	. . . . . . . . . . . . . . . 16 ⊢ ({𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} = ∅ → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) = V)
125	124	ineq2d 4172	. . . . . . . . . . . . . . 15 ⊢ ({𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} = ∅ → (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) = (𝑋 ∩ V))
126		inv1 4354	. . . . . . . . . . . . . . 15 ⊢ (𝑋 ∩ V) = 𝑋
127	125, 126	eqtrdi 2792	. . . . . . . . . . . . . 14 ⊢ ({𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} = ∅ → (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) = 𝑋)
128	127	adantl 482	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} = ∅) → (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) = 𝑋)
129		snex 5388	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑋} ∈ V
130	1	ptbas 22930	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝐵 ∈ TopBases)
131	1, 10	ptpjpre2 22931	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (𝑘 ∈ 𝐴 ∧ 𝑢 ∈ (𝐹‘𝑘))) → (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝐵)
132	131	ralrimivva 3197	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ∀𝑘 ∈ 𝐴 ∀𝑢 ∈ (𝐹‘𝑘)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝐵)
133		eqid 2736	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) = (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))
134	133	fmpox 7999	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑘 ∈ 𝐴 ∀𝑢 ∈ (𝐹‘𝑘)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝐵 ↔ (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)):∪ 𝑘 ∈ 𝐴 ({𝑘} × (𝐹‘𝑘))⟶𝐵)
135	132, 134	sylib 217	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)):∪ 𝑘 ∈ 𝐴 ({𝑘} × (𝐹‘𝑘))⟶𝐵)
136	135	frnd 6676	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) ⊆ 𝐵)
137	130, 136	ssexd 5281	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) ∈ V)
138		unexg 7683	. . . . . . . . . . . . . . . . . 18 ⊢ (({𝑋} ∈ V ∧ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) ∈ V) → ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ∈ V)
139	129, 137, 138	sylancr 587	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ∈ V)
140		ssfii 9355	. . . . . . . . . . . . . . . . 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 4132	. . . . . . . . . . . . . . . . 17 ⊢ {𝑋} ⊆ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))
144	116	snss 4746	. . . . . . . . . . . . . . . . 17 ⊢ (𝑋 ∈ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ↔ {𝑋} ⊆ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))
145	143, 144	mpbir 230	. . . . . . . . . . . . . . . 16 ⊢ 𝑋 ∈ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))
146	145	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → 𝑋 ∈ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))
147	142, 146	sseldd 3945	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → 𝑋 ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
148	147	adantr 481	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} = ∅) → 𝑋 ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
149	128, 148	eqeltrd 2838	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} = ∅) → (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
150	139	ad3antrrr 728	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ∈ V)
151		nfv 1917	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑛(((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦)))
152		nfcv 2907	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑛𝐴
153		nfcv 2907	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑛(𝐹‘𝑘)
154		nfixp1 8856	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ Ⅎ𝑛X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛)
155	10, 154	nfcxfr 2905	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ Ⅎ𝑛𝑋
156		nfcv 2907	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ Ⅎ𝑛(𝑤‘𝑘)
157	155, 156	nfmpt 5212	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ Ⅎ𝑛(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘))
158	157	nfcnv 5834	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑛^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘))
159		nfcv 2907	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑛𝑢
160	158, 159	nfima 6021	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑛(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)
161	152, 153, 160	nfmpo 7439	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑛(𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))
162	161	nfrn 5907	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑛ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))
163	162	nfcri 2894	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑛 𝑧 ∈ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))
164		df-ov 7360	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑛(𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))(ℎ‘𝑛)) = ((𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))‘⟨𝑛, (ℎ‘𝑛)⟩)
165	119	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ∈ V)
166		fveq2 6842	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑘 = 𝑛 → (𝑤‘𝑘) = (𝑤‘𝑛))
167	166	mpteq2dv 5207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑘 = 𝑛 → (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) = (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)))
168	167	cnveqd 5831	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑘 = 𝑛 → ^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) = ^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)))
169	168	imaeq1d 6012	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑘 = 𝑛 → (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ 𝑢))
170		imaeq2 6009	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑢 = (ℎ‘𝑛) → (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ 𝑢) = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
171	169, 170	sylan9eq 2796	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑘 = 𝑛 ∧ 𝑢 = (ℎ‘𝑛)) → (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
172		fveq2 6842	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑘 = 𝑛 → (𝐹‘𝑘) = (𝐹‘𝑛))
173	171, 172, 133	ovmpox 7508	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑛 ∈ 𝐴 ∧ (ℎ‘𝑛) ∈ (𝐹‘𝑛) ∧ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ∈ V) → (𝑛(𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))(ℎ‘𝑛)) = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
174	29, 35, 165, 173	syl3anc 1371	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (𝑛(𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))(ℎ‘𝑛)) = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
175	164, 174	eqtr3id 2790	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → ((𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))‘⟨𝑛, (ℎ‘𝑛)⟩) = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
176	135	ad3antrrr 728	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)):∪ 𝑘 ∈ 𝐴 ({𝑘} × (𝐹‘𝑘))⟶𝐵)
177	176	ffnd 6669	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) Fn ∪ 𝑘 ∈ 𝐴 ({𝑘} × (𝐹‘𝑘)))
178		opeliunxp 5699	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (⟨𝑛, (ℎ‘𝑛)⟩ ∈ ∪ 𝑛 ∈ 𝐴 ({𝑛} × (𝐹‘𝑛)) ↔ (𝑛 ∈ 𝐴 ∧ (ℎ‘𝑛) ∈ (𝐹‘𝑛)))
179	29, 35, 178	sylanbrc 583	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → ⟨𝑛, (ℎ‘𝑛)⟩ ∈ ∪ 𝑛 ∈ 𝐴 ({𝑛} × (𝐹‘𝑛)))
180		sneq 4596	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑛 = 𝑘 → {𝑛} = {𝑘})
181		fveq2 6842	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑛 = 𝑘 → (𝐹‘𝑛) = (𝐹‘𝑘))
182	180, 181	xpeq12d 5664	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑛 = 𝑘 → ({𝑛} × (𝐹‘𝑛)) = ({𝑘} × (𝐹‘𝑘)))
183	182	cbviunv 5000	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ∪ 𝑛 ∈ 𝐴 ({𝑛} × (𝐹‘𝑛)) = ∪ 𝑘 ∈ 𝐴 ({𝑘} × (𝐹‘𝑘))
184	179, 183	eleqtrdi 2848	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → ⟨𝑛, (ℎ‘𝑛)⟩ ∈ ∪ 𝑘 ∈ 𝐴 ({𝑘} × (𝐹‘𝑘)))
185		fnfvelrn 7031	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) Fn ∪ 𝑘 ∈ 𝐴 ({𝑘} × (𝐹‘𝑘)) ∧ ⟨𝑛, (ℎ‘𝑛)⟩ ∈ ∪ 𝑘 ∈ 𝐴 ({𝑘} × (𝐹‘𝑘))) → ((𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))‘⟨𝑛, (ℎ‘𝑛)⟩) ∈ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))
186	177, 184, 185	syl2anc 584	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → ((𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))‘⟨𝑛, (ℎ‘𝑛)⟩) ∈ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))
187	175, 186	eqeltrrd 2839	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ∈ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))
188		eleq1 2825	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) → (𝑧 ∈ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) ↔ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ∈ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))
189	187, 188	syl5ibrcom 246	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) → 𝑧 ∈ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))
190	189	ex 413	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → (𝑛 ∈ (𝐴 ∩ 𝑚) → (𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) → 𝑧 ∈ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
191	151, 163, 190	rexlimd 3249	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → (∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) → 𝑧 ∈ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))
192	191	abssdv 4025	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ⊆ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))
193		ssun2 4133	. . . . . . . . . . . . . . . . . . . 20 ⊢ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) ⊆ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))
194	192, 193	sstrdi 3956	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ⊆ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))
195	194	adantr 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ⊆ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))
196		simpr 485	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅)
197		simplrl 775	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → 𝑚 ∈ Fin)
198		ssfi 9117	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑚 ∈ Fin ∧ (𝐴 ∩ 𝑚) ⊆ 𝑚) → (𝐴 ∩ 𝑚) ∈ Fin)
199	197, 84, 198	sylancl 586	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → (𝐴 ∩ 𝑚) ∈ Fin)
200		abrexfi 9296	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∩ 𝑚) ∈ Fin → {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ∈ Fin)
201	199, 200	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ∈ Fin)
202		elfir 9351	. . . . . . . . . . . . . . . . . 18 ⊢ ((({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ∈ V ∧ ({𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ⊆ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅ ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ∈ Fin)) → ∩ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
203	150, 195, 196, 201, 202	syl13anc 1372	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → ∩ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
204	120, 203	eqeltrid 2842	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
205		elssuni 4898	. . . . . . . . . . . . . . . 16 ⊢ (∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ ∪ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
206	204, 205	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ ∪ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
207		fiuni 9364	. . . . . . . . . . . . . . . . . 18 ⊢ (({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ∈ V → ∪ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) = ∪ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
208	139, 207	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ∪ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) = ∪ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
209	116	pwid 4582	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑋 ∈ 𝒫 𝑋
210	209	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝑋 ∈ 𝒫 𝑋)
211	210	snssd 4769	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → {𝑋} ⊆ 𝒫 𝑋)
212	1	ptuni2 22927	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) = ∪ 𝐵)
213	10, 212	eqtrid 2788	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝑋 = ∪ 𝐵)
214		eqimss2 4001	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑋 = ∪ 𝐵 → ∪ 𝐵 ⊆ 𝑋)
215	213, 214	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ∪ 𝐵 ⊆ 𝑋)
216		sspwuni 5060	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐵 ⊆ 𝒫 𝑋 ↔ ∪ 𝐵 ⊆ 𝑋)
217	215, 216	sylibr 233	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝐵 ⊆ 𝒫 𝑋)
218	136, 217	sstrd 3954	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) ⊆ 𝒫 𝑋)
219	211, 218	unssd 4146	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ⊆ 𝒫 𝑋)
220		sspwuni 5060	. . . . . . . . . . . . . . . . . . 19 ⊢ (({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ⊆ 𝒫 𝑋 ↔ ∪ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ⊆ 𝑋)
221	219, 220	sylib 217	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ∪ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ⊆ 𝑋)
222		elssuni 4898	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑋 ∈ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) → 𝑋 ⊆ ∪ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))
223	145, 222	mp1i 13	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝑋 ⊆ ∪ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))
224	221, 223	eqssd 3961	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ∪ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) = 𝑋)
225	208, 224	eqtr3d 2778	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ∪ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))) = 𝑋)
226	225	ad3antrrr 728	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → ∪ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))) = 𝑋)
227	206, 226	sseqtrd 3984	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ 𝑋)
228	227, 52	sylib 217	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
229	228, 204	eqeltrd 2838	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
230	149, 229	pm2.61dane 3032	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
231	110, 230	eqeltrd 2838	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
232	231	rexlimdvaa 3153	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) → (∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))))
233	232	impr 455	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ ((ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦)) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
234	3, 233	sylan2b 594	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
235		eleq1 2825	. . . . . . 7 ⊢ (𝑠 = X𝑦 ∈ 𝐴 (ℎ‘𝑦) → (𝑠 ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))) ↔ X𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))))
236	234, 235	syl5ibrcom 246	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → (𝑠 = X𝑦 ∈ 𝐴 (ℎ‘𝑦) → 𝑠 ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))))
237	236	expimpd 454	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (((ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑠 = X𝑦 ∈ 𝐴 (ℎ‘𝑦)) → 𝑠 ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))))
238	237	exlimdv 1936	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (∃ℎ((ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑠 = X𝑦 ∈ 𝐴 (ℎ‘𝑦)) → 𝑠 ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))))
239	2, 238	biimtrid 241	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (𝑠 ∈ 𝐵 → 𝑠 ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))))
240	239	ssrdv 3950	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝐵 ⊆ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
241	1	ptbasid 22926	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) ∈ 𝐵)
242	10, 241	eqeltrid 2842	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝑋 ∈ 𝐵)
243	242	snssd 4769	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → {𝑋} ⊆ 𝐵)
244	243, 136	unssd 4146	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ⊆ 𝐵)
245		fiss 9360	. . . 4 ⊢ ((𝐵 ∈ TopBases ∧ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ⊆ 𝐵) → (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))) ⊆ (fi‘𝐵))
246	130, 244, 245	syl2anc 584	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))) ⊆ (fi‘𝐵))
247	1	ptbasin2 22929	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (fi‘𝐵) = 𝐵)
248	246, 247	sseqtrd 3984	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))) ⊆ 𝐵)
249	240, 248	eqssd 3961	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝐵 = (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 396 ∧ w3a 1087 = wceq 1541 ∃wex 1781 ∈ wcel 2106 {cab 2713 ≠ wne 2943 ∀wral 3064 ∃wrex 3073 Vcvv 3445 ∖ cdif 3907 ∪ cun 3908 ∩ cin 3909 ⊆ wss 3910 ∅c0 4282 ifcif 4486 𝒫 cpw 4560 {csn 4586 ⟨cop 4592 ∪ cuni 4865 ∩ cint 4907 ∪ ciun 4954 ∩ ciin 4955 ↦ cmpt 5188 × cxp 5631 ^◡ccnv 5632 dom cdm 5633 ran crn 5634 “ cima 5636 Fn wfn 6491 ⟶wf 6492 ‘cfv 6496 (class class class)co 7357 ∈ cmpo 7359 Xcixp 8835 Fincfn 8883 ficfi 9346 Topctop 22242 TopBasesctb 22295

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-rep 5242 ax-sep 5256 ax-nul 5263 ax-pow 5320 ax-pr 5384 ax-un 7672

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ne 2944 df-ral 3065 df-rex 3074 df-reu 3354 df-rab 3408 df-v 3447 df-sbc 3740 df-csb 3856 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-pss 3929 df-nul 4283 df-if 4487 df-pw 4562 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-int 4908 df-iun 4956 df-iin 4957 df-br 5106 df-opab 5168 df-mpt 5189 df-tr 5223 df-id 5531 df-eprel 5537 df-po 5545 df-so 5546 df-fr 5588 df-we 5590 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-res 5645 df-ima 5646 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6498 df-fn 6499 df-f 6500 df-f1 6501 df-fo 6502 df-f1o 6503 df-fv 6504 df-ov 7360 df-oprab 7361 df-mpo 7362 df-om 7803 df-1st 7921 df-2nd 7922 df-1o 8412 df-er 8648 df-ixp 8836 df-en 8884 df-dom 8885 df-fin 8887 df-fi 9347 df-top 22243 df-bases 22296

This theorem is referenced by: ptval2 22952 xkoptsub 23005 ptcmplem1 23403 prdsxmslem2 23885

W3C validator