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

Theorem ptbasfi 22830
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 22821 . . . 4 (𝑠𝐵 ↔ ∃(( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑦)))
3 df-3an 1088 . . . . . . . 8 (( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦)) ↔ (( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦)) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦)))
4 simprr 770 . . . . . . . . . . . . . 14 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))
5 disjdif2 4425 . . . . . . . . . . . . . . . . . 18 ((𝐴𝑚) = ∅ → (𝐴𝑚) = 𝐴)
65raleqdv 3309 . . . . . . . . . . . . . . . . 17 ((𝐴𝑚) = ∅ → (∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦) ↔ ∀𝑦𝐴 (𝑦) = (𝐹𝑦)))
76biimpac 479 . . . . . . . . . . . . . . . 16 ((∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦) ∧ (𝐴𝑚) = ∅) → ∀𝑦𝐴 (𝑦) = (𝐹𝑦))
8 ixpeq2 8762 . . . . . . . . . . . . . . . 16 (∀𝑦𝐴 (𝑦) = (𝐹𝑦) → X𝑦𝐴 (𝑦) = X𝑦𝐴 (𝐹𝑦))
97, 8syl 17 . . . . . . . . . . . . . . 15 ((∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦) ∧ (𝐴𝑚) = ∅) → X𝑦𝐴 (𝑦) = X𝑦𝐴 (𝐹𝑦))
10 ptbasfi.2 . . . . . . . . . . . . . . . 16 𝑋 = X𝑛𝐴 (𝐹𝑛)
11 fveq2 6819 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑦 → (𝐹𝑛) = (𝐹𝑦))
1211unieqd 4865 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑦 (𝐹𝑛) = (𝐹𝑦))
1312cbvixpv 8766 . . . . . . . . . . . . . . . 16 X𝑛𝐴 (𝐹𝑛) = X𝑦𝐴 (𝐹𝑦)
1410, 13eqtri 2764 . . . . . . . . . . . . . . 15 𝑋 = X𝑦𝐴 (𝐹𝑦)
159, 14eqtr4di 2794 . . . . . . . . . . . . . 14 ((∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦) ∧ (𝐴𝑚) = ∅) → X𝑦𝐴 (𝑦) = 𝑋)
164, 15sylan 580 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) = ∅) → X𝑦𝐴 (𝑦) = 𝑋)
17 ssv 3955 . . . . . . . . . . . . . . . 16 𝑋 ⊆ V
18 iineq1 4955 . . . . . . . . . . . . . . . . 17 ((𝐴𝑚) = ∅ → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) = 𝑛 ∈ ∅ ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
19 0iin 5008 . . . . . . . . . . . . . . . . 17 𝑛 ∈ ∅ ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) = V
2018, 19eqtrdi 2792 . . . . . . . . . . . . . . . 16 ((𝐴𝑚) = ∅ → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) = V)
2117, 20sseqtrrid 3984 . . . . . . . . . . . . . . 15 ((𝐴𝑚) = ∅ → 𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
2221adantl 482 . . . . . . . . . . . . . 14 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) = ∅) → 𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
23 df-ss 3914 . . . . . . . . . . . . . 14 (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ↔ (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) = 𝑋)
2422, 23sylib 217 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) = ∅) → (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) = 𝑋)
2516, 24eqtr4d 2779 . . . . . . . . . . . 12 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) = ∅) → X𝑦𝐴 (𝑦) = (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))))
26 simplll 772 . . . . . . . . . . . . . . . 16 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → (𝐴𝑉𝐹:𝐴⟶Top))
27 inss1 4174 . . . . . . . . . . . . . . . . 17 (𝐴𝑚) ⊆ 𝐴
28 simpr 485 . . . . . . . . . . . . . . . . 17 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → 𝑛 ∈ (𝐴𝑚))
2927, 28sselid 3929 . . . . . . . . . . . . . . . 16 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → 𝑛𝐴)
30 fveq2 6819 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑛 → (𝑦) = (𝑛))
31 fveq2 6819 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑛 → (𝐹𝑦) = (𝐹𝑛))
3230, 31eleq12d 2831 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑛 → ((𝑦) ∈ (𝐹𝑦) ↔ (𝑛) ∈ (𝐹𝑛)))
33 simprr 770 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) → ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))
3433ad2antrr 723 . . . . . . . . . . . . . . . . 17 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))
3532, 34, 29rspcdva 3571 . . . . . . . . . . . . . . . 16 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → (𝑛) ∈ (𝐹𝑛))
3614ptpjpre1 22820 . . . . . . . . . . . . . . . 16 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝑛𝐴 ∧ (𝑛) ∈ (𝐹𝑛))) → ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) = X𝑦𝐴 if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
3726, 29, 35, 36syl12anc 834 . . . . . . . . . . . . . . 15 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) = X𝑦𝐴 if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
3837adantlr 712 . . . . . . . . . . . . . 14 ((((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) ∧ 𝑛 ∈ (𝐴𝑚)) → ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) = X𝑦𝐴 if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
3938iineq2dv 4963 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) = 𝑛 ∈ (𝐴𝑚)X𝑦𝐴 if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
40 simpr 485 . . . . . . . . . . . . . . . . 17 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → (𝐴𝑚) ≠ ∅)
41 cnvimass 6013 . . . . . . . . . . . . . . . . . . . 20 ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ dom (𝑤𝑋 ↦ (𝑤𝑛))
42 eqid 2736 . . . . . . . . . . . . . . . . . . . . 21 (𝑤𝑋 ↦ (𝑤𝑛)) = (𝑤𝑋 ↦ (𝑤𝑛))
4342dmmptss 6173 . . . . . . . . . . . . . . . . . . . 20 dom (𝑤𝑋 ↦ (𝑤𝑛)) ⊆ 𝑋
4441, 43sstri 3940 . . . . . . . . . . . . . . . . . . 19 ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ 𝑋
4544, 14sseqtri 3967 . . . . . . . . . . . . . . . . . 18 ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ X𝑦𝐴 (𝐹𝑦)
4645rgenw 3065 . . . . . . . . . . . . . . . . 17 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ X𝑦𝐴 (𝐹𝑦)
47 r19.2z 4438 . . . . . . . . . . . . . . . . 17 (((𝐴𝑚) ≠ ∅ ∧ ∀𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ X𝑦𝐴 (𝐹𝑦)) → ∃𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ X𝑦𝐴 (𝐹𝑦))
4840, 46, 47sylancl 586 . . . . . . . . . . . . . . . 16 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → ∃𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ X𝑦𝐴 (𝐹𝑦))
49 iinss 5000 . . . . . . . . . . . . . . . 16 (∃𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ X𝑦𝐴 (𝐹𝑦) → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ X𝑦𝐴 (𝐹𝑦))
5048, 49syl 17 . . . . . . . . . . . . . . 15 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ X𝑦𝐴 (𝐹𝑦))
5150, 14sseqtrrdi 3982 . . . . . . . . . . . . . 14 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ 𝑋)
52 sseqin2 4161 . . . . . . . . . . . . . 14 ( 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ 𝑋 ↔ (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) = 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
5351, 52sylib 217 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) = 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
5433ad2antrr 723 . . . . . . . . . . . . . . . . 17 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))
55 ssralv 3997 . . . . . . . . . . . . . . . . . 18 ((𝐴𝑚) ⊆ 𝐴 → (∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦) → ∀𝑦 ∈ (𝐴𝑚)(𝑦) ∈ (𝐹𝑦)))
5627, 55ax-mp 5 . . . . . . . . . . . . . . . . 17 (∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦) → ∀𝑦 ∈ (𝐴𝑚)(𝑦) ∈ (𝐹𝑦))
57 elssuni 4884 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑦) ∈ (𝐹𝑦) → (𝑦) ⊆ (𝐹𝑦))
58 iffalse 4481 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑦 = 𝑛 → if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) = (𝐹𝑦))
5958sseq2d 3963 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑦 = 𝑛 → ((𝑦) ⊆ if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ↔ (𝑦) ⊆ (𝐹𝑦)))
6057, 59syl5ibrcom 246 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦) ∈ (𝐹𝑦) → (¬ 𝑦 = 𝑛 → (𝑦) ⊆ if(𝑦 = 𝑛, (𝑛), (𝐹𝑦))))
61 ssid 3953 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦) ⊆ (𝑦)
62 iftrue 4478 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑛 → if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) = (𝑛))
6362, 30eqtr4d 2779 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = 𝑛 → if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) = (𝑦))
6461, 63sseqtrrid 3984 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = 𝑛 → (𝑦) ⊆ if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
6560, 64pm2.61d2 181 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦) ∈ (𝐹𝑦) → (𝑦) ⊆ if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
6665ralrimivw 3143 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦) ∈ (𝐹𝑦) → ∀𝑛 ∈ (𝐴𝑚)(𝑦) ⊆ if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
67 ssiin 4999 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦) ⊆ 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ↔ ∀𝑛 ∈ (𝐴𝑚)(𝑦) ⊆ if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
6866, 67sylibr 233 . . . . . . . . . . . . . . . . . . . 20 ((𝑦) ∈ (𝐹𝑦) → (𝑦) ⊆ 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
6968adantl 482 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ (𝐴𝑚) ∧ (𝑦) ∈ (𝐹𝑦)) → (𝑦) ⊆ 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
7062equcoms 2022 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = 𝑦 → if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) = (𝑛))
71 fveq2 6819 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = 𝑦 → (𝑛) = (𝑦))
7270, 71eqtrd 2776 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝑦 → if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) = (𝑦))
7372sseq1d 3962 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑦 → (if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ⊆ (𝑦) ↔ (𝑦) ⊆ (𝑦)))
7473rspcev 3570 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 ∈ (𝐴𝑚) ∧ (𝑦) ⊆ (𝑦)) → ∃𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ⊆ (𝑦))
7561, 74mpan2 688 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ (𝐴𝑚) → ∃𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ⊆ (𝑦))
76 iinss 5000 . . . . . . . . . . . . . . . . . . . . 21 (∃𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ⊆ (𝑦) → 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ⊆ (𝑦))
7775, 76syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (𝐴𝑚) → 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ⊆ (𝑦))
7877adantr 481 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ (𝐴𝑚) ∧ (𝑦) ∈ (𝐹𝑦)) → 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ⊆ (𝑦))
7969, 78eqssd 3948 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ (𝐴𝑚) ∧ (𝑦) ∈ (𝐹𝑦)) → (𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
8079ralimiaa 3081 . . . . . . . . . . . . . . . . 17 (∀𝑦 ∈ (𝐴𝑚)(𝑦) ∈ (𝐹𝑦) → ∀𝑦 ∈ (𝐴𝑚)(𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
8154, 56, 803syl 18 . . . . . . . . . . . . . . . 16 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → ∀𝑦 ∈ (𝐴𝑚)(𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
82 eldifn 4073 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ (𝐴𝑚) → ¬ 𝑦𝑚)
8382ad2antlr 724 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐴𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴𝑚)) ∧ 𝑛 ∈ (𝐴𝑚)) → ¬ 𝑦𝑚)
84 inss2 4175 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴𝑚) ⊆ 𝑚
85 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐴𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴𝑚)) ∧ 𝑛 ∈ (𝐴𝑚)) → 𝑛 ∈ (𝐴𝑚))
8684, 85sselid 3929 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐴𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴𝑚)) ∧ 𝑛 ∈ (𝐴𝑚)) → 𝑛𝑚)
87 eleq1 2824 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = 𝑛 → (𝑦𝑚𝑛𝑚))
8886, 87syl5ibrcom 246 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐴𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴𝑚)) ∧ 𝑛 ∈ (𝐴𝑚)) → (𝑦 = 𝑛𝑦𝑚))
8983, 88mtod 197 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴𝑚)) ∧ 𝑛 ∈ (𝐴𝑚)) → ¬ 𝑦 = 𝑛)
9089, 58syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴𝑚)) ∧ 𝑛 ∈ (𝐴𝑚)) → if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) = (𝐹𝑦))
9190iineq2dv 4963 . . . . . . . . . . . . . . . . . . . 20 (((𝐴𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴𝑚)) → 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) = 𝑛 ∈ (𝐴𝑚) (𝐹𝑦))
92 iinconst 4948 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴𝑚) ≠ ∅ → 𝑛 ∈ (𝐴𝑚) (𝐹𝑦) = (𝐹𝑦))
9392adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((𝐴𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴𝑚)) → 𝑛 ∈ (𝐴𝑚) (𝐹𝑦) = (𝐹𝑦))
9491, 93eqtr2d 2777 . . . . . . . . . . . . . . . . . . 19 (((𝐴𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴𝑚)) → (𝐹𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
95 eqeq1 2740 . . . . . . . . . . . . . . . . . . 19 ((𝑦) = (𝐹𝑦) → ((𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ↔ (𝐹𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦))))
9694, 95syl5ibrcom 246 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴𝑚)) → ((𝑦) = (𝐹𝑦) → (𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦))))
9796ralimdva 3160 . . . . . . . . . . . . . . . . 17 ((𝐴𝑚) ≠ ∅ → (∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦) → ∀𝑦 ∈ (𝐴𝑚)(𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦))))
984, 97mpan9 507 . . . . . . . . . . . . . . . 16 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → ∀𝑦 ∈ (𝐴𝑚)(𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
99 inundif 4424 . . . . . . . . . . . . . . . . . 18 ((𝐴𝑚) ∪ (𝐴𝑚)) = 𝐴
10099raleqi 3307 . . . . . . . . . . . . . . . . 17 (∀𝑦 ∈ ((𝐴𝑚) ∪ (𝐴𝑚))(𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ↔ ∀𝑦𝐴 (𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
101 ralunb 4137 . . . . . . . . . . . . . . . . 17 (∀𝑦 ∈ ((𝐴𝑚) ∪ (𝐴𝑚))(𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ↔ (∀𝑦 ∈ (𝐴𝑚)(𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦))))
102100, 101bitr3i 276 . . . . . . . . . . . . . . . 16 (∀𝑦𝐴 (𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ↔ (∀𝑦 ∈ (𝐴𝑚)(𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦))))
10381, 98, 102sylanbrc 583 . . . . . . . . . . . . . . 15 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → ∀𝑦𝐴 (𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
104 ixpeq2 8762 . . . . . . . . . . . . . . 15 (∀𝑦𝐴 (𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) → X𝑦𝐴 (𝑦) = X𝑦𝐴 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
105103, 104syl 17 . . . . . . . . . . . . . 14 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → X𝑦𝐴 (𝑦) = X𝑦𝐴 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
106 ixpiin 8775 . . . . . . . . . . . . . . 15 ((𝐴𝑚) ≠ ∅ → X𝑦𝐴 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) = 𝑛 ∈ (𝐴𝑚)X𝑦𝐴 if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
107106adantl 482 . . . . . . . . . . . . . 14 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → X𝑦𝐴 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) = 𝑛 ∈ (𝐴𝑚)X𝑦𝐴 if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
108105, 107eqtrd 2776 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → X𝑦𝐴 (𝑦) = 𝑛 ∈ (𝐴𝑚)X𝑦𝐴 if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
10939, 53, 1083eqtr4rd 2787 . . . . . . . . . . . 12 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → X𝑦𝐴 (𝑦) = (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))))
11025, 109pm2.61dane 3029 . . . . . . . . . . 11 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → X𝑦𝐴 (𝑦) = (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))))
111 ixpexg 8773 . . . . . . . . . . . . . . . . . . . . . . . 24 (∀𝑛𝐴 (𝐹𝑛) ∈ V → X𝑛𝐴 (𝐹𝑛) ∈ V)
112 fvex 6832 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐹𝑛) ∈ V
113112uniex 7648 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐹𝑛) ∈ V
114113a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛𝐴 (𝐹𝑛) ∈ V)
115111, 114mprg 3067 . . . . . . . . . . . . . . . . . . . . . . 23 X𝑛𝐴 (𝐹𝑛) ∈ V
11610, 115eqeltri 2833 . . . . . . . . . . . . . . . . . . . . . 22 𝑋 ∈ V
117116mptex 7149 . . . . . . . . . . . . . . . . . . . . 21 (𝑤𝑋 ↦ (𝑤𝑛)) ∈ V
118117cnvex 7832 . . . . . . . . . . . . . . . . . . . 20 (𝑤𝑋 ↦ (𝑤𝑛)) ∈ V
119118imaex 7823 . . . . . . . . . . . . . . . . . . 19 ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ∈ V
120119dfiin2 4978 . . . . . . . . . . . . . . . . . 18 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) = {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))}
121 inteq 4896 . . . . . . . . . . . . . . . . . 18 ({𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} = ∅ → {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} = ∅)
122120, 121eqtrid 2788 . . . . . . . . . . . . . . . . 17 ({𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} = ∅ → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) = ∅)
123 int0 4907 . . . . . . . . . . . . . . . . 17 ∅ = V
124122, 123eqtrdi 2792 . . . . . . . . . . . . . . . 16 ({𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} = ∅ → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) = V)
125124ineq2d 4158 . . . . . . . . . . . . . . 15 ({𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} = ∅ → (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) = (𝑋 ∩ V))
126 inv1 4340 . . . . . . . . . . . . . . 15 (𝑋 ∩ V) = 𝑋
127125, 126eqtrdi 2792 . . . . . . . . . . . . . 14 ({𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} = ∅ → (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) = 𝑋)
128127adantl 482 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} = ∅) → (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) = 𝑋)
129 snex 5373 . . . . . . . . . . . . . . . . . 18 {𝑋} ∈ V
1301ptbas 22828 . . . . . . . . . . . . . . . . . . 19 ((𝐴𝑉𝐹:𝐴⟶Top) → 𝐵 ∈ TopBases)
1311, 10ptpjpre2 22829 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝑘𝐴𝑢 ∈ (𝐹𝑘))) → ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) ∈ 𝐵)
132131ralrimivva 3193 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴𝑉𝐹:𝐴⟶Top) → ∀𝑘𝐴𝑢 ∈ (𝐹𝑘)((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) ∈ 𝐵)
133 eqid 2736 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)) = (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))
134133fmpox 7967 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑘𝐴𝑢 ∈ (𝐹𝑘)((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) ∈ 𝐵 ↔ (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)): 𝑘𝐴 ({𝑘} × (𝐹𝑘))⟶𝐵)
135132, 134sylib 217 . . . . . . . . . . . . . . . . . . . 20 ((𝐴𝑉𝐹:𝐴⟶Top) → (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)): 𝑘𝐴 ({𝑘} × (𝐹𝑘))⟶𝐵)
136135frnd 6653 . . . . . . . . . . . . . . . . . . 19 ((𝐴𝑉𝐹:𝐴⟶Top) → ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)) ⊆ 𝐵)
137130, 136ssexd 5265 . . . . . . . . . . . . . . . . . 18 ((𝐴𝑉𝐹:𝐴⟶Top) → ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)) ∈ V)
138 unexg 7653 . . . . . . . . . . . . . . . . . 18 (({𝑋} ∈ V ∧ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)) ∈ V) → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ∈ V)
139129, 137, 138sylancr 587 . . . . . . . . . . . . . . . . 17 ((𝐴𝑉𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ∈ V)
140 ssfii 9268 . . . . . . . . . . . . . . . . 17 (({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ∈ V → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ⊆ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
141139, 140syl 17 . . . . . . . . . . . . . . . 16 ((𝐴𝑉𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ⊆ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
142141ad2antrr 723 . . . . . . . . . . . . . . 15 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ⊆ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
143 ssun1 4118 . . . . . . . . . . . . . . . . 17 {𝑋} ⊆ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))
144116snss 4732 . . . . . . . . . . . . . . . . 17 (𝑋 ∈ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ↔ {𝑋} ⊆ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))
145143, 144mpbir 230 . . . . . . . . . . . . . . . 16 𝑋 ∈ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))
146145a1i 11 . . . . . . . . . . . . . . 15 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → 𝑋 ∈ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))
147142, 146sseldd 3932 . . . . . . . . . . . . . 14 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → 𝑋 ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
148147adantr 481 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} = ∅) → 𝑋 ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
149128, 148eqeltrd 2837 . . . . . . . . . . . 12 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} = ∅) → (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
150139ad3antrrr 727 . . . . . . . . . . . . . . . . . 18 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ∈ V)
151 nfv 1916 . . . . . . . . . . . . . . . . . . . . . 22 𝑛(((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦)))
152 nfcv 2904 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑛𝐴
153 nfcv 2904 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑛(𝐹𝑘)
154 nfixp1 8769 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑛X𝑛𝐴 (𝐹𝑛)
15510, 154nfcxfr 2902 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑛𝑋
156 nfcv 2904 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑛(𝑤𝑘)
157155, 156nfmpt 5196 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑛(𝑤𝑋 ↦ (𝑤𝑘))
158157nfcnv 5814 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑛(𝑤𝑋 ↦ (𝑤𝑘))
159 nfcv 2904 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑛𝑢
160158, 159nfima 6001 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑛((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)
161152, 153, 160nfmpo 7411 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑛(𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))
162161nfrn 5887 . . . . . . . . . . . . . . . . . . . . . . 23 𝑛ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))
163162nfcri 2891 . . . . . . . . . . . . . . . . . . . . . 22 𝑛 𝑧 ∈ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))
164 df-ov 7332 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛(𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))(𝑛)) = ((𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))‘⟨𝑛, (𝑛)⟩)
165119a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ∈ V)
166 fveq2 6819 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑘 = 𝑛 → (𝑤𝑘) = (𝑤𝑛))
167166mpteq2dv 5191 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 = 𝑛 → (𝑤𝑋 ↦ (𝑤𝑘)) = (𝑤𝑋 ↦ (𝑤𝑛)))
168167cnveqd 5811 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑘 = 𝑛(𝑤𝑋 ↦ (𝑤𝑘)) = (𝑤𝑋 ↦ (𝑤𝑛)))
169168imaeq1d 5992 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘 = 𝑛 → ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) = ((𝑤𝑋 ↦ (𝑤𝑛)) “ 𝑢))
170 imaeq2 5989 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑢 = (𝑛) → ((𝑤𝑋 ↦ (𝑤𝑛)) “ 𝑢) = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
171169, 170sylan9eq 2796 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑘 = 𝑛𝑢 = (𝑛)) → ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
172 fveq2 6819 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑘 = 𝑛 → (𝐹𝑘) = (𝐹𝑛))
173171, 172, 133ovmpox 7480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑛𝐴 ∧ (𝑛) ∈ (𝐹𝑛) ∧ ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ∈ V) → (𝑛(𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))(𝑛)) = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
17429, 35, 165, 173syl3anc 1370 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → (𝑛(𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))(𝑛)) = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
175164, 174eqtr3id 2790 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → ((𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))‘⟨𝑛, (𝑛)⟩) = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
176135ad3antrrr 727 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)): 𝑘𝐴 ({𝑘} × (𝐹𝑘))⟶𝐵)
177176ffnd 6646 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)) Fn 𝑘𝐴 ({𝑘} × (𝐹𝑘)))
178 opeliunxp 5679 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (⟨𝑛, (𝑛)⟩ ∈ 𝑛𝐴 ({𝑛} × (𝐹𝑛)) ↔ (𝑛𝐴 ∧ (𝑛) ∈ (𝐹𝑛)))
17929, 35, 178sylanbrc 583 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → ⟨𝑛, (𝑛)⟩ ∈ 𝑛𝐴 ({𝑛} × (𝐹𝑛)))
180 sneq 4582 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 = 𝑘 → {𝑛} = {𝑘})
181 fveq2 6819 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 = 𝑘 → (𝐹𝑛) = (𝐹𝑘))
182180, 181xpeq12d 5645 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 = 𝑘 → ({𝑛} × (𝐹𝑛)) = ({𝑘} × (𝐹𝑘)))
183182cbviunv 4984 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑛𝐴 ({𝑛} × (𝐹𝑛)) = 𝑘𝐴 ({𝑘} × (𝐹𝑘))
184179, 183eleqtrdi 2847 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → ⟨𝑛, (𝑛)⟩ ∈ 𝑘𝐴 ({𝑘} × (𝐹𝑘)))
185 fnfvelrn 7008 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)) Fn 𝑘𝐴 ({𝑘} × (𝐹𝑘)) ∧ ⟨𝑛, (𝑛)⟩ ∈ 𝑘𝐴 ({𝑘} × (𝐹𝑘))) → ((𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))‘⟨𝑛, (𝑛)⟩) ∈ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))
186177, 184, 185syl2anc 584 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → ((𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))‘⟨𝑛, (𝑛)⟩) ∈ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))
187175, 186eqeltrrd 2838 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ∈ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))
188 eleq1 2824 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) → (𝑧 ∈ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)) ↔ ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ∈ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))
189187, 188syl5ibrcom 246 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → (𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) → 𝑧 ∈ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))
190189ex 413 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → (𝑛 ∈ (𝐴𝑚) → (𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) → 𝑧 ∈ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
191151, 163, 190rexlimd 3245 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → (∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) → 𝑧 ∈ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))
192191abssdv 4012 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ⊆ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))
193 ssun2 4119 . . . . . . . . . . . . . . . . . . . 20 ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)) ⊆ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))
194192, 193sstrdi 3943 . . . . . . . . . . . . . . . . . . 19 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ⊆ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))
195194adantr 481 . . . . . . . . . . . . . . . . . 18 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ⊆ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))
196 simpr 485 . . . . . . . . . . . . . . . . . 18 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅)
197 simplrl 774 . . . . . . . . . . . . . . . . . . . 20 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → 𝑚 ∈ Fin)
198 ssfi 9030 . . . . . . . . . . . . . . . . . . . 20 ((𝑚 ∈ Fin ∧ (𝐴𝑚) ⊆ 𝑚) → (𝐴𝑚) ∈ Fin)
199197, 84, 198sylancl 586 . . . . . . . . . . . . . . . . . . 19 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → (𝐴𝑚) ∈ Fin)
200 abrexfi 9209 . . . . . . . . . . . . . . . . . . 19 ((𝐴𝑚) ∈ Fin → {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ∈ Fin)
201199, 200syl 17 . . . . . . . . . . . . . . . . . 18 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ∈ Fin)
202 elfir 9264 . . . . . . . . . . . . . . . . . 18 ((({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ∈ V ∧ ({𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ⊆ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅ ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ∈ Fin)) → {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
203150, 195, 196, 201, 202syl13anc 1371 . . . . . . . . . . . . . . . . 17 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
204120, 203eqeltrid 2841 . . . . . . . . . . . . . . . 16 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
205 elssuni 4884 . . . . . . . . . . . . . . . 16 ( 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))) → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
206204, 205syl 17 . . . . . . . . . . . . . . 15 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
207 fiuni 9277 . . . . . . . . . . . . . . . . . 18 (({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ∈ V → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) = (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
208139, 207syl 17 . . . . . . . . . . . . . . . . 17 ((𝐴𝑉𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) = (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
209116pwid 4568 . . . . . . . . . . . . . . . . . . . . . 22 𝑋 ∈ 𝒫 𝑋
210209a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴𝑉𝐹:𝐴⟶Top) → 𝑋 ∈ 𝒫 𝑋)
211210snssd 4755 . . . . . . . . . . . . . . . . . . . 20 ((𝐴𝑉𝐹:𝐴⟶Top) → {𝑋} ⊆ 𝒫 𝑋)
2121ptuni2 22825 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴𝑉𝐹:𝐴⟶Top) → X𝑛𝐴 (𝐹𝑛) = 𝐵)
21310, 212eqtrid 2788 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴𝑉𝐹:𝐴⟶Top) → 𝑋 = 𝐵)
214 eqimss2 3988 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑋 = 𝐵 𝐵𝑋)
215213, 214syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴𝑉𝐹:𝐴⟶Top) → 𝐵𝑋)
216 sspwuni 5044 . . . . . . . . . . . . . . . . . . . . . 22 (𝐵 ⊆ 𝒫 𝑋 𝐵𝑋)
217215, 216sylibr 233 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴𝑉𝐹:𝐴⟶Top) → 𝐵 ⊆ 𝒫 𝑋)
218136, 217sstrd 3941 . . . . . . . . . . . . . . . . . . . 20 ((𝐴𝑉𝐹:𝐴⟶Top) → ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)) ⊆ 𝒫 𝑋)
219211, 218unssd 4132 . . . . . . . . . . . . . . . . . . 19 ((𝐴𝑉𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ⊆ 𝒫 𝑋)
220 sspwuni 5044 . . . . . . . . . . . . . . . . . . 19 (({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ⊆ 𝒫 𝑋 ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ⊆ 𝑋)
221219, 220sylib 217 . . . . . . . . . . . . . . . . . 18 ((𝐴𝑉𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ⊆ 𝑋)
222 elssuni 4884 . . . . . . . . . . . . . . . . . . 19 (𝑋 ∈ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) → 𝑋 ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))
223145, 222mp1i 13 . . . . . . . . . . . . . . . . . 18 ((𝐴𝑉𝐹:𝐴⟶Top) → 𝑋 ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))
224221, 223eqssd 3948 . . . . . . . . . . . . . . . . 17 ((𝐴𝑉𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) = 𝑋)
225208, 224eqtr3d 2778 . . . . . . . . . . . . . . . 16 ((𝐴𝑉𝐹:𝐴⟶Top) → (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))) = 𝑋)
226225ad3antrrr 727 . . . . . . . . . . . . . . 15 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))) = 𝑋)
227206, 226sseqtrd 3971 . . . . . . . . . . . . . 14 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ 𝑋)
228227, 52sylib 217 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) = 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
229228, 204eqeltrd 2837 . . . . . . . . . . . 12 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
230149, 229pm2.61dane 3029 . . . . . . . . . . 11 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
231110, 230eqeltrd 2837 . . . . . . . . . 10 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → X𝑦𝐴 (𝑦) ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
232231rexlimdvaa 3149 . . . . . . . . 9 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) → (∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦) → X𝑦𝐴 (𝑦) ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))))
233232impr 455 . . . . . . . 8 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦)) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → X𝑦𝐴 (𝑦) ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
2343, 233sylan2b 594 . . . . . . 7 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → X𝑦𝐴 (𝑦) ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
235 eleq1 2824 . . . . . . 7 (𝑠 = X𝑦𝐴 (𝑦) → (𝑠 ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))) ↔ X𝑦𝐴 (𝑦) ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))))
236234, 235syl5ibrcom 246 . . . . . 6 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → (𝑠 = X𝑦𝐴 (𝑦) → 𝑠 ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))))
237236expimpd 454 . . . . 5 ((𝐴𝑉𝐹:𝐴⟶Top) → ((( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑦)) → 𝑠 ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))))
238237exlimdv 1935 . . . 4 ((𝐴𝑉𝐹:𝐴⟶Top) → (∃(( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑦)) → 𝑠 ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))))
2392, 238biimtrid 241 . . 3 ((𝐴𝑉𝐹:𝐴⟶Top) → (𝑠𝐵𝑠 ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))))
240239ssrdv 3937 . 2 ((𝐴𝑉𝐹:𝐴⟶Top) → 𝐵 ⊆ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
2411ptbasid 22824 . . . . . . 7 ((𝐴𝑉𝐹:𝐴⟶Top) → X𝑛𝐴 (𝐹𝑛) ∈ 𝐵)
24210, 241eqeltrid 2841 . . . . . 6 ((𝐴𝑉𝐹:𝐴⟶Top) → 𝑋𝐵)
243242snssd 4755 . . . . 5 ((𝐴𝑉𝐹:𝐴⟶Top) → {𝑋} ⊆ 𝐵)
244243, 136unssd 4132 . . . 4 ((𝐴𝑉𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ⊆ 𝐵)
245 fiss 9273 . . . 4 ((𝐵 ∈ TopBases ∧ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ⊆ 𝐵) → (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))) ⊆ (fi‘𝐵))
246130, 244, 245syl2anc 584 . . 3 ((𝐴𝑉𝐹:𝐴⟶Top) → (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))) ⊆ (fi‘𝐵))
2471ptbasin2 22827 . . 3 ((𝐴𝑉𝐹:𝐴⟶Top) → (fi‘𝐵) = 𝐵)
248246, 247sseqtrd 3971 . 2 ((𝐴𝑉𝐹:𝐴⟶Top) → (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))) ⊆ 𝐵)
249240, 248eqssd 3948 1 ((𝐴𝑉𝐹:𝐴⟶Top) → 𝐵 = (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  w3a 1086   = wceq 1540  wex 1780  wcel 2105  {cab 2713  wne 2940  wral 3061  wrex 3070  Vcvv 3441  cdif 3894  cun 3895  cin 3896  wss 3897  c0 4268  ifcif 4472  𝒫 cpw 4546  {csn 4572  cop 4578   cuni 4851   cint 4893   ciun 4938   ciin 4939  cmpt 5172   × cxp 5612  ccnv 5613  dom cdm 5614  ran crn 5615  cima 5617   Fn wfn 6468  wf 6469  cfv 6473  (class class class)co 7329  cmpo 7331  Xcixp 8748  Fincfn 8796  ficfi 9259  Topctop 22140  TopBasesctb 22193
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5226  ax-sep 5240  ax-nul 5247  ax-pow 5305  ax-pr 5369  ax-un 7642
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-nul 4269  df-if 4473  df-pw 4548  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4852  df-int 4894  df-iun 4940  df-iin 4941  df-br 5090  df-opab 5152  df-mpt 5173  df-tr 5207  df-id 5512  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5569  df-we 5571  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-ord 6299  df-on 6300  df-lim 6301  df-suc 6302  df-iota 6425  df-fun 6475  df-fn 6476  df-f 6477  df-f1 6478  df-fo 6479  df-f1o 6480  df-fv 6481  df-ov 7332  df-oprab 7333  df-mpo 7334  df-om 7773  df-1st 7891  df-2nd 7892  df-1o 8359  df-er 8561  df-ixp 8749  df-en 8797  df-dom 8798  df-fin 8800  df-fi 9260  df-top 22141  df-bases 22194
This theorem is referenced by:  ptval2  22850  xkoptsub  22903  ptcmplem1  23301  prdsxmslem2  23783
  Copyright terms: Public domain W3C validator