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 21194

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 21185	. . . 4 ⊢ (𝑠 ∈ 𝐵 ↔ ∃ℎ((ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑠 = X𝑦 ∈ 𝐴 (ℎ‘𝑦)))
3		df-3an 1033	. . . . . . . 8 ⊢ ((ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦)) ↔ ((ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦)) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦)))
4		simprr 792	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))
5		disjdif2 3999	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∩ 𝑚) = ∅ → (𝐴 ∖ 𝑚) = 𝐴)
6	5	raleqdv 3121	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∩ 𝑚) = ∅ → (∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦) ↔ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) = ∪ (𝐹‘𝑦)))
7	6	biimpac 502	. . . . . . . . . . . . . . . 16 ⊢ ((∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦) ∧ (𝐴 ∩ 𝑚) = ∅) → ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) = ∪ (𝐹‘𝑦))
8		ixpeq2 7808	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑦 ∈ 𝐴 (ℎ‘𝑦) = ∪ (𝐹‘𝑦) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) = X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦))
9	7, 8	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦) ∧ (𝐴 ∩ 𝑚) = ∅) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) = X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦))
10		ptbasfi.2	. . . . . . . . . . . . . . . 16 ⊢ 𝑋 = X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛)
11		fveq2 6103	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 = 𝑦 → (𝐹‘𝑛) = (𝐹‘𝑦))
12	11	unieqd 4382	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑦 → ∪ (𝐹‘𝑛) = ∪ (𝐹‘𝑦))
13	12	cbvixpv 7812	. . . . . . . . . . . . . . . 16 ⊢ X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) = X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦)
14	10, 13	eqtri 2632	. . . . . . . . . . . . . . 15 ⊢ 𝑋 = X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦)
15	9, 14	syl6eqr 2662	. . . . . . . . . . . . . 14 ⊢ ((∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦) ∧ (𝐴 ∩ 𝑚) = ∅) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) = 𝑋)
16	4, 15	sylan 487	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) = ∅) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) = 𝑋)
17		ssv 3588	. . . . . . . . . . . . . . . 16 ⊢ 𝑋 ⊆ V
18		iineq1 4471	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∩ 𝑚) = ∅ → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) = ∩ 𝑛 ∈ ∅ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
19		0iin 4514	. . . . . . . . . . . . . . . . 17 ⊢ ∩ 𝑛 ∈ ∅ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) = V
20	18, 19	syl6eq 2660	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∩ 𝑚) = ∅ → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) = V)
21	17, 20	syl5sseqr 3617	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∩ 𝑚) = ∅ → 𝑋 ⊆ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
22	21	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) = ∅) → 𝑋 ⊆ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
23		df-ss 3554	. . . . . . . . . . . . . 14 ⊢ (𝑋 ⊆ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ↔ (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) = 𝑋)
24	22, 23	sylib 207	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) = ∅) → (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) = 𝑋)
25	16, 24	eqtr4d 2647	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) = ∅) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) = (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))))
26		simplll 794	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top))
27		inss1 3795	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 ∩ 𝑚) ⊆ 𝐴
28		simpr 476	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → 𝑛 ∈ (𝐴 ∩ 𝑚))
29	27, 28	sseldi 3566	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → 𝑛 ∈ 𝐴)
30		simprr 792	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) → ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))
31	30	ad2antrr 758	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))
32		fveq2 6103	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑛 → (ℎ‘𝑦) = (ℎ‘𝑛))
33		fveq2 6103	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑛 → (𝐹‘𝑦) = (𝐹‘𝑛))
34	32, 33	eleq12d 2682	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑛 → ((ℎ‘𝑦) ∈ (𝐹‘𝑦) ↔ (ℎ‘𝑛) ∈ (𝐹‘𝑛)))
35	34	rspcv 3278	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ 𝐴 → (∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦) → (ℎ‘𝑛) ∈ (𝐹‘𝑛)))
36	29, 31, 35	sylc 63	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (ℎ‘𝑛) ∈ (𝐹‘𝑛))
37	14	ptpjpre1 21184	. . . . . . . . . . . . . . . 16 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (𝑛 ∈ 𝐴 ∧ (ℎ‘𝑛) ∈ (𝐹‘𝑛))) → (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) = X𝑦 ∈ 𝐴 if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
38	26, 29, 36, 37	syl12anc 1316	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) = X𝑦 ∈ 𝐴 if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
39	38	adantlr 747	. . . . . . . . . . . . . 14 ⊢ ((((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) = X𝑦 ∈ 𝐴 if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
40	39	iineq2dv 4479	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)X𝑦 ∈ 𝐴 if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
41		simpr 476	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → (𝐴 ∩ 𝑚) ≠ ∅)
42		cnvimass 5404	. . . . . . . . . . . . . . . . . . . 20 ⊢ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ dom (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛))
43		eqid 2610	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) = (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛))
44	43	dmmptss 5548	. . . . . . . . . . . . . . . . . . . 20 ⊢ dom (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) ⊆ 𝑋
45	42, 44	sstri 3577	. . . . . . . . . . . . . . . . . . 19 ⊢ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ 𝑋
46	45, 14	sseqtri 3600	. . . . . . . . . . . . . . . . . 18 ⊢ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦)
47	46	rgenw 2908	. . . . . . . . . . . . . . . . 17 ⊢ ∀𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦)
48		r19.2z 4012	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐴 ∩ 𝑚) ≠ ∅ ∧ ∀𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦)) → ∃𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦))
49	41, 47, 48	sylancl 693	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → ∃𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦))
50		iinss 4507	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦))
51	49, 50	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ X𝑦 ∈ 𝐴 ∪ (𝐹‘𝑦))
52	51, 14	syl6sseqr 3615	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ 𝑋)
53		sseqin2 3779	. . . . . . . . . . . . . 14 ⊢ (∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ 𝑋 ↔ (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
54	52, 53	sylib 207	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
55	30	ad2antrr 758	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))
56		ssralv 3629	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∩ 𝑚) ⊆ 𝐴 → (∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦) → ∀𝑦 ∈ (𝐴 ∩ 𝑚)(ℎ‘𝑦) ∈ (𝐹‘𝑦)))
57	27, 56	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦) → ∀𝑦 ∈ (𝐴 ∩ 𝑚)(ℎ‘𝑦) ∈ (𝐹‘𝑦))
58		elssuni 4403	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((ℎ‘𝑦) ∈ (𝐹‘𝑦) → (ℎ‘𝑦) ⊆ ∪ (𝐹‘𝑦))
59		iffalse 4045	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (¬ 𝑦 = 𝑛 → if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) = ∪ (𝐹‘𝑦))
60	59	sseq2d 3596	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (¬ 𝑦 = 𝑛 → ((ℎ‘𝑦) ⊆ if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ↔ (ℎ‘𝑦) ⊆ ∪ (𝐹‘𝑦)))
61	58, 60	syl5ibrcom 236	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ℎ‘𝑦) ∈ (𝐹‘𝑦) → (¬ 𝑦 = 𝑛 → (ℎ‘𝑦) ⊆ if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦))))
62		ssid 3587	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ℎ‘𝑦) ⊆ (ℎ‘𝑦)
63		iftrue 4042	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑦 = 𝑛 → if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) = (ℎ‘𝑛))
64	63, 32	eqtr4d 2647	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = 𝑛 → if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) = (ℎ‘𝑦))
65	62, 64	syl5sseqr 3617	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = 𝑛 → (ℎ‘𝑦) ⊆ if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
66	61, 65	pm2.61d2 171	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℎ‘𝑦) ∈ (𝐹‘𝑦) → (ℎ‘𝑦) ⊆ if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
67	66	ralrimivw 2950	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℎ‘𝑦) ∈ (𝐹‘𝑦) → ∀𝑛 ∈ (𝐴 ∩ 𝑚)(ℎ‘𝑦) ⊆ if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
68		ssiin 4506	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((ℎ‘𝑦) ⊆ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ↔ ∀𝑛 ∈ (𝐴 ∩ 𝑚)(ℎ‘𝑦) ⊆ if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
69	67, 68	sylibr 223	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ‘𝑦) ∈ (𝐹‘𝑦) → (ℎ‘𝑦) ⊆ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
70	69	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ (𝐴 ∩ 𝑚) ∧ (ℎ‘𝑦) ∈ (𝐹‘𝑦)) → (ℎ‘𝑦) ⊆ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
71	63	equcoms 1934	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 = 𝑦 → if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) = (ℎ‘𝑛))
72		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑛 = 𝑦 → (ℎ‘𝑛) = (ℎ‘𝑦))
73	71, 72	eqtrd 2644	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 = 𝑦 → if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) = (ℎ‘𝑦))
74	73	sseq1d 3595	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑛 = 𝑦 → (if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ⊆ (ℎ‘𝑦) ↔ (ℎ‘𝑦) ⊆ (ℎ‘𝑦)))
75	74	rspcev 3282	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑦 ∈ (𝐴 ∩ 𝑚) ∧ (ℎ‘𝑦) ⊆ (ℎ‘𝑦)) → ∃𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ⊆ (ℎ‘𝑦))
76	62, 75	mpan2 703	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 ∈ (𝐴 ∩ 𝑚) → ∃𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ⊆ (ℎ‘𝑦))
77		iinss 4507	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∃𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ⊆ (ℎ‘𝑦) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ⊆ (ℎ‘𝑦))
78	76, 77	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ (𝐴 ∩ 𝑚) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ⊆ (ℎ‘𝑦))
79	78	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ (𝐴 ∩ 𝑚) ∧ (ℎ‘𝑦) ∈ (𝐹‘𝑦)) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ⊆ (ℎ‘𝑦))
80	70, 79	eqssd 3585	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑦 ∈ (𝐴 ∩ 𝑚) ∧ (ℎ‘𝑦) ∈ (𝐹‘𝑦)) → (ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
81	80	ralimiaa 2935	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑦 ∈ (𝐴 ∩ 𝑚)(ℎ‘𝑦) ∈ (𝐹‘𝑦) → ∀𝑦 ∈ (𝐴 ∩ 𝑚)(ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
82	55, 57, 81	3syl 18	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → ∀𝑦 ∈ (𝐴 ∩ 𝑚)(ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
83		eldifn 3695	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 ∈ (𝐴 ∖ 𝑚) → ¬ 𝑦 ∈ 𝑚)
84	83	ad2antlr 759	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ∩ 𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴 ∖ 𝑚)) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → ¬ 𝑦 ∈ 𝑚)
85		inss2 3796	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝐴 ∩ 𝑚) ⊆ 𝑚
86		simpr 476	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝐴 ∩ 𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴 ∖ 𝑚)) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → 𝑛 ∈ (𝐴 ∩ 𝑚))
87	85, 86	sseldi 3566	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝐴 ∩ 𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴 ∖ 𝑚)) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → 𝑛 ∈ 𝑚)
88		eleq1 2676	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = 𝑛 → (𝑦 ∈ 𝑚 ↔ 𝑛 ∈ 𝑚))
89	87, 88	syl5ibrcom 236	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝐴 ∩ 𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴 ∖ 𝑚)) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (𝑦 = 𝑛 → 𝑦 ∈ 𝑚))
90	84, 89	mtod 188	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∩ 𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴 ∖ 𝑚)) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → ¬ 𝑦 = 𝑛)
91	90, 59	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∩ 𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴 ∖ 𝑚)) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) = ∪ (𝐹‘𝑦))
92	91	iineq2dv 4479	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∩ 𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴 ∖ 𝑚)) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)∪ (𝐹‘𝑦))
93		iinconst 4466	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∩ 𝑚) ≠ ∅ → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)∪ (𝐹‘𝑦) = ∪ (𝐹‘𝑦))
94	93	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐴 ∩ 𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴 ∖ 𝑚)) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)∪ (𝐹‘𝑦) = ∪ (𝐹‘𝑦))
95	92, 94	eqtr2d 2645	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝐴 ∩ 𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴 ∖ 𝑚)) → ∪ (𝐹‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
96		eqeq1 2614	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℎ‘𝑦) = ∪ (𝐹‘𝑦) → ((ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ↔ ∪ (𝐹‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦))))
97	95, 96	syl5ibrcom 236	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 ∩ 𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴 ∖ 𝑚)) → ((ℎ‘𝑦) = ∪ (𝐹‘𝑦) → (ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦))))
98	97	ralimdva 2945	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∩ 𝑚) ≠ ∅ → (∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦) → ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦))))
99	4, 98	mpan9 485	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
100		inundif 3998	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∩ 𝑚) ∪ (𝐴 ∖ 𝑚)) = 𝐴
101	100	raleqi 3119	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑦 ∈ ((𝐴 ∩ 𝑚) ∪ (𝐴 ∖ 𝑚))(ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ↔ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
102		ralunb 3756	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑦 ∈ ((𝐴 ∩ 𝑚) ∪ (𝐴 ∖ 𝑚))(ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ↔ (∀𝑦 ∈ (𝐴 ∩ 𝑚)(ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦))))
103	101, 102	bitr3i 265	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑦 ∈ 𝐴 (ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ↔ (∀𝑦 ∈ (𝐴 ∩ 𝑚)(ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦))))
104	82, 99, 103	sylanbrc 695	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
105		ixpeq2 7808	. . . . . . . . . . . . . . 15 ⊢ (∀𝑦 ∈ 𝐴 (ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) = X𝑦 ∈ 𝐴 ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
106	104, 105	syl 17	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) = X𝑦 ∈ 𝐴 ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
107		ixpiin 7820	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∩ 𝑚) ≠ ∅ → X𝑦 ∈ 𝐴 ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)X𝑦 ∈ 𝐴 if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
108	107	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → X𝑦 ∈ 𝐴 ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)X𝑦 ∈ 𝐴 if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
109	106, 108	eqtrd 2644	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)X𝑦 ∈ 𝐴 if(𝑦 = 𝑛, (ℎ‘𝑛), ∪ (𝐹‘𝑦)))
110	40, 54, 109	3eqtr4rd 2655	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ (𝐴 ∩ 𝑚) ≠ ∅) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) = (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))))
111	25, 110	pm2.61dane 2869	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) = (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))))
112		ixpexg 7818	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∀𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) ∈ V → X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) ∈ V)
113		fvex 6113	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝐹‘𝑛) ∈ V
114	113	uniex 6851	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ∪ (𝐹‘𝑛) ∈ V
115	114	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑛 ∈ 𝐴 → ∪ (𝐹‘𝑛) ∈ V)
116	112, 115	mprg 2910	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) ∈ V
117	10, 116	eqeltri 2684	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑋 ∈ V
118	117	mptex 6390	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) ∈ V
119	118	cnvex 7006	. . . . . . . . . . . . . . . . . . . 20 ⊢ ^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) ∈ V
120	119	imaex 6996	. . . . . . . . . . . . . . . . . . 19 ⊢ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ∈ V
121	120	dfiin2 4491	. . . . . . . . . . . . . . . . . 18 ⊢ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) = ∩ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))}
122		inteq 4413	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} = ∅ → ∩ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} = ∩ ∅)
123	121, 122	syl5eq 2656	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} = ∅ → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) = ∩ ∅)
124		int0 4425	. . . . . . . . . . . . . . . . 17 ⊢ ∩ ∅ = V
125	123, 124	syl6eq 2660	. . . . . . . . . . . . . . . 16 ⊢ ({𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} = ∅ → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) = V)
126	125	ineq2d 3776	. . . . . . . . . . . . . . 15 ⊢ ({𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} = ∅ → (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) = (𝑋 ∩ V))
127		inv1 3922	. . . . . . . . . . . . . . 15 ⊢ (𝑋 ∩ V) = 𝑋
128	126, 127	syl6eq 2660	. . . . . . . . . . . . . 14 ⊢ ({𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} = ∅ → (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) = 𝑋)
129	128	adantl 481	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} = ∅) → (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) = 𝑋)
130		snex 4835	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑋} ∈ V
131	1	ptbas 21192	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝐵 ∈ TopBases)
132	1, 10	ptpjpre2 21193	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (𝑘 ∈ 𝐴 ∧ 𝑢 ∈ (𝐹‘𝑘))) → (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝐵)
133	132	ralrimivva 2954	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ∀𝑘 ∈ 𝐴 ∀𝑢 ∈ (𝐹‘𝑘)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝐵)
134		eqid 2610	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) = (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))
135	134	fmpt2x 7125	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑘 ∈ 𝐴 ∀𝑢 ∈ (𝐹‘𝑘)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) ∈ 𝐵 ↔ (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)):∪ 𝑘 ∈ 𝐴 ({𝑘} × (𝐹‘𝑘))⟶𝐵)
136	133, 135	sylib 207	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)):∪ 𝑘 ∈ 𝐴 ({𝑘} × (𝐹‘𝑘))⟶𝐵)
137		frn 5966	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)):∪ 𝑘 ∈ 𝐴 ({𝑘} × (𝐹‘𝑘))⟶𝐵 → ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) ⊆ 𝐵)
138	136, 137	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) ⊆ 𝐵)
139	131, 138	ssexd 4733	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) ∈ V)
140		unexg 6857	. . . . . . . . . . . . . . . . . 18 ⊢ (({𝑋} ∈ V ∧ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) ∈ V) → ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ∈ V)
141	130, 139, 140	sylancr 694	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ∈ V)
142		ssfii 8208	. . . . . . . . . . . . . . . . 17 ⊢ (({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ∈ V → ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ⊆ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
143	141, 142	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ⊆ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
144	143	ad2antrr 758	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ⊆ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
145		ssun1 3738	. . . . . . . . . . . . . . . . 17 ⊢ {𝑋} ⊆ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))
146	117	snss 4259	. . . . . . . . . . . . . . . . 17 ⊢ (𝑋 ∈ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ↔ {𝑋} ⊆ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))
147	145, 146	mpbir 220	. . . . . . . . . . . . . . . 16 ⊢ 𝑋 ∈ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))
148	147	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → 𝑋 ∈ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))
149	144, 148	sseldd 3569	. . . . . . . . . . . . . 14 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → 𝑋 ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
150	149	adantr 480	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} = ∅) → 𝑋 ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
151	129, 150	eqeltrd 2688	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} = ∅) → (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
152	141	ad3antrrr 762	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ∈ V)
153		nfv 1830	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑛(((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦)))
154		nfcv 2751	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑛𝐴
155		nfcv 2751	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑛(𝐹‘𝑘)
156		nfixp1 7814	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ Ⅎ𝑛X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛)
157	10, 156	nfcxfr 2749	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ Ⅎ𝑛𝑋
158		nfcv 2751	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ Ⅎ𝑛(𝑤‘𝑘)
159	157, 158	nfmpt 4674	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ Ⅎ𝑛(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘))
160	159	nfcnv 5223	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑛^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘))
161		nfcv 2751	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ Ⅎ𝑛𝑢
162	160, 161	nfima 5393	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑛(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)
163	154, 155, 162	nfmpt2 6622	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ Ⅎ𝑛(𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))
164	163	nfrn 5289	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ Ⅎ𝑛ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))
165	164	nfcri 2745	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ Ⅎ𝑛 𝑧 ∈ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))
166		df-ov 6552	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑛(𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))(ℎ‘𝑛)) = ((𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))‘⟨𝑛, (ℎ‘𝑛)⟩)
167	120	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ∈ V)
168		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑘 = 𝑛 → (𝑤‘𝑘) = (𝑤‘𝑛))
169	168	mpteq2dv 4673	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑘 = 𝑛 → (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) = (𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)))
170	169	cnveqd 5220	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑘 = 𝑛 → ^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) = ^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)))
171	170	imaeq1d 5384	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑘 = 𝑛 → (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ 𝑢))
172		imaeq2 5381	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑢 = (ℎ‘𝑛) → (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ 𝑢) = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
173	171, 172	sylan9eq 2664	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑘 = 𝑛 ∧ 𝑢 = (ℎ‘𝑛)) → (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢) = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
174		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑘 = 𝑛 → (𝐹‘𝑘) = (𝐹‘𝑛))
175	173, 174, 134	ovmpt2x 6687	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑛 ∈ 𝐴 ∧ (ℎ‘𝑛) ∈ (𝐹‘𝑛) ∧ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ∈ V) → (𝑛(𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))(ℎ‘𝑛)) = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
176	29, 36, 167, 175	syl3anc 1318	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (𝑛(𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))(ℎ‘𝑛)) = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
177	166, 176	syl5eqr 2658	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → ((𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))‘⟨𝑛, (ℎ‘𝑛)⟩) = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
178	136	ad3antrrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)):∪ 𝑘 ∈ 𝐴 ({𝑘} × (𝐹‘𝑘))⟶𝐵)
179	178	ffnd 5959	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) Fn ∪ 𝑘 ∈ 𝐴 ({𝑘} × (𝐹‘𝑘)))
180		opeliunxp 5093	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (⟨𝑛, (ℎ‘𝑛)⟩ ∈ ∪ 𝑛 ∈ 𝐴 ({𝑛} × (𝐹‘𝑛)) ↔ (𝑛 ∈ 𝐴 ∧ (ℎ‘𝑛) ∈ (𝐹‘𝑛)))
181	29, 36, 180	sylanbrc 695	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → ⟨𝑛, (ℎ‘𝑛)⟩ ∈ ∪ 𝑛 ∈ 𝐴 ({𝑛} × (𝐹‘𝑛)))
182		sneq 4135	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑛 = 𝑘 → {𝑛} = {𝑘})
183		fveq2 6103	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑛 = 𝑘 → (𝐹‘𝑛) = (𝐹‘𝑘))
184	182, 183	xpeq12d 5064	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑛 = 𝑘 → ({𝑛} × (𝐹‘𝑛)) = ({𝑘} × (𝐹‘𝑘)))
185	184	cbviunv 4495	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ∪ 𝑛 ∈ 𝐴 ({𝑛} × (𝐹‘𝑛)) = ∪ 𝑘 ∈ 𝐴 ({𝑘} × (𝐹‘𝑘))
186	181, 185	syl6eleq 2698	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → ⟨𝑛, (ℎ‘𝑛)⟩ ∈ ∪ 𝑘 ∈ 𝐴 ({𝑘} × (𝐹‘𝑘)))
187		fnfvelrn 6264	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) Fn ∪ 𝑘 ∈ 𝐴 ({𝑘} × (𝐹‘𝑘)) ∧ ⟨𝑛, (ℎ‘𝑛)⟩ ∈ ∪ 𝑘 ∈ 𝐴 ({𝑘} × (𝐹‘𝑘))) → ((𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))‘⟨𝑛, (ℎ‘𝑛)⟩) ∈ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))
188	179, 186, 187	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → ((𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))‘⟨𝑛, (ℎ‘𝑛)⟩) ∈ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))
189	177, 188	eqeltrrd 2689	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ∈ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))
190		eleq1 2676	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) → (𝑧 ∈ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) ↔ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ∈ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))
191	189, 190	syl5ibrcom 236	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ 𝑛 ∈ (𝐴 ∩ 𝑚)) → (𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) → 𝑧 ∈ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))
192	191	ex 449	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → (𝑛 ∈ (𝐴 ∩ 𝑚) → (𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) → 𝑧 ∈ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
193	153, 165, 192	rexlimd 3008	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → (∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) → 𝑧 ∈ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))
194	193	abssdv 3639	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ⊆ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))
195		ssun2 3739	. . . . . . . . . . . . . . . . . . . 20 ⊢ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) ⊆ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))
196	194, 195	syl6ss 3580	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ⊆ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))
197	196	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ⊆ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))
198		simpr 476	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅)
199		simplrl 796	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → 𝑚 ∈ Fin)
200		ssfi 8065	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑚 ∈ Fin ∧ (𝐴 ∩ 𝑚) ⊆ 𝑚) → (𝐴 ∩ 𝑚) ∈ Fin)
201	199, 85, 200	sylancl 693	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → (𝐴 ∩ 𝑚) ∈ Fin)
202		abrexfi 8149	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∩ 𝑚) ∈ Fin → {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ∈ Fin)
203	201, 202	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ∈ Fin)
204		elfir 8204	. . . . . . . . . . . . . . . . . 18 ⊢ ((({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ∈ V ∧ ({𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ⊆ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅ ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ∈ Fin)) → ∩ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
205	152, 197, 198, 203, 204	syl13anc 1320	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → ∩ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
206	121, 205	syl5eqel 2692	. . . . . . . . . . . . . . . 16 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
207		elssuni 4403	. . . . . . . . . . . . . . . 16 ⊢ (∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ ∪ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
208	206, 207	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ ∪ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
209		fiuni 8217	. . . . . . . . . . . . . . . . . 18 ⊢ (({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ∈ V → ∪ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) = ∪ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
210	141, 209	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ∪ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) = ∪ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
211	117	pwid 4122	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑋 ∈ 𝒫 𝑋
212	211	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝑋 ∈ 𝒫 𝑋)
213	212	snssd 4281	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → {𝑋} ⊆ 𝒫 𝑋)
214	1	ptuni2 21189	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) = ∪ 𝐵)
215	10, 214	syl5eq 2656	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝑋 = ∪ 𝐵)
216		eqimss2 3621	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑋 = ∪ 𝐵 → ∪ 𝐵 ⊆ 𝑋)
217	215, 216	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ∪ 𝐵 ⊆ 𝑋)
218		sspwuni 4547	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐵 ⊆ 𝒫 𝑋 ↔ ∪ 𝐵 ⊆ 𝑋)
219	217, 218	sylibr 223	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝐵 ⊆ 𝒫 𝑋)
220	138, 219	sstrd 3578	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)) ⊆ 𝒫 𝑋)
221	213, 220	unssd 3751	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ⊆ 𝒫 𝑋)
222		sspwuni 4547	. . . . . . . . . . . . . . . . . . 19 ⊢ (({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ⊆ 𝒫 𝑋 ↔ ∪ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ⊆ 𝑋)
223	221, 222	sylib 207	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ∪ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ⊆ 𝑋)
224		elssuni 4403	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑋 ∈ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) → 𝑋 ⊆ ∪ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))
225	147, 224	mp1i 13	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝑋 ⊆ ∪ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))
226	223, 225	eqssd 3585	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ∪ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) = 𝑋)
227	210, 226	eqtr3d 2646	. . . . . . . . . . . . . . . 16 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ∪ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))) = 𝑋)
228	227	ad3antrrr 762	. . . . . . . . . . . . . . 15 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → ∪ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))) = 𝑋)
229	208, 228	sseqtrd 3604	. . . . . . . . . . . . . 14 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)) ⊆ 𝑋)
230	229, 53	sylib 207	. . . . . . . . . . . . 13 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) = ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛)))
231	230, 206	eqeltrd 2688	. . . . . . . . . . . 12 ⊢ (((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴 ∩ 𝑚)𝑧 = (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))} ≠ ∅) → (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
232	151, 231	pm2.61dane 2869	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → (𝑋 ∩ ∩ 𝑛 ∈ (𝐴 ∩ 𝑚)(^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑛)) “ (ℎ‘𝑛))) ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
233	111, 232	eqeltrd 2688	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
234	233	rexlimdvaa 3014	. . . . . . . . 9 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦))) → (∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))))
235	234	impr 647	. . . . . . . 8 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ ((ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦)) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
236	3, 235	sylan2b 491	. . . . . . 7 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → X𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
237		eleq1 2676	. . . . . . 7 ⊢ (𝑠 = X𝑦 ∈ 𝐴 (ℎ‘𝑦) → (𝑠 ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))) ↔ X𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))))
238	236, 237	syl5ibrcom 236	. . . . . 6 ⊢ (((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) ∧ (ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦))) → (𝑠 = X𝑦 ∈ 𝐴 (ℎ‘𝑦) → 𝑠 ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))))
239	238	expimpd 627	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (((ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑠 = X𝑦 ∈ 𝐴 (ℎ‘𝑦)) → 𝑠 ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))))
240	239	exlimdv 1848	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (∃ℎ((ℎ Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (ℎ‘𝑦) ∈ (𝐹‘𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴 ∖ 𝑚)(ℎ‘𝑦) = ∪ (𝐹‘𝑦)) ∧ 𝑠 = X𝑦 ∈ 𝐴 (ℎ‘𝑦)) → 𝑠 ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))))
241	2, 240	syl5bi 231	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (𝑠 ∈ 𝐵 → 𝑠 ∈ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))))))
242	241	ssrdv 3574	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝐵 ⊆ (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))
243	1	ptbasid 21188	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → X𝑛 ∈ 𝐴 ∪ (𝐹‘𝑛) ∈ 𝐵)
244	10, 243	syl5eqel 2692	. . . . . 6 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝑋 ∈ 𝐵)
245	244	snssd 4281	. . . . 5 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → {𝑋} ⊆ 𝐵)
246	245, 138	unssd 3751	. . . 4 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ⊆ 𝐵)
247		fiss 8213	. . . 4 ⊢ ((𝐵 ∈ TopBases ∧ ({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢))) ⊆ 𝐵) → (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))) ⊆ (fi‘𝐵))
248	131, 246, 247	syl2anc 691	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))) ⊆ (fi‘𝐵))
249	1	ptbasin2 21191	. . 3 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (fi‘𝐵) = 𝐵)
250	248, 249	sseqtrd 3604	. 2 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))) ⊆ 𝐵)
251	242, 250	eqssd 3585	1 ⊢ ((𝐴 ∈ 𝑉 ∧ 𝐹:𝐴⟶Top) → 𝐵 = (fi‘({𝑋} ∪ ran (𝑘 ∈ 𝐴, 𝑢 ∈ (𝐹‘𝑘) ↦ (^◡(𝑤 ∈ 𝑋 ↦ (𝑤‘𝑘)) “ 𝑢)))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 383 ∧ w3a 1031 = wceq 1475 ∃wex 1695 ∈ wcel 1977 {cab 2596 ≠ wne 2780 ∀wral 2896 ∃wrex 2897 Vcvv 3173 ∖ cdif 3537 ∪ cun 3538 ∩ cin 3539 ⊆ wss 3540 ∅c0 3874 ifcif 4036 𝒫 cpw 4108 {csn 4125 ⟨cop 4131 ∪ cuni 4372 ∩ cint 4410 ∪ ciun 4455 ∩ ciin 4456 ↦ cmpt 4643 × cxp 5036 ^◡ccnv 5037 dom cdm 5038 ran crn 5039 “ cima 5041 Fn wfn 5799 ⟶wf 5800 ‘cfv 5804 (class class class)co 6549 ↦ cmpt2 6551 Xcixp 7794 Fincfn 7841 ficfi 8199 Topctop 20517 TopBasesctb 20520

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-ral 2901 df-rex 2902 df-reu 2903 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-int 4411 df-iun 4457 df-iin 4458 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-om 6958 df-1st 7059 df-2nd 7060 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-1o 7447 df-oadd 7451 df-er 7629 df-ixp 7795 df-en 7842 df-dom 7843 df-fin 7845 df-fi 8200 df-top 20521 df-bases 20522

This theorem is referenced by: ptval2 21214 xkoptsub 21267 ptcmplem1 21666 prdsxmslem2 22144

W3C validator