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

Theorem ptbasfi 23576
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 23567 . . . 4 (𝑠𝐵 ↔ ∃(( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑦)))
3 df-3an 1086 . . . . . . . 8 (( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦)) ↔ (( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦)) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦)))
4 simprr 771 . . . . . . . . . . . . . 14 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))
5 disjdif2 4484 . . . . . . . . . . . . . . . . . 18 ((𝐴𝑚) = ∅ → (𝐴𝑚) = 𝐴)
65raleqdv 3315 . . . . . . . . . . . . . . . . 17 ((𝐴𝑚) = ∅ → (∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦) ↔ ∀𝑦𝐴 (𝑦) = (𝐹𝑦)))
76biimpac 477 . . . . . . . . . . . . . . . 16 ((∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦) ∧ (𝐴𝑚) = ∅) → ∀𝑦𝐴 (𝑦) = (𝐹𝑦))
8 ixpeq2 8940 . . . . . . . . . . . . . . . 16 (∀𝑦𝐴 (𝑦) = (𝐹𝑦) → X𝑦𝐴 (𝑦) = X𝑦𝐴 (𝐹𝑦))
97, 8syl 17 . . . . . . . . . . . . . . 15 ((∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦) ∧ (𝐴𝑚) = ∅) → X𝑦𝐴 (𝑦) = X𝑦𝐴 (𝐹𝑦))
10 ptbasfi.2 . . . . . . . . . . . . . . . 16 𝑋 = X𝑛𝐴 (𝐹𝑛)
11 fveq2 6901 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑦 → (𝐹𝑛) = (𝐹𝑦))
1211unieqd 4926 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑦 (𝐹𝑛) = (𝐹𝑦))
1312cbvixpv 8944 . . . . . . . . . . . . . . . 16 X𝑛𝐴 (𝐹𝑛) = X𝑦𝐴 (𝐹𝑦)
1410, 13eqtri 2754 . . . . . . . . . . . . . . 15 𝑋 = X𝑦𝐴 (𝐹𝑦)
159, 14eqtr4di 2784 . . . . . . . . . . . . . 14 ((∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦) ∧ (𝐴𝑚) = ∅) → X𝑦𝐴 (𝑦) = 𝑋)
164, 15sylan 578 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) = ∅) → X𝑦𝐴 (𝑦) = 𝑋)
17 ssv 4004 . . . . . . . . . . . . . . . 16 𝑋 ⊆ V
18 iineq1 5018 . . . . . . . . . . . . . . . . 17 ((𝐴𝑚) = ∅ → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) = 𝑛 ∈ ∅ ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
19 0iin 5072 . . . . . . . . . . . . . . . . 17 𝑛 ∈ ∅ ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) = V
2018, 19eqtrdi 2782 . . . . . . . . . . . . . . . 16 ((𝐴𝑚) = ∅ → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) = V)
2117, 20sseqtrrid 4033 . . . . . . . . . . . . . . 15 ((𝐴𝑚) = ∅ → 𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
2221adantl 480 . . . . . . . . . . . . . 14 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) = ∅) → 𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
23 dfss2 3965 . . . . . . . . . . . . . 14 (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ↔ (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) = 𝑋)
2422, 23sylib 217 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) = ∅) → (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) = 𝑋)
2516, 24eqtr4d 2769 . . . . . . . . . . . 12 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) = ∅) → X𝑦𝐴 (𝑦) = (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))))
26 simplll 773 . . . . . . . . . . . . . . . 16 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → (𝐴𝑉𝐹:𝐴⟶Top))
27 inss1 4230 . . . . . . . . . . . . . . . . 17 (𝐴𝑚) ⊆ 𝐴
28 simpr 483 . . . . . . . . . . . . . . . . 17 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → 𝑛 ∈ (𝐴𝑚))
2927, 28sselid 3977 . . . . . . . . . . . . . . . 16 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → 𝑛𝐴)
30 fveq2 6901 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑛 → (𝑦) = (𝑛))
31 fveq2 6901 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑛 → (𝐹𝑦) = (𝐹𝑛))
3230, 31eleq12d 2820 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑛 → ((𝑦) ∈ (𝐹𝑦) ↔ (𝑛) ∈ (𝐹𝑛)))
33 simprr 771 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) → ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))
3433ad2antrr 724 . . . . . . . . . . . . . . . . 17 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))
3532, 34, 29rspcdva 3609 . . . . . . . . . . . . . . . 16 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → (𝑛) ∈ (𝐹𝑛))
3614ptpjpre1 23566 . . . . . . . . . . . . . . . 16 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝑛𝐴 ∧ (𝑛) ∈ (𝐹𝑛))) → ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) = X𝑦𝐴 if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
3726, 29, 35, 36syl12anc 835 . . . . . . . . . . . . . . 15 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) = X𝑦𝐴 if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
3837adantlr 713 . . . . . . . . . . . . . 14 ((((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) ∧ 𝑛 ∈ (𝐴𝑚)) → ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) = X𝑦𝐴 if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
3938iineq2dv 5026 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) = 𝑛 ∈ (𝐴𝑚)X𝑦𝐴 if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
40 simpr 483 . . . . . . . . . . . . . . . . 17 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → (𝐴𝑚) ≠ ∅)
41 cnvimass 6091 . . . . . . . . . . . . . . . . . . . 20 ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ dom (𝑤𝑋 ↦ (𝑤𝑛))
42 eqid 2726 . . . . . . . . . . . . . . . . . . . . 21 (𝑤𝑋 ↦ (𝑤𝑛)) = (𝑤𝑋 ↦ (𝑤𝑛))
4342dmmptss 6252 . . . . . . . . . . . . . . . . . . . 20 dom (𝑤𝑋 ↦ (𝑤𝑛)) ⊆ 𝑋
4441, 43sstri 3989 . . . . . . . . . . . . . . . . . . 19 ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ 𝑋
4544, 14sseqtri 4016 . . . . . . . . . . . . . . . . . 18 ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ X𝑦𝐴 (𝐹𝑦)
4645rgenw 3055 . . . . . . . . . . . . . . . . 17 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ X𝑦𝐴 (𝐹𝑦)
47 r19.2z 4499 . . . . . . . . . . . . . . . . 17 (((𝐴𝑚) ≠ ∅ ∧ ∀𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ X𝑦𝐴 (𝐹𝑦)) → ∃𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ X𝑦𝐴 (𝐹𝑦))
4840, 46, 47sylancl 584 . . . . . . . . . . . . . . . 16 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → ∃𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ X𝑦𝐴 (𝐹𝑦))
49 iinss 5064 . . . . . . . . . . . . . . . 16 (∃𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ X𝑦𝐴 (𝐹𝑦) → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ X𝑦𝐴 (𝐹𝑦))
5048, 49syl 17 . . . . . . . . . . . . . . 15 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ X𝑦𝐴 (𝐹𝑦))
5150, 14sseqtrrdi 4031 . . . . . . . . . . . . . 14 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ 𝑋)
52 sseqin2 4216 . . . . . . . . . . . . . 14 ( 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ 𝑋 ↔ (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) = 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
5351, 52sylib 217 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) = 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
5433ad2antrr 724 . . . . . . . . . . . . . . . . 17 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))
55 ssralv 4048 . . . . . . . . . . . . . . . . . 18 ((𝐴𝑚) ⊆ 𝐴 → (∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦) → ∀𝑦 ∈ (𝐴𝑚)(𝑦) ∈ (𝐹𝑦)))
5627, 55ax-mp 5 . . . . . . . . . . . . . . . . 17 (∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦) → ∀𝑦 ∈ (𝐴𝑚)(𝑦) ∈ (𝐹𝑦))
57 elssuni 4945 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑦) ∈ (𝐹𝑦) → (𝑦) ⊆ (𝐹𝑦))
58 iffalse 4542 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑦 = 𝑛 → if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) = (𝐹𝑦))
5958sseq2d 4012 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑦 = 𝑛 → ((𝑦) ⊆ if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ↔ (𝑦) ⊆ (𝐹𝑦)))
6057, 59syl5ibrcom 246 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦) ∈ (𝐹𝑦) → (¬ 𝑦 = 𝑛 → (𝑦) ⊆ if(𝑦 = 𝑛, (𝑛), (𝐹𝑦))))
61 ssid 4002 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦) ⊆ (𝑦)
62 iftrue 4539 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑛 → if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) = (𝑛))
6362, 30eqtr4d 2769 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = 𝑛 → if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) = (𝑦))
6461, 63sseqtrrid 4033 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = 𝑛 → (𝑦) ⊆ if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
6560, 64pm2.61d2 181 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦) ∈ (𝐹𝑦) → (𝑦) ⊆ if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
6665ralrimivw 3140 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦) ∈ (𝐹𝑦) → ∀𝑛 ∈ (𝐴𝑚)(𝑦) ⊆ if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
67 ssiin 5063 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦) ⊆ 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ↔ ∀𝑛 ∈ (𝐴𝑚)(𝑦) ⊆ if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
6866, 67sylibr 233 . . . . . . . . . . . . . . . . . . . 20 ((𝑦) ∈ (𝐹𝑦) → (𝑦) ⊆ 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
6968adantl 480 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ (𝐴𝑚) ∧ (𝑦) ∈ (𝐹𝑦)) → (𝑦) ⊆ 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
7062equcoms 2016 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = 𝑦 → if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) = (𝑛))
71 fveq2 6901 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = 𝑦 → (𝑛) = (𝑦))
7270, 71eqtrd 2766 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝑦 → if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) = (𝑦))
7372sseq1d 4011 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑦 → (if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ⊆ (𝑦) ↔ (𝑦) ⊆ (𝑦)))
7473rspcev 3608 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 ∈ (𝐴𝑚) ∧ (𝑦) ⊆ (𝑦)) → ∃𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ⊆ (𝑦))
7561, 74mpan2 689 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ (𝐴𝑚) → ∃𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ⊆ (𝑦))
76 iinss 5064 . . . . . . . . . . . . . . . . . . . . 21 (∃𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ⊆ (𝑦) → 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ⊆ (𝑦))
7775, 76syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (𝐴𝑚) → 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ⊆ (𝑦))
7877adantr 479 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ (𝐴𝑚) ∧ (𝑦) ∈ (𝐹𝑦)) → 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ⊆ (𝑦))
7969, 78eqssd 3997 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ (𝐴𝑚) ∧ (𝑦) ∈ (𝐹𝑦)) → (𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
8079ralimiaa 3072 . . . . . . . . . . . . . . . . 17 (∀𝑦 ∈ (𝐴𝑚)(𝑦) ∈ (𝐹𝑦) → ∀𝑦 ∈ (𝐴𝑚)(𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
8154, 56, 803syl 18 . . . . . . . . . . . . . . . 16 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → ∀𝑦 ∈ (𝐴𝑚)(𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
82 eldifn 4127 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ (𝐴𝑚) → ¬ 𝑦𝑚)
8382ad2antlr 725 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐴𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴𝑚)) ∧ 𝑛 ∈ (𝐴𝑚)) → ¬ 𝑦𝑚)
84 inss2 4231 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴𝑚) ⊆ 𝑚
85 simpr 483 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐴𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴𝑚)) ∧ 𝑛 ∈ (𝐴𝑚)) → 𝑛 ∈ (𝐴𝑚))
8684, 85sselid 3977 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐴𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴𝑚)) ∧ 𝑛 ∈ (𝐴𝑚)) → 𝑛𝑚)
87 eleq1 2814 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = 𝑛 → (𝑦𝑚𝑛𝑚))
8886, 87syl5ibrcom 246 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐴𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴𝑚)) ∧ 𝑛 ∈ (𝐴𝑚)) → (𝑦 = 𝑛𝑦𝑚))
8983, 88mtod 197 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴𝑚)) ∧ 𝑛 ∈ (𝐴𝑚)) → ¬ 𝑦 = 𝑛)
9089, 58syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴𝑚)) ∧ 𝑛 ∈ (𝐴𝑚)) → if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) = (𝐹𝑦))
9190iineq2dv 5026 . . . . . . . . . . . . . . . . . . . 20 (((𝐴𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴𝑚)) → 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) = 𝑛 ∈ (𝐴𝑚) (𝐹𝑦))
92 iinconst 5011 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴𝑚) ≠ ∅ → 𝑛 ∈ (𝐴𝑚) (𝐹𝑦) = (𝐹𝑦))
9392adantr 479 . . . . . . . . . . . . . . . . . . . 20 (((𝐴𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴𝑚)) → 𝑛 ∈ (𝐴𝑚) (𝐹𝑦) = (𝐹𝑦))
9491, 93eqtr2d 2767 . . . . . . . . . . . . . . . . . . 19 (((𝐴𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴𝑚)) → (𝐹𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
95 eqeq1 2730 . . . . . . . . . . . . . . . . . . 19 ((𝑦) = (𝐹𝑦) → ((𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ↔ (𝐹𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦))))
9694, 95syl5ibrcom 246 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴𝑚)) → ((𝑦) = (𝐹𝑦) → (𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦))))
9796ralimdva 3157 . . . . . . . . . . . . . . . . 17 ((𝐴𝑚) ≠ ∅ → (∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦) → ∀𝑦 ∈ (𝐴𝑚)(𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦))))
984, 97mpan9 505 . . . . . . . . . . . . . . . 16 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → ∀𝑦 ∈ (𝐴𝑚)(𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
99 inundif 4483 . . . . . . . . . . . . . . . . . 18 ((𝐴𝑚) ∪ (𝐴𝑚)) = 𝐴
10099raleqi 3313 . . . . . . . . . . . . . . . . 17 (∀𝑦 ∈ ((𝐴𝑚) ∪ (𝐴𝑚))(𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ↔ ∀𝑦𝐴 (𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
101 ralunb 4192 . . . . . . . . . . . . . . . . 17 (∀𝑦 ∈ ((𝐴𝑚) ∪ (𝐴𝑚))(𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ↔ (∀𝑦 ∈ (𝐴𝑚)(𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦))))
102100, 101bitr3i 276 . . . . . . . . . . . . . . . 16 (∀𝑦𝐴 (𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ↔ (∀𝑦 ∈ (𝐴𝑚)(𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦))))
10381, 98, 102sylanbrc 581 . . . . . . . . . . . . . . 15 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → ∀𝑦𝐴 (𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
104 ixpeq2 8940 . . . . . . . . . . . . . . 15 (∀𝑦𝐴 (𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) → X𝑦𝐴 (𝑦) = X𝑦𝐴 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
105103, 104syl 17 . . . . . . . . . . . . . 14 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → X𝑦𝐴 (𝑦) = X𝑦𝐴 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
106 ixpiin 8953 . . . . . . . . . . . . . . 15 ((𝐴𝑚) ≠ ∅ → X𝑦𝐴 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) = 𝑛 ∈ (𝐴𝑚)X𝑦𝐴 if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
107106adantl 480 . . . . . . . . . . . . . 14 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → X𝑦𝐴 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) = 𝑛 ∈ (𝐴𝑚)X𝑦𝐴 if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
108105, 107eqtrd 2766 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → X𝑦𝐴 (𝑦) = 𝑛 ∈ (𝐴𝑚)X𝑦𝐴 if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
10939, 53, 1083eqtr4rd 2777 . . . . . . . . . . . 12 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → X𝑦𝐴 (𝑦) = (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))))
11025, 109pm2.61dane 3019 . . . . . . . . . . 11 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → X𝑦𝐴 (𝑦) = (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))))
111 ixpexg 8951 . . . . . . . . . . . . . . . . . . . . . . . 24 (∀𝑛𝐴 (𝐹𝑛) ∈ V → X𝑛𝐴 (𝐹𝑛) ∈ V)
112 fvex 6914 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐹𝑛) ∈ V
113112uniex 7752 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐹𝑛) ∈ V
114113a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛𝐴 (𝐹𝑛) ∈ V)
115111, 114mprg 3057 . . . . . . . . . . . . . . . . . . . . . . 23 X𝑛𝐴 (𝐹𝑛) ∈ V
11610, 115eqeltri 2822 . . . . . . . . . . . . . . . . . . . . . 22 𝑋 ∈ V
117116mptex 7240 . . . . . . . . . . . . . . . . . . . . 21 (𝑤𝑋 ↦ (𝑤𝑛)) ∈ V
118117cnvex 7938 . . . . . . . . . . . . . . . . . . . 20 (𝑤𝑋 ↦ (𝑤𝑛)) ∈ V
119118imaex 7927 . . . . . . . . . . . . . . . . . . 19 ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ∈ V
120119dfiin2 5042 . . . . . . . . . . . . . . . . . 18 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) = {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))}
121 inteq 4957 . . . . . . . . . . . . . . . . . 18 ({𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} = ∅ → {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} = ∅)
122120, 121eqtrid 2778 . . . . . . . . . . . . . . . . 17 ({𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} = ∅ → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) = ∅)
123 int0 4970 . . . . . . . . . . . . . . . . 17 ∅ = V
124122, 123eqtrdi 2782 . . . . . . . . . . . . . . . 16 ({𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} = ∅ → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) = V)
125124ineq2d 4213 . . . . . . . . . . . . . . 15 ({𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} = ∅ → (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) = (𝑋 ∩ V))
126 inv1 4399 . . . . . . . . . . . . . . 15 (𝑋 ∩ V) = 𝑋
127125, 126eqtrdi 2782 . . . . . . . . . . . . . 14 ({𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} = ∅ → (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) = 𝑋)
128127adantl 480 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} = ∅) → (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) = 𝑋)
129 snex 5437 . . . . . . . . . . . . . . . . . 18 {𝑋} ∈ V
1301ptbas 23574 . . . . . . . . . . . . . . . . . . 19 ((𝐴𝑉𝐹:𝐴⟶Top) → 𝐵 ∈ TopBases)
1311, 10ptpjpre2 23575 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝑘𝐴𝑢 ∈ (𝐹𝑘))) → ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) ∈ 𝐵)
132131ralrimivva 3191 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴𝑉𝐹:𝐴⟶Top) → ∀𝑘𝐴𝑢 ∈ (𝐹𝑘)((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) ∈ 𝐵)
133 eqid 2726 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)) = (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))
134133fmpox 8081 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑘𝐴𝑢 ∈ (𝐹𝑘)((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) ∈ 𝐵 ↔ (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)): 𝑘𝐴 ({𝑘} × (𝐹𝑘))⟶𝐵)
135132, 134sylib 217 . . . . . . . . . . . . . . . . . . . 20 ((𝐴𝑉𝐹:𝐴⟶Top) → (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)): 𝑘𝐴 ({𝑘} × (𝐹𝑘))⟶𝐵)
136135frnd 6736 . . . . . . . . . . . . . . . . . . 19 ((𝐴𝑉𝐹:𝐴⟶Top) → ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)) ⊆ 𝐵)
137130, 136ssexd 5329 . . . . . . . . . . . . . . . . . 18 ((𝐴𝑉𝐹:𝐴⟶Top) → ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)) ∈ V)
138 unexg 7757 . . . . . . . . . . . . . . . . . 18 (({𝑋} ∈ V ∧ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)) ∈ V) → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ∈ V)
139129, 137, 138sylancr 585 . . . . . . . . . . . . . . . . 17 ((𝐴𝑉𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ∈ V)
140 ssfii 9462 . . . . . . . . . . . . . . . . 17 (({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ∈ V → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ⊆ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
141139, 140syl 17 . . . . . . . . . . . . . . . 16 ((𝐴𝑉𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ⊆ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
142141ad2antrr 724 . . . . . . . . . . . . . . 15 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ⊆ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
143 ssun1 4173 . . . . . . . . . . . . . . . . 17 {𝑋} ⊆ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))
144116snss 4794 . . . . . . . . . . . . . . . . 17 (𝑋 ∈ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ↔ {𝑋} ⊆ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))
145143, 144mpbir 230 . . . . . . . . . . . . . . . 16 𝑋 ∈ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))
146145a1i 11 . . . . . . . . . . . . . . 15 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → 𝑋 ∈ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))
147142, 146sseldd 3980 . . . . . . . . . . . . . 14 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → 𝑋 ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
148147adantr 479 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} = ∅) → 𝑋 ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
149128, 148eqeltrd 2826 . . . . . . . . . . . 12 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} = ∅) → (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
150139ad3antrrr 728 . . . . . . . . . . . . . . . . . 18 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ∈ V)
151 nfv 1910 . . . . . . . . . . . . . . . . . . . . . 22 𝑛(((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦)))
152 nfcv 2892 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑛𝐴
153 nfcv 2892 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑛(𝐹𝑘)
154 nfixp1 8947 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑛X𝑛𝐴 (𝐹𝑛)
15510, 154nfcxfr 2890 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑛𝑋
156 nfcv 2892 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑛(𝑤𝑘)
157155, 156nfmpt 5260 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑛(𝑤𝑋 ↦ (𝑤𝑘))
158157nfcnv 5885 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑛(𝑤𝑋 ↦ (𝑤𝑘))
159 nfcv 2892 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑛𝑢
160158, 159nfima 6077 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑛((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)
161152, 153, 160nfmpo 7507 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑛(𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))
162161nfrn 5958 . . . . . . . . . . . . . . . . . . . . . . 23 𝑛ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))
163162nfcri 2883 . . . . . . . . . . . . . . . . . . . . . 22 𝑛 𝑧 ∈ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))
164 df-ov 7427 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛(𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))(𝑛)) = ((𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))‘⟨𝑛, (𝑛)⟩)
165119a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ∈ V)
166 fveq2 6901 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑘 = 𝑛 → (𝑤𝑘) = (𝑤𝑛))
167166mpteq2dv 5255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 = 𝑛 → (𝑤𝑋 ↦ (𝑤𝑘)) = (𝑤𝑋 ↦ (𝑤𝑛)))
168167cnveqd 5882 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑘 = 𝑛(𝑤𝑋 ↦ (𝑤𝑘)) = (𝑤𝑋 ↦ (𝑤𝑛)))
169168imaeq1d 6068 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘 = 𝑛 → ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) = ((𝑤𝑋 ↦ (𝑤𝑛)) “ 𝑢))
170 imaeq2 6065 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑢 = (𝑛) → ((𝑤𝑋 ↦ (𝑤𝑛)) “ 𝑢) = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
171169, 170sylan9eq 2786 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑘 = 𝑛𝑢 = (𝑛)) → ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
172 fveq2 6901 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑘 = 𝑛 → (𝐹𝑘) = (𝐹𝑛))
173171, 172, 133ovmpox 7579 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑛𝐴 ∧ (𝑛) ∈ (𝐹𝑛) ∧ ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ∈ V) → (𝑛(𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))(𝑛)) = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
17429, 35, 165, 173syl3anc 1368 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → (𝑛(𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))(𝑛)) = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
175164, 174eqtr3id 2780 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → ((𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))‘⟨𝑛, (𝑛)⟩) = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
176135ad3antrrr 728 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)): 𝑘𝐴 ({𝑘} × (𝐹𝑘))⟶𝐵)
177176ffnd 6729 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)) Fn 𝑘𝐴 ({𝑘} × (𝐹𝑘)))
178 opeliunxp 5749 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (⟨𝑛, (𝑛)⟩ ∈ 𝑛𝐴 ({𝑛} × (𝐹𝑛)) ↔ (𝑛𝐴 ∧ (𝑛) ∈ (𝐹𝑛)))
17929, 35, 178sylanbrc 581 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → ⟨𝑛, (𝑛)⟩ ∈ 𝑛𝐴 ({𝑛} × (𝐹𝑛)))
180 sneq 4643 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 = 𝑘 → {𝑛} = {𝑘})
181 fveq2 6901 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 = 𝑘 → (𝐹𝑛) = (𝐹𝑘))
182180, 181xpeq12d 5713 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 = 𝑘 → ({𝑛} × (𝐹𝑛)) = ({𝑘} × (𝐹𝑘)))
183182cbviunv 5048 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑛𝐴 ({𝑛} × (𝐹𝑛)) = 𝑘𝐴 ({𝑘} × (𝐹𝑘))
184179, 183eleqtrdi 2836 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → ⟨𝑛, (𝑛)⟩ ∈ 𝑘𝐴 ({𝑘} × (𝐹𝑘)))
185 fnfvelrn 7094 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)) Fn 𝑘𝐴 ({𝑘} × (𝐹𝑘)) ∧ ⟨𝑛, (𝑛)⟩ ∈ 𝑘𝐴 ({𝑘} × (𝐹𝑘))) → ((𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))‘⟨𝑛, (𝑛)⟩) ∈ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))
186177, 184, 185syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → ((𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))‘⟨𝑛, (𝑛)⟩) ∈ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))
187175, 186eqeltrrd 2827 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ∈ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))
188 eleq1 2814 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) → (𝑧 ∈ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)) ↔ ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ∈ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))
189187, 188syl5ibrcom 246 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → (𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) → 𝑧 ∈ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))
190189ex 411 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → (𝑛 ∈ (𝐴𝑚) → (𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) → 𝑧 ∈ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
191151, 163, 190rexlimd 3254 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → (∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) → 𝑧 ∈ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))
192191abssdv 4064 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ⊆ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))
193 ssun2 4174 . . . . . . . . . . . . . . . . . . . 20 ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)) ⊆ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))
194192, 193sstrdi 3992 . . . . . . . . . . . . . . . . . . 19 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ⊆ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))
195194adantr 479 . . . . . . . . . . . . . . . . . 18 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ⊆ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))
196 simpr 483 . . . . . . . . . . . . . . . . . 18 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅)
197 simplrl 775 . . . . . . . . . . . . . . . . . . . 20 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → 𝑚 ∈ Fin)
198 ssfi 9211 . . . . . . . . . . . . . . . . . . . 20 ((𝑚 ∈ Fin ∧ (𝐴𝑚) ⊆ 𝑚) → (𝐴𝑚) ∈ Fin)
199197, 84, 198sylancl 584 . . . . . . . . . . . . . . . . . . 19 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → (𝐴𝑚) ∈ Fin)
200 abrexfi 9396 . . . . . . . . . . . . . . . . . . 19 ((𝐴𝑚) ∈ Fin → {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ∈ Fin)
201199, 200syl 17 . . . . . . . . . . . . . . . . . 18 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ∈ Fin)
202 elfir 9458 . . . . . . . . . . . . . . . . . 18 ((({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ∈ V ∧ ({𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ⊆ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅ ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ∈ Fin)) → {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
203150, 195, 196, 201, 202syl13anc 1369 . . . . . . . . . . . . . . . . 17 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
204120, 203eqeltrid 2830 . . . . . . . . . . . . . . . 16 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
205 elssuni 4945 . . . . . . . . . . . . . . . 16 ( 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))) → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
206204, 205syl 17 . . . . . . . . . . . . . . 15 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
207 fiuni 9471 . . . . . . . . . . . . . . . . . 18 (({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ∈ V → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) = (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
208139, 207syl 17 . . . . . . . . . . . . . . . . 17 ((𝐴𝑉𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) = (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
209116pwid 4629 . . . . . . . . . . . . . . . . . . . . . 22 𝑋 ∈ 𝒫 𝑋
210209a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴𝑉𝐹:𝐴⟶Top) → 𝑋 ∈ 𝒫 𝑋)
211210snssd 4818 . . . . . . . . . . . . . . . . . . . 20 ((𝐴𝑉𝐹:𝐴⟶Top) → {𝑋} ⊆ 𝒫 𝑋)
2121ptuni2 23571 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴𝑉𝐹:𝐴⟶Top) → X𝑛𝐴 (𝐹𝑛) = 𝐵)
21310, 212eqtrid 2778 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴𝑉𝐹:𝐴⟶Top) → 𝑋 = 𝐵)
214 eqimss2 4039 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑋 = 𝐵 𝐵𝑋)
215213, 214syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴𝑉𝐹:𝐴⟶Top) → 𝐵𝑋)
216 sspwuni 5108 . . . . . . . . . . . . . . . . . . . . . 22 (𝐵 ⊆ 𝒫 𝑋 𝐵𝑋)
217215, 216sylibr 233 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴𝑉𝐹:𝐴⟶Top) → 𝐵 ⊆ 𝒫 𝑋)
218136, 217sstrd 3990 . . . . . . . . . . . . . . . . . . . 20 ((𝐴𝑉𝐹:𝐴⟶Top) → ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)) ⊆ 𝒫 𝑋)
219211, 218unssd 4187 . . . . . . . . . . . . . . . . . . 19 ((𝐴𝑉𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ⊆ 𝒫 𝑋)
220 sspwuni 5108 . . . . . . . . . . . . . . . . . . 19 (({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ⊆ 𝒫 𝑋 ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ⊆ 𝑋)
221219, 220sylib 217 . . . . . . . . . . . . . . . . . 18 ((𝐴𝑉𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ⊆ 𝑋)
222 elssuni 4945 . . . . . . . . . . . . . . . . . . 19 (𝑋 ∈ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) → 𝑋 ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))
223145, 222mp1i 13 . . . . . . . . . . . . . . . . . 18 ((𝐴𝑉𝐹:𝐴⟶Top) → 𝑋 ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))
224221, 223eqssd 3997 . . . . . . . . . . . . . . . . 17 ((𝐴𝑉𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) = 𝑋)
225208, 224eqtr3d 2768 . . . . . . . . . . . . . . . 16 ((𝐴𝑉𝐹:𝐴⟶Top) → (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))) = 𝑋)
226225ad3antrrr 728 . . . . . . . . . . . . . . 15 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))) = 𝑋)
227206, 226sseqtrd 4020 . . . . . . . . . . . . . 14 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ 𝑋)
228227, 52sylib 217 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) = 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
229228, 204eqeltrd 2826 . . . . . . . . . . . 12 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
230149, 229pm2.61dane 3019 . . . . . . . . . . 11 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
231110, 230eqeltrd 2826 . . . . . . . . . 10 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → X𝑦𝐴 (𝑦) ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
232231rexlimdvaa 3146 . . . . . . . . 9 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) → (∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦) → X𝑦𝐴 (𝑦) ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))))
233232impr 453 . . . . . . . 8 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦)) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → X𝑦𝐴 (𝑦) ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
2343, 233sylan2b 592 . . . . . . 7 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → X𝑦𝐴 (𝑦) ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
235 eleq1 2814 . . . . . . 7 (𝑠 = X𝑦𝐴 (𝑦) → (𝑠 ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))) ↔ X𝑦𝐴 (𝑦) ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))))
236234, 235syl5ibrcom 246 . . . . . 6 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → (𝑠 = X𝑦𝐴 (𝑦) → 𝑠 ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))))
237236expimpd 452 . . . . 5 ((𝐴𝑉𝐹:𝐴⟶Top) → ((( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑦)) → 𝑠 ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))))
238237exlimdv 1929 . . . 4 ((𝐴𝑉𝐹:𝐴⟶Top) → (∃(( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑦)) → 𝑠 ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))))
2392, 238biimtrid 241 . . 3 ((𝐴𝑉𝐹:𝐴⟶Top) → (𝑠𝐵𝑠 ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))))
240239ssrdv 3985 . 2 ((𝐴𝑉𝐹:𝐴⟶Top) → 𝐵 ⊆ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
2411ptbasid 23570 . . . . . . 7 ((𝐴𝑉𝐹:𝐴⟶Top) → X𝑛𝐴 (𝐹𝑛) ∈ 𝐵)
24210, 241eqeltrid 2830 . . . . . 6 ((𝐴𝑉𝐹:𝐴⟶Top) → 𝑋𝐵)
243242snssd 4818 . . . . 5 ((𝐴𝑉𝐹:𝐴⟶Top) → {𝑋} ⊆ 𝐵)
244243, 136unssd 4187 . . . 4 ((𝐴𝑉𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ⊆ 𝐵)
245 fiss 9467 . . . 4 ((𝐵 ∈ TopBases ∧ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ⊆ 𝐵) → (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))) ⊆ (fi‘𝐵))
246130, 244, 245syl2anc 582 . . 3 ((𝐴𝑉𝐹:𝐴⟶Top) → (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))) ⊆ (fi‘𝐵))
2471ptbasin2 23573 . . 3 ((𝐴𝑉𝐹:𝐴⟶Top) → (fi‘𝐵) = 𝐵)
248246, 247sseqtrd 4020 . 2 ((𝐴𝑉𝐹:𝐴⟶Top) → (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))) ⊆ 𝐵)
249240, 248eqssd 3997 1 ((𝐴𝑉𝐹:𝐴⟶Top) → 𝐵 = (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 394  w3a 1084   = wceq 1534  wex 1774  wcel 2099  {cab 2703  wne 2930  wral 3051  wrex 3060  Vcvv 3462  cdif 3944  cun 3945  cin 3946  wss 3947  c0 4325  ifcif 4533  𝒫 cpw 4607  {csn 4633  cop 4639   cuni 4913   cint 4954   ciun 5001   ciin 5002  cmpt 5236   × cxp 5680  ccnv 5681  dom cdm 5682  ran crn 5683  cima 5685   Fn wfn 6549  wf 6550  cfv 6554  (class class class)co 7424  cmpo 7426  Xcixp 8926  Fincfn 8974  ficfi 9453  Topctop 22886  TopBasesctb 22939
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-rep 5290  ax-sep 5304  ax-nul 5311  ax-pow 5369  ax-pr 5433  ax-un 7746
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-ral 3052  df-rex 3061  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3967  df-nul 4326  df-if 4534  df-pw 4609  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-int 4955  df-iun 5003  df-iin 5004  df-br 5154  df-opab 5216  df-mpt 5237  df-tr 5271  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-ord 6379  df-on 6380  df-lim 6381  df-suc 6382  df-iota 6506  df-fun 6556  df-fn 6557  df-f 6558  df-f1 6559  df-fo 6560  df-f1o 6561  df-fv 6562  df-ov 7427  df-oprab 7428  df-mpo 7429  df-om 7877  df-1st 8003  df-2nd 8004  df-1o 8496  df-2o 8497  df-ixp 8927  df-en 8975  df-dom 8976  df-fin 8978  df-fi 9454  df-top 22887  df-bases 22940
This theorem is referenced by:  ptval2  23596  xkoptsub  23649  ptcmplem1  24047  prdsxmslem2  24529
  Copyright terms: Public domain W3C validator