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

Theorem ptbasfi 22117
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.
StepHypRef Expression
1 ptbas.1 . . . . 5 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑥 = X𝑦𝐴 (𝑔𝑦))}
21elpt 22108 . . . 4 (𝑠𝐵 ↔ ∃(( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑦)))
3 df-3an 1081 . . . . . . . 8 (( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦)) ↔ (( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦)) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦)))
4 simprr 769 . . . . . . . . . . . . . 14 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))
5 disjdif2 4424 . . . . . . . . . . . . . . . . . 18 ((𝐴𝑚) = ∅ → (𝐴𝑚) = 𝐴)
65raleqdv 3413 . . . . . . . . . . . . . . . . 17 ((𝐴𝑚) = ∅ → (∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦) ↔ ∀𝑦𝐴 (𝑦) = (𝐹𝑦)))
76biimpac 479 . . . . . . . . . . . . . . . 16 ((∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦) ∧ (𝐴𝑚) = ∅) → ∀𝑦𝐴 (𝑦) = (𝐹𝑦))
8 ixpeq2 8463 . . . . . . . . . . . . . . . 16 (∀𝑦𝐴 (𝑦) = (𝐹𝑦) → X𝑦𝐴 (𝑦) = X𝑦𝐴 (𝐹𝑦))
97, 8syl 17 . . . . . . . . . . . . . . 15 ((∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦) ∧ (𝐴𝑚) = ∅) → X𝑦𝐴 (𝑦) = X𝑦𝐴 (𝐹𝑦))
10 ptbasfi.2 . . . . . . . . . . . . . . . 16 𝑋 = X𝑛𝐴 (𝐹𝑛)
11 fveq2 6663 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑦 → (𝐹𝑛) = (𝐹𝑦))
1211unieqd 4840 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑦 (𝐹𝑛) = (𝐹𝑦))
1312cbvixpv 8467 . . . . . . . . . . . . . . . 16 X𝑛𝐴 (𝐹𝑛) = X𝑦𝐴 (𝐹𝑦)
1410, 13eqtri 2841 . . . . . . . . . . . . . . 15 𝑋 = X𝑦𝐴 (𝐹𝑦)
159, 14syl6eqr 2871 . . . . . . . . . . . . . 14 ((∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦) ∧ (𝐴𝑚) = ∅) → X𝑦𝐴 (𝑦) = 𝑋)
164, 15sylan 580 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) = ∅) → X𝑦𝐴 (𝑦) = 𝑋)
17 ssv 3988 . . . . . . . . . . . . . . . 16 𝑋 ⊆ V
18 iineq1 4927 . . . . . . . . . . . . . . . . 17 ((𝐴𝑚) = ∅ → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) = 𝑛 ∈ ∅ ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
19 0iin 4978 . . . . . . . . . . . . . . . . 17 𝑛 ∈ ∅ ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) = V
2018, 19syl6eq 2869 . . . . . . . . . . . . . . . 16 ((𝐴𝑚) = ∅ → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) = V)
2117, 20sseqtrrid 4017 . . . . . . . . . . . . . . 15 ((𝐴𝑚) = ∅ → 𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
2221adantl 482 . . . . . . . . . . . . . 14 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) = ∅) → 𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
23 df-ss 3949 . . . . . . . . . . . . . 14 (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ↔ (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) = 𝑋)
2422, 23sylib 219 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) = ∅) → (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) = 𝑋)
2516, 24eqtr4d 2856 . . . . . . . . . . . 12 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) = ∅) → X𝑦𝐴 (𝑦) = (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))))
26 simplll 771 . . . . . . . . . . . . . . . 16 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → (𝐴𝑉𝐹:𝐴⟶Top))
27 inss1 4202 . . . . . . . . . . . . . . . . 17 (𝐴𝑚) ⊆ 𝐴
28 simpr 485 . . . . . . . . . . . . . . . . 17 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → 𝑛 ∈ (𝐴𝑚))
2927, 28sseldi 3962 . . . . . . . . . . . . . . . 16 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → 𝑛𝐴)
30 fveq2 6663 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑛 → (𝑦) = (𝑛))
31 fveq2 6663 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑛 → (𝐹𝑦) = (𝐹𝑛))
3230, 31eleq12d 2904 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑛 → ((𝑦) ∈ (𝐹𝑦) ↔ (𝑛) ∈ (𝐹𝑛)))
33 simprr 769 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) → ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))
3433ad2antrr 722 . . . . . . . . . . . . . . . . 17 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))
3532, 34, 29rspcdva 3622 . . . . . . . . . . . . . . . 16 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → (𝑛) ∈ (𝐹𝑛))
3614ptpjpre1 22107 . . . . . . . . . . . . . . . 16 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝑛𝐴 ∧ (𝑛) ∈ (𝐹𝑛))) → ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) = X𝑦𝐴 if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
3726, 29, 35, 36syl12anc 832 . . . . . . . . . . . . . . 15 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) = X𝑦𝐴 if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
3837adantlr 711 . . . . . . . . . . . . . 14 ((((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) ∧ 𝑛 ∈ (𝐴𝑚)) → ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) = X𝑦𝐴 if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
3938iineq2dv 4935 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) = 𝑛 ∈ (𝐴𝑚)X𝑦𝐴 if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
40 simpr 485 . . . . . . . . . . . . . . . . 17 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → (𝐴𝑚) ≠ ∅)
41 cnvimass 5942 . . . . . . . . . . . . . . . . . . . 20 ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ dom (𝑤𝑋 ↦ (𝑤𝑛))
42 eqid 2818 . . . . . . . . . . . . . . . . . . . . 21 (𝑤𝑋 ↦ (𝑤𝑛)) = (𝑤𝑋 ↦ (𝑤𝑛))
4342dmmptss 6088 . . . . . . . . . . . . . . . . . . . 20 dom (𝑤𝑋 ↦ (𝑤𝑛)) ⊆ 𝑋
4441, 43sstri 3973 . . . . . . . . . . . . . . . . . . 19 ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ 𝑋
4544, 14sseqtri 4000 . . . . . . . . . . . . . . . . . 18 ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ X𝑦𝐴 (𝐹𝑦)
4645rgenw 3147 . . . . . . . . . . . . . . . . 17 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ X𝑦𝐴 (𝐹𝑦)
47 r19.2z 4436 . . . . . . . . . . . . . . . . 17 (((𝐴𝑚) ≠ ∅ ∧ ∀𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ X𝑦𝐴 (𝐹𝑦)) → ∃𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ X𝑦𝐴 (𝐹𝑦))
4840, 46, 47sylancl 586 . . . . . . . . . . . . . . . 16 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → ∃𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ X𝑦𝐴 (𝐹𝑦))
49 iinss 4971 . . . . . . . . . . . . . . . 16 (∃𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ X𝑦𝐴 (𝐹𝑦) → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ X𝑦𝐴 (𝐹𝑦))
5048, 49syl 17 . . . . . . . . . . . . . . 15 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ X𝑦𝐴 (𝐹𝑦))
5150, 14sseqtrrdi 4015 . . . . . . . . . . . . . 14 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ 𝑋)
52 sseqin2 4189 . . . . . . . . . . . . . 14 ( 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ 𝑋 ↔ (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) = 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
5351, 52sylib 219 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) = 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
5433ad2antrr 722 . . . . . . . . . . . . . . . . 17 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))
55 ssralv 4030 . . . . . . . . . . . . . . . . . 18 ((𝐴𝑚) ⊆ 𝐴 → (∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦) → ∀𝑦 ∈ (𝐴𝑚)(𝑦) ∈ (𝐹𝑦)))
5627, 55ax-mp 5 . . . . . . . . . . . . . . . . 17 (∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦) → ∀𝑦 ∈ (𝐴𝑚)(𝑦) ∈ (𝐹𝑦))
57 elssuni 4859 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑦) ∈ (𝐹𝑦) → (𝑦) ⊆ (𝐹𝑦))
58 iffalse 4472 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑦 = 𝑛 → if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) = (𝐹𝑦))
5958sseq2d 3996 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑦 = 𝑛 → ((𝑦) ⊆ if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ↔ (𝑦) ⊆ (𝐹𝑦)))
6057, 59syl5ibrcom 248 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦) ∈ (𝐹𝑦) → (¬ 𝑦 = 𝑛 → (𝑦) ⊆ if(𝑦 = 𝑛, (𝑛), (𝐹𝑦))))
61 ssid 3986 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦) ⊆ (𝑦)
62 iftrue 4469 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑛 → if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) = (𝑛))
6362, 30eqtr4d 2856 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = 𝑛 → if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) = (𝑦))
6461, 63sseqtrrid 4017 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = 𝑛 → (𝑦) ⊆ if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
6560, 64pm2.61d2 182 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦) ∈ (𝐹𝑦) → (𝑦) ⊆ if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
6665ralrimivw 3180 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦) ∈ (𝐹𝑦) → ∀𝑛 ∈ (𝐴𝑚)(𝑦) ⊆ if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
67 ssiin 4970 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦) ⊆ 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ↔ ∀𝑛 ∈ (𝐴𝑚)(𝑦) ⊆ if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
6866, 67sylibr 235 . . . . . . . . . . . . . . . . . . . 20 ((𝑦) ∈ (𝐹𝑦) → (𝑦) ⊆ 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
6968adantl 482 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ (𝐴𝑚) ∧ (𝑦) ∈ (𝐹𝑦)) → (𝑦) ⊆ 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
7062equcoms 2018 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = 𝑦 → if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) = (𝑛))
71 fveq2 6663 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = 𝑦 → (𝑛) = (𝑦))
7270, 71eqtrd 2853 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝑦 → if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) = (𝑦))
7372sseq1d 3995 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑦 → (if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ⊆ (𝑦) ↔ (𝑦) ⊆ (𝑦)))
7473rspcev 3620 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 ∈ (𝐴𝑚) ∧ (𝑦) ⊆ (𝑦)) → ∃𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ⊆ (𝑦))
7561, 74mpan2 687 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ (𝐴𝑚) → ∃𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ⊆ (𝑦))
76 iinss 4971 . . . . . . . . . . . . . . . . . . . . 21 (∃𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ⊆ (𝑦) → 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ⊆ (𝑦))
7775, 76syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (𝐴𝑚) → 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ⊆ (𝑦))
7877adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ (𝐴𝑚) ∧ (𝑦) ∈ (𝐹𝑦)) → 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ⊆ (𝑦))
7969, 78eqssd 3981 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ (𝐴𝑚) ∧ (𝑦) ∈ (𝐹𝑦)) → (𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
8079ralimiaa 3156 . . . . . . . . . . . . . . . . 17 (∀𝑦 ∈ (𝐴𝑚)(𝑦) ∈ (𝐹𝑦) → ∀𝑦 ∈ (𝐴𝑚)(𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
8154, 56, 803syl 18 . . . . . . . . . . . . . . . 16 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → ∀𝑦 ∈ (𝐴𝑚)(𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
82 eldifn 4101 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ (𝐴𝑚) → ¬ 𝑦𝑚)
8382ad2antlr 723 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐴𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴𝑚)) ∧ 𝑛 ∈ (𝐴𝑚)) → ¬ 𝑦𝑚)
84 inss2 4203 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴𝑚) ⊆ 𝑚
85 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐴𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴𝑚)) ∧ 𝑛 ∈ (𝐴𝑚)) → 𝑛 ∈ (𝐴𝑚))
8684, 85sseldi 3962 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐴𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴𝑚)) ∧ 𝑛 ∈ (𝐴𝑚)) → 𝑛𝑚)
87 eleq1 2897 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = 𝑛 → (𝑦𝑚𝑛𝑚))
8886, 87syl5ibrcom 248 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐴𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴𝑚)) ∧ 𝑛 ∈ (𝐴𝑚)) → (𝑦 = 𝑛𝑦𝑚))
8983, 88mtod 199 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴𝑚)) ∧ 𝑛 ∈ (𝐴𝑚)) → ¬ 𝑦 = 𝑛)
9089, 58syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴𝑚)) ∧ 𝑛 ∈ (𝐴𝑚)) → if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) = (𝐹𝑦))
9190iineq2dv 4935 . . . . . . . . . . . . . . . . . . . 20 (((𝐴𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴𝑚)) → 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) = 𝑛 ∈ (𝐴𝑚) (𝐹𝑦))
92 iinconst 4920 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴𝑚) ≠ ∅ → 𝑛 ∈ (𝐴𝑚) (𝐹𝑦) = (𝐹𝑦))
9392adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((𝐴𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴𝑚)) → 𝑛 ∈ (𝐴𝑚) (𝐹𝑦) = (𝐹𝑦))
9491, 93eqtr2d 2854 . . . . . . . . . . . . . . . . . . 19 (((𝐴𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴𝑚)) → (𝐹𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
95 eqeq1 2822 . . . . . . . . . . . . . . . . . . 19 ((𝑦) = (𝐹𝑦) → ((𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ↔ (𝐹𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦))))
9694, 95syl5ibrcom 248 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴𝑚)) → ((𝑦) = (𝐹𝑦) → (𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦))))
9796ralimdva 3174 . . . . . . . . . . . . . . . . 17 ((𝐴𝑚) ≠ ∅ → (∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦) → ∀𝑦 ∈ (𝐴𝑚)(𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦))))
984, 97mpan9 507 . . . . . . . . . . . . . . . 16 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → ∀𝑦 ∈ (𝐴𝑚)(𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
99 inundif 4423 . . . . . . . . . . . . . . . . . 18 ((𝐴𝑚) ∪ (𝐴𝑚)) = 𝐴
10099raleqi 3411 . . . . . . . . . . . . . . . . 17 (∀𝑦 ∈ ((𝐴𝑚) ∪ (𝐴𝑚))(𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ↔ ∀𝑦𝐴 (𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
101 ralunb 4164 . . . . . . . . . . . . . . . . 17 (∀𝑦 ∈ ((𝐴𝑚) ∪ (𝐴𝑚))(𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ↔ (∀𝑦 ∈ (𝐴𝑚)(𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦))))
102100, 101bitr3i 278 . . . . . . . . . . . . . . . 16 (∀𝑦𝐴 (𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ↔ (∀𝑦 ∈ (𝐴𝑚)(𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦))))
10381, 98, 102sylanbrc 583 . . . . . . . . . . . . . . 15 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → ∀𝑦𝐴 (𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
104 ixpeq2 8463 . . . . . . . . . . . . . . 15 (∀𝑦𝐴 (𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) → X𝑦𝐴 (𝑦) = X𝑦𝐴 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
105103, 104syl 17 . . . . . . . . . . . . . 14 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → X𝑦𝐴 (𝑦) = X𝑦𝐴 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
106 ixpiin 8476 . . . . . . . . . . . . . . 15 ((𝐴𝑚) ≠ ∅ → X𝑦𝐴 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) = 𝑛 ∈ (𝐴𝑚)X𝑦𝐴 if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
107106adantl 482 . . . . . . . . . . . . . 14 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → X𝑦𝐴 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) = 𝑛 ∈ (𝐴𝑚)X𝑦𝐴 if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
108105, 107eqtrd 2853 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → X𝑦𝐴 (𝑦) = 𝑛 ∈ (𝐴𝑚)X𝑦𝐴 if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
10939, 53, 1083eqtr4rd 2864 . . . . . . . . . . . 12 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → X𝑦𝐴 (𝑦) = (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))))
11025, 109pm2.61dane 3101 . . . . . . . . . . 11 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → X𝑦𝐴 (𝑦) = (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))))
111 ixpexg 8474 . . . . . . . . . . . . . . . . . . . . . . . 24 (∀𝑛𝐴 (𝐹𝑛) ∈ V → X𝑛𝐴 (𝐹𝑛) ∈ V)
112 fvex 6676 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐹𝑛) ∈ V
113112uniex 7454 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐹𝑛) ∈ V
114113a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛𝐴 (𝐹𝑛) ∈ V)
115111, 114mprg 3149 . . . . . . . . . . . . . . . . . . . . . . 23 X𝑛𝐴 (𝐹𝑛) ∈ V
11610, 115eqeltri 2906 . . . . . . . . . . . . . . . . . . . . . 22 𝑋 ∈ V
117116mptex 6977 . . . . . . . . . . . . . . . . . . . . 21 (𝑤𝑋 ↦ (𝑤𝑛)) ∈ V
118117cnvex 7619 . . . . . . . . . . . . . . . . . . . 20 (𝑤𝑋 ↦ (𝑤𝑛)) ∈ V
119118imaex 7610 . . . . . . . . . . . . . . . . . . 19 ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ∈ V
120119dfiin2 4950 . . . . . . . . . . . . . . . . . 18 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) = {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))}
121 inteq 4870 . . . . . . . . . . . . . . . . . 18 ({𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} = ∅ → {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} = ∅)
122120, 121syl5eq 2865 . . . . . . . . . . . . . . . . 17 ({𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} = ∅ → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) = ∅)
123 int0 4881 . . . . . . . . . . . . . . . . 17 ∅ = V
124122, 123syl6eq 2869 . . . . . . . . . . . . . . . 16 ({𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} = ∅ → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) = V)
125124ineq2d 4186 . . . . . . . . . . . . . . 15 ({𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} = ∅ → (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) = (𝑋 ∩ V))
126 inv1 4345 . . . . . . . . . . . . . . 15 (𝑋 ∩ V) = 𝑋
127125, 126syl6eq 2869 . . . . . . . . . . . . . 14 ({𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} = ∅ → (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) = 𝑋)
128127adantl 482 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} = ∅) → (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) = 𝑋)
129 snex 5322 . . . . . . . . . . . . . . . . . 18 {𝑋} ∈ V
1301ptbas 22115 . . . . . . . . . . . . . . . . . . 19 ((𝐴𝑉𝐹:𝐴⟶Top) → 𝐵 ∈ TopBases)
1311, 10ptpjpre2 22116 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝑘𝐴𝑢 ∈ (𝐹𝑘))) → ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) ∈ 𝐵)
132131ralrimivva 3188 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴𝑉𝐹:𝐴⟶Top) → ∀𝑘𝐴𝑢 ∈ (𝐹𝑘)((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) ∈ 𝐵)
133 eqid 2818 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)) = (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))
134133fmpox 7754 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑘𝐴𝑢 ∈ (𝐹𝑘)((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) ∈ 𝐵 ↔ (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)): 𝑘𝐴 ({𝑘} × (𝐹𝑘))⟶𝐵)
135132, 134sylib 219 . . . . . . . . . . . . . . . . . . . 20 ((𝐴𝑉𝐹:𝐴⟶Top) → (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)): 𝑘𝐴 ({𝑘} × (𝐹𝑘))⟶𝐵)
136135frnd 6514 . . . . . . . . . . . . . . . . . . 19 ((𝐴𝑉𝐹:𝐴⟶Top) → ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)) ⊆ 𝐵)
137130, 136ssexd 5219 . . . . . . . . . . . . . . . . . 18 ((𝐴𝑉𝐹:𝐴⟶Top) → ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)) ∈ V)
138 unexg 7461 . . . . . . . . . . . . . . . . . 18 (({𝑋} ∈ V ∧ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)) ∈ V) → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ∈ V)
139129, 137, 138sylancr 587 . . . . . . . . . . . . . . . . 17 ((𝐴𝑉𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ∈ V)
140 ssfii 8871 . . . . . . . . . . . . . . . . 17 (({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ∈ V → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ⊆ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
141139, 140syl 17 . . . . . . . . . . . . . . . 16 ((𝐴𝑉𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ⊆ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
142141ad2antrr 722 . . . . . . . . . . . . . . 15 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ⊆ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
143 ssun1 4145 . . . . . . . . . . . . . . . . 17 {𝑋} ⊆ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))
144116snss 4710 . . . . . . . . . . . . . . . . 17 (𝑋 ∈ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ↔ {𝑋} ⊆ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))
145143, 144mpbir 232 . . . . . . . . . . . . . . . 16 𝑋 ∈ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))
146145a1i 11 . . . . . . . . . . . . . . 15 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → 𝑋 ∈ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))
147142, 146sseldd 3965 . . . . . . . . . . . . . 14 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → 𝑋 ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
148147adantr 481 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} = ∅) → 𝑋 ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
149128, 148eqeltrd 2910 . . . . . . . . . . . 12 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} = ∅) → (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
150139ad3antrrr 726 . . . . . . . . . . . . . . . . . 18 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ∈ V)
151 nfv 1906 . . . . . . . . . . . . . . . . . . . . . 22 𝑛(((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦)))
152 nfcv 2974 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑛𝐴
153 nfcv 2974 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑛(𝐹𝑘)
154 nfixp1 8470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑛X𝑛𝐴 (𝐹𝑛)
15510, 154nfcxfr 2972 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑛𝑋
156 nfcv 2974 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑛(𝑤𝑘)
157155, 156nfmpt 5154 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑛(𝑤𝑋 ↦ (𝑤𝑘))
158157nfcnv 5742 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑛(𝑤𝑋 ↦ (𝑤𝑘))
159 nfcv 2974 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑛𝑢
160158, 159nfima 5930 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑛((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)
161152, 153, 160nfmpo 7225 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑛(𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))
162161nfrn 5817 . . . . . . . . . . . . . . . . . . . . . . 23 𝑛ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))
163162nfcri 2968 . . . . . . . . . . . . . . . . . . . . . 22 𝑛 𝑧 ∈ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))
164 df-ov 7148 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛(𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))(𝑛)) = ((𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))‘⟨𝑛, (𝑛)⟩)
165119a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ∈ V)
166 fveq2 6663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑘 = 𝑛 → (𝑤𝑘) = (𝑤𝑛))
167166mpteq2dv 5153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 = 𝑛 → (𝑤𝑋 ↦ (𝑤𝑘)) = (𝑤𝑋 ↦ (𝑤𝑛)))
168167cnveqd 5739 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑘 = 𝑛(𝑤𝑋 ↦ (𝑤𝑘)) = (𝑤𝑋 ↦ (𝑤𝑛)))
169168imaeq1d 5921 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘 = 𝑛 → ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) = ((𝑤𝑋 ↦ (𝑤𝑛)) “ 𝑢))
170 imaeq2 5918 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑢 = (𝑛) → ((𝑤𝑋 ↦ (𝑤𝑛)) “ 𝑢) = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
171169, 170sylan9eq 2873 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑘 = 𝑛𝑢 = (𝑛)) → ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
172 fveq2 6663 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑘 = 𝑛 → (𝐹𝑘) = (𝐹𝑛))
173171, 172, 133ovmpox 7292 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑛𝐴 ∧ (𝑛) ∈ (𝐹𝑛) ∧ ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ∈ V) → (𝑛(𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))(𝑛)) = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
17429, 35, 165, 173syl3anc 1363 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → (𝑛(𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))(𝑛)) = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
175164, 174syl5eqr 2867 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → ((𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))‘⟨𝑛, (𝑛)⟩) = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
176135ad3antrrr 726 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)): 𝑘𝐴 ({𝑘} × (𝐹𝑘))⟶𝐵)
177176ffnd 6508 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)) Fn 𝑘𝐴 ({𝑘} × (𝐹𝑘)))
178 opeliunxp 5612 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (⟨𝑛, (𝑛)⟩ ∈ 𝑛𝐴 ({𝑛} × (𝐹𝑛)) ↔ (𝑛𝐴 ∧ (𝑛) ∈ (𝐹𝑛)))
17929, 35, 178sylanbrc 583 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → ⟨𝑛, (𝑛)⟩ ∈ 𝑛𝐴 ({𝑛} × (𝐹𝑛)))
180 sneq 4567 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 = 𝑘 → {𝑛} = {𝑘})
181 fveq2 6663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 = 𝑘 → (𝐹𝑛) = (𝐹𝑘))
182180, 181xpeq12d 5579 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 = 𝑘 → ({𝑛} × (𝐹𝑛)) = ({𝑘} × (𝐹𝑘)))
183182cbviunv 4956 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑛𝐴 ({𝑛} × (𝐹𝑛)) = 𝑘𝐴 ({𝑘} × (𝐹𝑘))
184179, 183eleqtrdi 2920 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → ⟨𝑛, (𝑛)⟩ ∈ 𝑘𝐴 ({𝑘} × (𝐹𝑘)))
185 fnfvelrn 6840 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)) Fn 𝑘𝐴 ({𝑘} × (𝐹𝑘)) ∧ ⟨𝑛, (𝑛)⟩ ∈ 𝑘𝐴 ({𝑘} × (𝐹𝑘))) → ((𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))‘⟨𝑛, (𝑛)⟩) ∈ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))
186177, 184, 185syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → ((𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))‘⟨𝑛, (𝑛)⟩) ∈ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))
187175, 186eqeltrrd 2911 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ∈ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))
188 eleq1 2897 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) → (𝑧 ∈ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)) ↔ ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ∈ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))
189187, 188syl5ibrcom 248 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → (𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) → 𝑧 ∈ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))
190189ex 413 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → (𝑛 ∈ (𝐴𝑚) → (𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) → 𝑧 ∈ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
191151, 163, 190rexlimd 3314 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → (∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) → 𝑧 ∈ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))
192191abssdv 4042 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ⊆ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))
193 ssun2 4146 . . . . . . . . . . . . . . . . . . . 20 ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)) ⊆ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))
194192, 193sstrdi 3976 . . . . . . . . . . . . . . . . . . 19 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ⊆ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))
195194adantr 481 . . . . . . . . . . . . . . . . . 18 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ⊆ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))
196 simpr 485 . . . . . . . . . . . . . . . . . 18 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅)
197 simplrl 773 . . . . . . . . . . . . . . . . . . . 20 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → 𝑚 ∈ Fin)
198 ssfi 8726 . . . . . . . . . . . . . . . . . . . 20 ((𝑚 ∈ Fin ∧ (𝐴𝑚) ⊆ 𝑚) → (𝐴𝑚) ∈ Fin)
199197, 84, 198sylancl 586 . . . . . . . . . . . . . . . . . . 19 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → (𝐴𝑚) ∈ Fin)
200 abrexfi 8812 . . . . . . . . . . . . . . . . . . 19 ((𝐴𝑚) ∈ Fin → {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ∈ Fin)
201199, 200syl 17 . . . . . . . . . . . . . . . . . 18 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ∈ Fin)
202 elfir 8867 . . . . . . . . . . . . . . . . . 18 ((({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ∈ V ∧ ({𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ⊆ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅ ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ∈ Fin)) → {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
203150, 195, 196, 201, 202syl13anc 1364 . . . . . . . . . . . . . . . . 17 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
204120, 203eqeltrid 2914 . . . . . . . . . . . . . . . 16 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
205 elssuni 4859 . . . . . . . . . . . . . . . 16 ( 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))) → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
206204, 205syl 17 . . . . . . . . . . . . . . 15 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
207 fiuni 8880 . . . . . . . . . . . . . . . . . 18 (({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ∈ V → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) = (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
208139, 207syl 17 . . . . . . . . . . . . . . . . 17 ((𝐴𝑉𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) = (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
209116pwid 4554 . . . . . . . . . . . . . . . . . . . . . 22 𝑋 ∈ 𝒫 𝑋
210209a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴𝑉𝐹:𝐴⟶Top) → 𝑋 ∈ 𝒫 𝑋)
211210snssd 4734 . . . . . . . . . . . . . . . . . . . 20 ((𝐴𝑉𝐹:𝐴⟶Top) → {𝑋} ⊆ 𝒫 𝑋)
2121ptuni2 22112 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴𝑉𝐹:𝐴⟶Top) → X𝑛𝐴 (𝐹𝑛) = 𝐵)
21310, 212syl5eq 2865 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴𝑉𝐹:𝐴⟶Top) → 𝑋 = 𝐵)
214 eqimss2 4021 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑋 = 𝐵 𝐵𝑋)
215213, 214syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴𝑉𝐹:𝐴⟶Top) → 𝐵𝑋)
216 sspwuni 5013 . . . . . . . . . . . . . . . . . . . . . 22 (𝐵 ⊆ 𝒫 𝑋 𝐵𝑋)
217215, 216sylibr 235 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴𝑉𝐹:𝐴⟶Top) → 𝐵 ⊆ 𝒫 𝑋)
218136, 217sstrd 3974 . . . . . . . . . . . . . . . . . . . 20 ((𝐴𝑉𝐹:𝐴⟶Top) → ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)) ⊆ 𝒫 𝑋)
219211, 218unssd 4159 . . . . . . . . . . . . . . . . . . 19 ((𝐴𝑉𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ⊆ 𝒫 𝑋)
220 sspwuni 5013 . . . . . . . . . . . . . . . . . . 19 (({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ⊆ 𝒫 𝑋 ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ⊆ 𝑋)
221219, 220sylib 219 . . . . . . . . . . . . . . . . . 18 ((𝐴𝑉𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ⊆ 𝑋)
222 elssuni 4859 . . . . . . . . . . . . . . . . . . 19 (𝑋 ∈ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) → 𝑋 ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))
223145, 222mp1i 13 . . . . . . . . . . . . . . . . . 18 ((𝐴𝑉𝐹:𝐴⟶Top) → 𝑋 ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))
224221, 223eqssd 3981 . . . . . . . . . . . . . . . . 17 ((𝐴𝑉𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) = 𝑋)
225208, 224eqtr3d 2855 . . . . . . . . . . . . . . . 16 ((𝐴𝑉𝐹:𝐴⟶Top) → (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))) = 𝑋)
226225ad3antrrr 726 . . . . . . . . . . . . . . 15 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))) = 𝑋)
227206, 226sseqtrd 4004 . . . . . . . . . . . . . 14 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ 𝑋)
228227, 52sylib 219 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) = 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
229228, 204eqeltrd 2910 . . . . . . . . . . . 12 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
230149, 229pm2.61dane 3101 . . . . . . . . . . 11 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
231110, 230eqeltrd 2910 . . . . . . . . . 10 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → X𝑦𝐴 (𝑦) ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
232231rexlimdvaa 3282 . . . . . . . . 9 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) → (∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦) → X𝑦𝐴 (𝑦) ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))))
233232impr 455 . . . . . . . 8 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦)) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → X𝑦𝐴 (𝑦) ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
2343, 233sylan2b 593 . . . . . . 7 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → X𝑦𝐴 (𝑦) ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
235 eleq1 2897 . . . . . . 7 (𝑠 = X𝑦𝐴 (𝑦) → (𝑠 ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))) ↔ X𝑦𝐴 (𝑦) ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))))
236234, 235syl5ibrcom 248 . . . . . 6 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → (𝑠 = X𝑦𝐴 (𝑦) → 𝑠 ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))))
237236expimpd 454 . . . . 5 ((𝐴𝑉𝐹:𝐴⟶Top) → ((( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑦)) → 𝑠 ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))))
238237exlimdv 1925 . . . 4 ((𝐴𝑉𝐹:𝐴⟶Top) → (∃(( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑦)) → 𝑠 ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))))
2392, 238syl5bi 243 . . 3 ((𝐴𝑉𝐹:𝐴⟶Top) → (𝑠𝐵𝑠 ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))))
240239ssrdv 3970 . 2 ((𝐴𝑉𝐹:𝐴⟶Top) → 𝐵 ⊆ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
2411ptbasid 22111 . . . . . . 7 ((𝐴𝑉𝐹:𝐴⟶Top) → X𝑛𝐴 (𝐹𝑛) ∈ 𝐵)
24210, 241eqeltrid 2914 . . . . . 6 ((𝐴𝑉𝐹:𝐴⟶Top) → 𝑋𝐵)
243242snssd 4734 . . . . 5 ((𝐴𝑉𝐹:𝐴⟶Top) → {𝑋} ⊆ 𝐵)
244243, 136unssd 4159 . . . 4 ((𝐴𝑉𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ⊆ 𝐵)
245 fiss 8876 . . . 4 ((𝐵 ∈ TopBases ∧ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ⊆ 𝐵) → (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))) ⊆ (fi‘𝐵))
246130, 244, 245syl2anc 584 . . 3 ((𝐴𝑉𝐹:𝐴⟶Top) → (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))) ⊆ (fi‘𝐵))
2471ptbasin2 22114 . . 3 ((𝐴𝑉𝐹:𝐴⟶Top) → (fi‘𝐵) = 𝐵)
248246, 247sseqtrd 4004 . 2 ((𝐴𝑉𝐹:𝐴⟶Top) → (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))) ⊆ 𝐵)
249240, 248eqssd 3981 1 ((𝐴𝑉𝐹:𝐴⟶Top) → 𝐵 = (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  w3a 1079   = wceq 1528  wex 1771  wcel 2105  {cab 2796  wne 3013  wral 3135  wrex 3136  Vcvv 3492  cdif 3930  cun 3931  cin 3932  wss 3933  c0 4288  ifcif 4463  𝒫 cpw 4535  {csn 4557  cop 4563   cuni 4830   cint 4867   ciun 4910   ciin 4911  cmpt 5137   × cxp 5546  ccnv 5547  dom cdm 5548  ran crn 5549  cima 5551   Fn wfn 6343  wf 6344  cfv 6348  (class class class)co 7145  cmpo 7147  Xcixp 8449  Fincfn 8497  ficfi 8862  Topctop 21429  TopBasesctb 21481
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-ral 3140  df-rex 3141  df-reu 3142  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-int 4868  df-iun 4912  df-iin 4913  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7570  df-1st 7678  df-2nd 7679  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-1o 8091  df-oadd 8095  df-er 8278  df-ixp 8450  df-en 8498  df-dom 8499  df-fin 8501  df-fi 8863  df-top 21430  df-bases 21482
This theorem is referenced by:  ptval2  22137  xkoptsub  22190  ptcmplem1  22588  prdsxmslem2  23066
  Copyright terms: Public domain W3C validator