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

Theorem ptbasfi 21604
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 21595 . . . 4 (𝑠𝐵 ↔ ∃(( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑦)))
3 df-3an 1073 . . . . . . . 8 (( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦)) ↔ (( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦)) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦)))
4 simprr 756 . . . . . . . . . . . . . 14 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))
5 disjdif2 4190 . . . . . . . . . . . . . . . . . 18 ((𝐴𝑚) = ∅ → (𝐴𝑚) = 𝐴)
65raleqdv 3293 . . . . . . . . . . . . . . . . 17 ((𝐴𝑚) = ∅ → (∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦) ↔ ∀𝑦𝐴 (𝑦) = (𝐹𝑦)))
76biimpac 464 . . . . . . . . . . . . . . . 16 ((∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦) ∧ (𝐴𝑚) = ∅) → ∀𝑦𝐴 (𝑦) = (𝐹𝑦))
8 ixpeq2 8079 . . . . . . . . . . . . . . . 16 (∀𝑦𝐴 (𝑦) = (𝐹𝑦) → X𝑦𝐴 (𝑦) = X𝑦𝐴 (𝐹𝑦))
97, 8syl 17 . . . . . . . . . . . . . . 15 ((∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦) ∧ (𝐴𝑚) = ∅) → X𝑦𝐴 (𝑦) = X𝑦𝐴 (𝐹𝑦))
10 ptbasfi.2 . . . . . . . . . . . . . . . 16 𝑋 = X𝑛𝐴 (𝐹𝑛)
11 fveq2 6333 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑦 → (𝐹𝑛) = (𝐹𝑦))
1211unieqd 4585 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑦 (𝐹𝑛) = (𝐹𝑦))
1312cbvixpv 8083 . . . . . . . . . . . . . . . 16 X𝑛𝐴 (𝐹𝑛) = X𝑦𝐴 (𝐹𝑦)
1410, 13eqtri 2793 . . . . . . . . . . . . . . 15 𝑋 = X𝑦𝐴 (𝐹𝑦)
159, 14syl6eqr 2823 . . . . . . . . . . . . . 14 ((∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦) ∧ (𝐴𝑚) = ∅) → X𝑦𝐴 (𝑦) = 𝑋)
164, 15sylan 569 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) = ∅) → X𝑦𝐴 (𝑦) = 𝑋)
17 ssv 3774 . . . . . . . . . . . . . . . 16 𝑋 ⊆ V
18 iineq1 4670 . . . . . . . . . . . . . . . . 17 ((𝐴𝑚) = ∅ → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) = 𝑛 ∈ ∅ ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
19 0iin 4713 . . . . . . . . . . . . . . . . 17 𝑛 ∈ ∅ ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) = V
2018, 19syl6eq 2821 . . . . . . . . . . . . . . . 16 ((𝐴𝑚) = ∅ → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) = V)
2117, 20syl5sseqr 3803 . . . . . . . . . . . . . . 15 ((𝐴𝑚) = ∅ → 𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
2221adantl 467 . . . . . . . . . . . . . 14 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) = ∅) → 𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
23 df-ss 3737 . . . . . . . . . . . . . 14 (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ↔ (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) = 𝑋)
2422, 23sylib 208 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) = ∅) → (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) = 𝑋)
2516, 24eqtr4d 2808 . . . . . . . . . . . 12 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) = ∅) → X𝑦𝐴 (𝑦) = (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))))
26 simplll 758 . . . . . . . . . . . . . . . 16 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → (𝐴𝑉𝐹:𝐴⟶Top))
27 inss1 3981 . . . . . . . . . . . . . . . . 17 (𝐴𝑚) ⊆ 𝐴
28 simpr 471 . . . . . . . . . . . . . . . . 17 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → 𝑛 ∈ (𝐴𝑚))
2927, 28sseldi 3750 . . . . . . . . . . . . . . . 16 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → 𝑛𝐴)
30 fveq2 6333 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑛 → (𝑦) = (𝑛))
31 fveq2 6333 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑛 → (𝐹𝑦) = (𝐹𝑛))
3230, 31eleq12d 2844 . . . . . . . . . . . . . . . . 17 (𝑦 = 𝑛 → ((𝑦) ∈ (𝐹𝑦) ↔ (𝑛) ∈ (𝐹𝑛)))
33 simprr 756 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) → ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))
3433ad2antrr 705 . . . . . . . . . . . . . . . . 17 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))
3532, 34, 29rspcdva 3466 . . . . . . . . . . . . . . . 16 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → (𝑛) ∈ (𝐹𝑛))
3614ptpjpre1 21594 . . . . . . . . . . . . . . . 16 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝑛𝐴 ∧ (𝑛) ∈ (𝐹𝑛))) → ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) = X𝑦𝐴 if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
3726, 29, 35, 36syl12anc 1474 . . . . . . . . . . . . . . 15 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) = X𝑦𝐴 if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
3837adantlr 694 . . . . . . . . . . . . . 14 ((((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) ∧ 𝑛 ∈ (𝐴𝑚)) → ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) = X𝑦𝐴 if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
3938iineq2dv 4678 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) = 𝑛 ∈ (𝐴𝑚)X𝑦𝐴 if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
40 simpr 471 . . . . . . . . . . . . . . . . 17 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → (𝐴𝑚) ≠ ∅)
41 cnvimass 5625 . . . . . . . . . . . . . . . . . . . 20 ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ dom (𝑤𝑋 ↦ (𝑤𝑛))
42 eqid 2771 . . . . . . . . . . . . . . . . . . . . 21 (𝑤𝑋 ↦ (𝑤𝑛)) = (𝑤𝑋 ↦ (𝑤𝑛))
4342dmmptss 5774 . . . . . . . . . . . . . . . . . . . 20 dom (𝑤𝑋 ↦ (𝑤𝑛)) ⊆ 𝑋
4441, 43sstri 3761 . . . . . . . . . . . . . . . . . . 19 ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ 𝑋
4544, 14sseqtri 3786 . . . . . . . . . . . . . . . . . 18 ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ X𝑦𝐴 (𝐹𝑦)
4645rgenw 3073 . . . . . . . . . . . . . . . . 17 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ X𝑦𝐴 (𝐹𝑦)
47 r19.2z 4202 . . . . . . . . . . . . . . . . 17 (((𝐴𝑚) ≠ ∅ ∧ ∀𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ X𝑦𝐴 (𝐹𝑦)) → ∃𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ X𝑦𝐴 (𝐹𝑦))
4840, 46, 47sylancl 574 . . . . . . . . . . . . . . . 16 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → ∃𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ X𝑦𝐴 (𝐹𝑦))
49 iinss 4706 . . . . . . . . . . . . . . . 16 (∃𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ X𝑦𝐴 (𝐹𝑦) → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ X𝑦𝐴 (𝐹𝑦))
5048, 49syl 17 . . . . . . . . . . . . . . 15 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ X𝑦𝐴 (𝐹𝑦))
5150, 14syl6sseqr 3801 . . . . . . . . . . . . . 14 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ 𝑋)
52 sseqin2 3968 . . . . . . . . . . . . . 14 ( 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ 𝑋 ↔ (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) = 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
5351, 52sylib 208 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) = 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
5433ad2antrr 705 . . . . . . . . . . . . . . . . 17 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))
55 ssralv 3815 . . . . . . . . . . . . . . . . . 18 ((𝐴𝑚) ⊆ 𝐴 → (∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦) → ∀𝑦 ∈ (𝐴𝑚)(𝑦) ∈ (𝐹𝑦)))
5627, 55ax-mp 5 . . . . . . . . . . . . . . . . 17 (∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦) → ∀𝑦 ∈ (𝐴𝑚)(𝑦) ∈ (𝐹𝑦))
57 elssuni 4604 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑦) ∈ (𝐹𝑦) → (𝑦) ⊆ (𝐹𝑦))
58 iffalse 4235 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑦 = 𝑛 → if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) = (𝐹𝑦))
5958sseq2d 3782 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑦 = 𝑛 → ((𝑦) ⊆ if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ↔ (𝑦) ⊆ (𝐹𝑦)))
6057, 59syl5ibrcom 237 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦) ∈ (𝐹𝑦) → (¬ 𝑦 = 𝑛 → (𝑦) ⊆ if(𝑦 = 𝑛, (𝑛), (𝐹𝑦))))
61 ssid 3773 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦) ⊆ (𝑦)
62 iftrue 4232 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑛 → if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) = (𝑛))
6362, 30eqtr4d 2808 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = 𝑛 → if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) = (𝑦))
6461, 63syl5sseqr 3803 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = 𝑛 → (𝑦) ⊆ if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
6560, 64pm2.61d2 173 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦) ∈ (𝐹𝑦) → (𝑦) ⊆ if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
6665ralrimivw 3116 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦) ∈ (𝐹𝑦) → ∀𝑛 ∈ (𝐴𝑚)(𝑦) ⊆ if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
67 ssiin 4705 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦) ⊆ 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ↔ ∀𝑛 ∈ (𝐴𝑚)(𝑦) ⊆ if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
6866, 67sylibr 224 . . . . . . . . . . . . . . . . . . . 20 ((𝑦) ∈ (𝐹𝑦) → (𝑦) ⊆ 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
6968adantl 467 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ (𝐴𝑚) ∧ (𝑦) ∈ (𝐹𝑦)) → (𝑦) ⊆ 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
7062equcoms 2105 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = 𝑦 → if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) = (𝑛))
71 fveq2 6333 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = 𝑦 → (𝑛) = (𝑦))
7270, 71eqtrd 2805 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝑦 → if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) = (𝑦))
7372sseq1d 3781 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑦 → (if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ⊆ (𝑦) ↔ (𝑦) ⊆ (𝑦)))
7473rspcev 3460 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 ∈ (𝐴𝑚) ∧ (𝑦) ⊆ (𝑦)) → ∃𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ⊆ (𝑦))
7561, 74mpan2 671 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ (𝐴𝑚) → ∃𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ⊆ (𝑦))
76 iinss 4706 . . . . . . . . . . . . . . . . . . . . 21 (∃𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ⊆ (𝑦) → 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ⊆ (𝑦))
7775, 76syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (𝐴𝑚) → 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ⊆ (𝑦))
7877adantr 466 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ (𝐴𝑚) ∧ (𝑦) ∈ (𝐹𝑦)) → 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ⊆ (𝑦))
7969, 78eqssd 3769 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ (𝐴𝑚) ∧ (𝑦) ∈ (𝐹𝑦)) → (𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
8079ralimiaa 3100 . . . . . . . . . . . . . . . . 17 (∀𝑦 ∈ (𝐴𝑚)(𝑦) ∈ (𝐹𝑦) → ∀𝑦 ∈ (𝐴𝑚)(𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
8154, 56, 803syl 18 . . . . . . . . . . . . . . . 16 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → ∀𝑦 ∈ (𝐴𝑚)(𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
82 eldifn 3884 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ (𝐴𝑚) → ¬ 𝑦𝑚)
8382ad2antlr 706 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐴𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴𝑚)) ∧ 𝑛 ∈ (𝐴𝑚)) → ¬ 𝑦𝑚)
84 inss2 3982 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴𝑚) ⊆ 𝑚
85 simpr 471 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐴𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴𝑚)) ∧ 𝑛 ∈ (𝐴𝑚)) → 𝑛 ∈ (𝐴𝑚))
8684, 85sseldi 3750 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐴𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴𝑚)) ∧ 𝑛 ∈ (𝐴𝑚)) → 𝑛𝑚)
87 eleq1 2838 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = 𝑛 → (𝑦𝑚𝑛𝑚))
8886, 87syl5ibrcom 237 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐴𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴𝑚)) ∧ 𝑛 ∈ (𝐴𝑚)) → (𝑦 = 𝑛𝑦𝑚))
8983, 88mtod 189 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴𝑚)) ∧ 𝑛 ∈ (𝐴𝑚)) → ¬ 𝑦 = 𝑛)
9089, 58syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴𝑚)) ∧ 𝑛 ∈ (𝐴𝑚)) → if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) = (𝐹𝑦))
9190iineq2dv 4678 . . . . . . . . . . . . . . . . . . . 20 (((𝐴𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴𝑚)) → 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) = 𝑛 ∈ (𝐴𝑚) (𝐹𝑦))
92 iinconst 4665 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴𝑚) ≠ ∅ → 𝑛 ∈ (𝐴𝑚) (𝐹𝑦) = (𝐹𝑦))
9392adantr 466 . . . . . . . . . . . . . . . . . . . 20 (((𝐴𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴𝑚)) → 𝑛 ∈ (𝐴𝑚) (𝐹𝑦) = (𝐹𝑦))
9491, 93eqtr2d 2806 . . . . . . . . . . . . . . . . . . 19 (((𝐴𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴𝑚)) → (𝐹𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
95 eqeq1 2775 . . . . . . . . . . . . . . . . . . 19 ((𝑦) = (𝐹𝑦) → ((𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ↔ (𝐹𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦))))
9694, 95syl5ibrcom 237 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴𝑚)) → ((𝑦) = (𝐹𝑦) → (𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦))))
9796ralimdva 3111 . . . . . . . . . . . . . . . . 17 ((𝐴𝑚) ≠ ∅ → (∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦) → ∀𝑦 ∈ (𝐴𝑚)(𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦))))
984, 97mpan9 496 . . . . . . . . . . . . . . . 16 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → ∀𝑦 ∈ (𝐴𝑚)(𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
99 inundif 4189 . . . . . . . . . . . . . . . . . 18 ((𝐴𝑚) ∪ (𝐴𝑚)) = 𝐴
10099raleqi 3291 . . . . . . . . . . . . . . . . 17 (∀𝑦 ∈ ((𝐴𝑚) ∪ (𝐴𝑚))(𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ↔ ∀𝑦𝐴 (𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
101 ralunb 3945 . . . . . . . . . . . . . . . . 17 (∀𝑦 ∈ ((𝐴𝑚) ∪ (𝐴𝑚))(𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ↔ (∀𝑦 ∈ (𝐴𝑚)(𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦))))
102100, 101bitr3i 266 . . . . . . . . . . . . . . . 16 (∀𝑦𝐴 (𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ↔ (∀𝑦 ∈ (𝐴𝑚)(𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦))))
10381, 98, 102sylanbrc 572 . . . . . . . . . . . . . . 15 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → ∀𝑦𝐴 (𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
104 ixpeq2 8079 . . . . . . . . . . . . . . 15 (∀𝑦𝐴 (𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) → X𝑦𝐴 (𝑦) = X𝑦𝐴 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
105103, 104syl 17 . . . . . . . . . . . . . 14 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → X𝑦𝐴 (𝑦) = X𝑦𝐴 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
106 ixpiin 8091 . . . . . . . . . . . . . . 15 ((𝐴𝑚) ≠ ∅ → X𝑦𝐴 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) = 𝑛 ∈ (𝐴𝑚)X𝑦𝐴 if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
107106adantl 467 . . . . . . . . . . . . . 14 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → X𝑦𝐴 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) = 𝑛 ∈ (𝐴𝑚)X𝑦𝐴 if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
108105, 107eqtrd 2805 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → X𝑦𝐴 (𝑦) = 𝑛 ∈ (𝐴𝑚)X𝑦𝐴 if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
10939, 53, 1083eqtr4rd 2816 . . . . . . . . . . . 12 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → X𝑦𝐴 (𝑦) = (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))))
11025, 109pm2.61dane 3030 . . . . . . . . . . 11 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → X𝑦𝐴 (𝑦) = (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))))
111 ixpexg 8089 . . . . . . . . . . . . . . . . . . . . . . . 24 (∀𝑛𝐴 (𝐹𝑛) ∈ V → X𝑛𝐴 (𝐹𝑛) ∈ V)
112 fvex 6344 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐹𝑛) ∈ V
113112uniex 7103 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐹𝑛) ∈ V
114113a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛𝐴 (𝐹𝑛) ∈ V)
115111, 114mprg 3075 . . . . . . . . . . . . . . . . . . . . . . 23 X𝑛𝐴 (𝐹𝑛) ∈ V
11610, 115eqeltri 2846 . . . . . . . . . . . . . . . . . . . . . 22 𝑋 ∈ V
117116mptex 6632 . . . . . . . . . . . . . . . . . . . . 21 (𝑤𝑋 ↦ (𝑤𝑛)) ∈ V
118117cnvex 7263 . . . . . . . . . . . . . . . . . . . 20 (𝑤𝑋 ↦ (𝑤𝑛)) ∈ V
119118imaex 7254 . . . . . . . . . . . . . . . . . . 19 ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ∈ V
120119dfiin2 4690 . . . . . . . . . . . . . . . . . 18 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) = {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))}
121 inteq 4615 . . . . . . . . . . . . . . . . . 18 ({𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} = ∅ → {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} = ∅)
122120, 121syl5eq 2817 . . . . . . . . . . . . . . . . 17 ({𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} = ∅ → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) = ∅)
123 int0 4626 . . . . . . . . . . . . . . . . 17 ∅ = V
124122, 123syl6eq 2821 . . . . . . . . . . . . . . . 16 ({𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} = ∅ → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) = V)
125124ineq2d 3965 . . . . . . . . . . . . . . 15 ({𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} = ∅ → (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) = (𝑋 ∩ V))
126 inv1 4115 . . . . . . . . . . . . . . 15 (𝑋 ∩ V) = 𝑋
127125, 126syl6eq 2821 . . . . . . . . . . . . . 14 ({𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} = ∅ → (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) = 𝑋)
128127adantl 467 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} = ∅) → (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) = 𝑋)
129 snex 5037 . . . . . . . . . . . . . . . . . 18 {𝑋} ∈ V
1301ptbas 21602 . . . . . . . . . . . . . . . . . . 19 ((𝐴𝑉𝐹:𝐴⟶Top) → 𝐵 ∈ TopBases)
1311, 10ptpjpre2 21603 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝑘𝐴𝑢 ∈ (𝐹𝑘))) → ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) ∈ 𝐵)
132131ralrimivva 3120 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴𝑉𝐹:𝐴⟶Top) → ∀𝑘𝐴𝑢 ∈ (𝐹𝑘)((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) ∈ 𝐵)
133 eqid 2771 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)) = (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))
134133fmpt2x 7389 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑘𝐴𝑢 ∈ (𝐹𝑘)((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) ∈ 𝐵 ↔ (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)): 𝑘𝐴 ({𝑘} × (𝐹𝑘))⟶𝐵)
135132, 134sylib 208 . . . . . . . . . . . . . . . . . . . 20 ((𝐴𝑉𝐹:𝐴⟶Top) → (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)): 𝑘𝐴 ({𝑘} × (𝐹𝑘))⟶𝐵)
136135frnd 6191 . . . . . . . . . . . . . . . . . . 19 ((𝐴𝑉𝐹:𝐴⟶Top) → ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)) ⊆ 𝐵)
137130, 136ssexd 4940 . . . . . . . . . . . . . . . . . 18 ((𝐴𝑉𝐹:𝐴⟶Top) → ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)) ∈ V)
138 unexg 7109 . . . . . . . . . . . . . . . . . 18 (({𝑋} ∈ V ∧ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)) ∈ V) → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ∈ V)
139129, 137, 138sylancr 575 . . . . . . . . . . . . . . . . 17 ((𝐴𝑉𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ∈ V)
140 ssfii 8484 . . . . . . . . . . . . . . . . 17 (({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ∈ V → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ⊆ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
141139, 140syl 17 . . . . . . . . . . . . . . . 16 ((𝐴𝑉𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ⊆ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
142141ad2antrr 705 . . . . . . . . . . . . . . 15 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ⊆ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
143 ssun1 3927 . . . . . . . . . . . . . . . . 17 {𝑋} ⊆ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))
144116snss 4452 . . . . . . . . . . . . . . . . 17 (𝑋 ∈ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ↔ {𝑋} ⊆ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))
145143, 144mpbir 221 . . . . . . . . . . . . . . . 16 𝑋 ∈ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))
146145a1i 11 . . . . . . . . . . . . . . 15 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → 𝑋 ∈ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))
147142, 146sseldd 3753 . . . . . . . . . . . . . 14 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → 𝑋 ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
148147adantr 466 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} = ∅) → 𝑋 ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
149128, 148eqeltrd 2850 . . . . . . . . . . . 12 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} = ∅) → (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
150139ad3antrrr 709 . . . . . . . . . . . . . . . . . 18 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ∈ V)
151 nfv 1995 . . . . . . . . . . . . . . . . . . . . . 22 𝑛(((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦)))
152 nfcv 2913 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑛𝐴
153 nfcv 2913 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑛(𝐹𝑘)
154 nfixp1 8085 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑛X𝑛𝐴 (𝐹𝑛)
15510, 154nfcxfr 2911 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑛𝑋
156 nfcv 2913 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑛(𝑤𝑘)
157155, 156nfmpt 4881 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑛(𝑤𝑋 ↦ (𝑤𝑘))
158157nfcnv 5438 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑛(𝑤𝑋 ↦ (𝑤𝑘))
159 nfcv 2913 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑛𝑢
160158, 159nfima 5614 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑛((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)
161152, 153, 160nfmpt2 6874 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑛(𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))
162161nfrn 5505 . . . . . . . . . . . . . . . . . . . . . . 23 𝑛ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))
163162nfcri 2907 . . . . . . . . . . . . . . . . . . . . . 22 𝑛 𝑧 ∈ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))
164 df-ov 6798 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛(𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))(𝑛)) = ((𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))‘⟨𝑛, (𝑛)⟩)
165119a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ∈ V)
166 fveq2 6333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑘 = 𝑛 → (𝑤𝑘) = (𝑤𝑛))
167166mpteq2dv 4880 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 = 𝑛 → (𝑤𝑋 ↦ (𝑤𝑘)) = (𝑤𝑋 ↦ (𝑤𝑛)))
168167cnveqd 5435 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑘 = 𝑛(𝑤𝑋 ↦ (𝑤𝑘)) = (𝑤𝑋 ↦ (𝑤𝑛)))
169168imaeq1d 5605 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘 = 𝑛 → ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) = ((𝑤𝑋 ↦ (𝑤𝑛)) “ 𝑢))
170 imaeq2 5602 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑢 = (𝑛) → ((𝑤𝑋 ↦ (𝑤𝑛)) “ 𝑢) = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
171169, 170sylan9eq 2825 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑘 = 𝑛𝑢 = (𝑛)) → ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
172 fveq2 6333 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑘 = 𝑛 → (𝐹𝑘) = (𝐹𝑛))
173171, 172, 133ovmpt2x 6939 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑛𝐴 ∧ (𝑛) ∈ (𝐹𝑛) ∧ ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ∈ V) → (𝑛(𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))(𝑛)) = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
17429, 35, 165, 173syl3anc 1476 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → (𝑛(𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))(𝑛)) = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
175164, 174syl5eqr 2819 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → ((𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))‘⟨𝑛, (𝑛)⟩) = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
176135ad3antrrr 709 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)): 𝑘𝐴 ({𝑘} × (𝐹𝑘))⟶𝐵)
177176ffnd 6185 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)) Fn 𝑘𝐴 ({𝑘} × (𝐹𝑘)))
178 opeliunxp 5309 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (⟨𝑛, (𝑛)⟩ ∈ 𝑛𝐴 ({𝑛} × (𝐹𝑛)) ↔ (𝑛𝐴 ∧ (𝑛) ∈ (𝐹𝑛)))
17929, 35, 178sylanbrc 572 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → ⟨𝑛, (𝑛)⟩ ∈ 𝑛𝐴 ({𝑛} × (𝐹𝑛)))
180 sneq 4327 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 = 𝑘 → {𝑛} = {𝑘})
181 fveq2 6333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 = 𝑘 → (𝐹𝑛) = (𝐹𝑘))
182180, 181xpeq12d 5280 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 = 𝑘 → ({𝑛} × (𝐹𝑛)) = ({𝑘} × (𝐹𝑘)))
183182cbviunv 4694 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑛𝐴 ({𝑛} × (𝐹𝑛)) = 𝑘𝐴 ({𝑘} × (𝐹𝑘))
184179, 183syl6eleq 2860 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → ⟨𝑛, (𝑛)⟩ ∈ 𝑘𝐴 ({𝑘} × (𝐹𝑘)))
185 fnfvelrn 6501 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)) Fn 𝑘𝐴 ({𝑘} × (𝐹𝑘)) ∧ ⟨𝑛, (𝑛)⟩ ∈ 𝑘𝐴 ({𝑘} × (𝐹𝑘))) → ((𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))‘⟨𝑛, (𝑛)⟩) ∈ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))
186177, 184, 185syl2anc 573 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → ((𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))‘⟨𝑛, (𝑛)⟩) ∈ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))
187175, 186eqeltrrd 2851 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ∈ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))
188 eleq1 2838 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) → (𝑧 ∈ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)) ↔ ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ∈ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))
189187, 188syl5ibrcom 237 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → (𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) → 𝑧 ∈ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))
190189ex 397 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → (𝑛 ∈ (𝐴𝑚) → (𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) → 𝑧 ∈ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
191151, 163, 190rexlimd 3174 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → (∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) → 𝑧 ∈ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))
192191abssdv 3825 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ⊆ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))
193 ssun2 3928 . . . . . . . . . . . . . . . . . . . 20 ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)) ⊆ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))
194192, 193syl6ss 3764 . . . . . . . . . . . . . . . . . . 19 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ⊆ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))
195194adantr 466 . . . . . . . . . . . . . . . . . 18 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ⊆ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))
196 simpr 471 . . . . . . . . . . . . . . . . . 18 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅)
197 simplrl 762 . . . . . . . . . . . . . . . . . . . 20 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → 𝑚 ∈ Fin)
198 ssfi 8339 . . . . . . . . . . . . . . . . . . . 20 ((𝑚 ∈ Fin ∧ (𝐴𝑚) ⊆ 𝑚) → (𝐴𝑚) ∈ Fin)
199197, 84, 198sylancl 574 . . . . . . . . . . . . . . . . . . 19 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → (𝐴𝑚) ∈ Fin)
200 abrexfi 8425 . . . . . . . . . . . . . . . . . . 19 ((𝐴𝑚) ∈ Fin → {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ∈ Fin)
201199, 200syl 17 . . . . . . . . . . . . . . . . . 18 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ∈ Fin)
202 elfir 8480 . . . . . . . . . . . . . . . . . 18 ((({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ∈ V ∧ ({𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ⊆ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅ ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ∈ Fin)) → {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
203150, 195, 196, 201, 202syl13anc 1478 . . . . . . . . . . . . . . . . 17 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
204120, 203syl5eqel 2854 . . . . . . . . . . . . . . . 16 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
205 elssuni 4604 . . . . . . . . . . . . . . . 16 ( 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))) → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
206204, 205syl 17 . . . . . . . . . . . . . . 15 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
207 fiuni 8493 . . . . . . . . . . . . . . . . . 18 (({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ∈ V → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) = (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
208139, 207syl 17 . . . . . . . . . . . . . . . . 17 ((𝐴𝑉𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) = (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
209116pwid 4314 . . . . . . . . . . . . . . . . . . . . . 22 𝑋 ∈ 𝒫 𝑋
210209a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴𝑉𝐹:𝐴⟶Top) → 𝑋 ∈ 𝒫 𝑋)
211210snssd 4476 . . . . . . . . . . . . . . . . . . . 20 ((𝐴𝑉𝐹:𝐴⟶Top) → {𝑋} ⊆ 𝒫 𝑋)
2121ptuni2 21599 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴𝑉𝐹:𝐴⟶Top) → X𝑛𝐴 (𝐹𝑛) = 𝐵)
21310, 212syl5eq 2817 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴𝑉𝐹:𝐴⟶Top) → 𝑋 = 𝐵)
214 eqimss2 3807 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑋 = 𝐵 𝐵𝑋)
215213, 214syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴𝑉𝐹:𝐴⟶Top) → 𝐵𝑋)
216 sspwuni 4746 . . . . . . . . . . . . . . . . . . . . . 22 (𝐵 ⊆ 𝒫 𝑋 𝐵𝑋)
217215, 216sylibr 224 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴𝑉𝐹:𝐴⟶Top) → 𝐵 ⊆ 𝒫 𝑋)
218136, 217sstrd 3762 . . . . . . . . . . . . . . . . . . . 20 ((𝐴𝑉𝐹:𝐴⟶Top) → ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)) ⊆ 𝒫 𝑋)
219211, 218unssd 3940 . . . . . . . . . . . . . . . . . . 19 ((𝐴𝑉𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ⊆ 𝒫 𝑋)
220 sspwuni 4746 . . . . . . . . . . . . . . . . . . 19 (({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ⊆ 𝒫 𝑋 ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ⊆ 𝑋)
221219, 220sylib 208 . . . . . . . . . . . . . . . . . 18 ((𝐴𝑉𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ⊆ 𝑋)
222 elssuni 4604 . . . . . . . . . . . . . . . . . . 19 (𝑋 ∈ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) → 𝑋 ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))
223145, 222mp1i 13 . . . . . . . . . . . . . . . . . 18 ((𝐴𝑉𝐹:𝐴⟶Top) → 𝑋 ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))
224221, 223eqssd 3769 . . . . . . . . . . . . . . . . 17 ((𝐴𝑉𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) = 𝑋)
225208, 224eqtr3d 2807 . . . . . . . . . . . . . . . 16 ((𝐴𝑉𝐹:𝐴⟶Top) → (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))) = 𝑋)
226225ad3antrrr 709 . . . . . . . . . . . . . . 15 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))) = 𝑋)
227206, 226sseqtrd 3790 . . . . . . . . . . . . . 14 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ 𝑋)
228227, 52sylib 208 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) = 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
229228, 204eqeltrd 2850 . . . . . . . . . . . 12 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
230149, 229pm2.61dane 3030 . . . . . . . . . . 11 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
231110, 230eqeltrd 2850 . . . . . . . . . 10 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → X𝑦𝐴 (𝑦) ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
232231rexlimdvaa 3180 . . . . . . . . 9 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) → (∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦) → X𝑦𝐴 (𝑦) ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))))
233232impr 442 . . . . . . . 8 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦)) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → X𝑦𝐴 (𝑦) ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
2343, 233sylan2b 581 . . . . . . 7 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → X𝑦𝐴 (𝑦) ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
235 eleq1 2838 . . . . . . 7 (𝑠 = X𝑦𝐴 (𝑦) → (𝑠 ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))) ↔ X𝑦𝐴 (𝑦) ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))))
236234, 235syl5ibrcom 237 . . . . . 6 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → (𝑠 = X𝑦𝐴 (𝑦) → 𝑠 ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))))
237236expimpd 441 . . . . 5 ((𝐴𝑉𝐹:𝐴⟶Top) → ((( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑦)) → 𝑠 ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))))
238237exlimdv 2013 . . . 4 ((𝐴𝑉𝐹:𝐴⟶Top) → (∃(( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑦)) → 𝑠 ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))))
2392, 238syl5bi 232 . . 3 ((𝐴𝑉𝐹:𝐴⟶Top) → (𝑠𝐵𝑠 ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))))
240239ssrdv 3758 . 2 ((𝐴𝑉𝐹:𝐴⟶Top) → 𝐵 ⊆ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
2411ptbasid 21598 . . . . . . 7 ((𝐴𝑉𝐹:𝐴⟶Top) → X𝑛𝐴 (𝐹𝑛) ∈ 𝐵)
24210, 241syl5eqel 2854 . . . . . 6 ((𝐴𝑉𝐹:𝐴⟶Top) → 𝑋𝐵)
243242snssd 4476 . . . . 5 ((𝐴𝑉𝐹:𝐴⟶Top) → {𝑋} ⊆ 𝐵)
244243, 136unssd 3940 . . . 4 ((𝐴𝑉𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ⊆ 𝐵)
245 fiss 8489 . . . 4 ((𝐵 ∈ TopBases ∧ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ⊆ 𝐵) → (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))) ⊆ (fi‘𝐵))
246130, 244, 245syl2anc 573 . . 3 ((𝐴𝑉𝐹:𝐴⟶Top) → (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))) ⊆ (fi‘𝐵))
2471ptbasin2 21601 . . 3 ((𝐴𝑉𝐹:𝐴⟶Top) → (fi‘𝐵) = 𝐵)
248246, 247sseqtrd 3790 . 2 ((𝐴𝑉𝐹:𝐴⟶Top) → (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))) ⊆ 𝐵)
249240, 248eqssd 3769 1 ((𝐴𝑉𝐹:𝐴⟶Top) → 𝐵 = (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 382  w3a 1071   = wceq 1631  wex 1852  wcel 2145  {cab 2757  wne 2943  wral 3061  wrex 3062  Vcvv 3351  cdif 3720  cun 3721  cin 3722  wss 3723  c0 4063  ifcif 4226  𝒫 cpw 4298  {csn 4317  cop 4323   cuni 4575   cint 4612   ciun 4655   ciin 4656  cmpt 4864   × cxp 5248  ccnv 5249  dom cdm 5250  ran crn 5251  cima 5253   Fn wfn 6025  wf 6026  cfv 6030  (class class class)co 6795  cmpt2 6797  Xcixp 8065  Fincfn 8112  ficfi 8475  Topctop 20917  TopBasesctb 20969
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4905  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035  ax-un 7099
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4576  df-int 4613  df-iun 4657  df-iin 4658  df-br 4788  df-opab 4848  df-mpt 4865  df-tr 4888  df-id 5158  df-eprel 5163  df-po 5171  df-so 5172  df-fr 5209  df-we 5211  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263  df-pred 5822  df-ord 5868  df-on 5869  df-lim 5870  df-suc 5871  df-iota 5993  df-fun 6032  df-fn 6033  df-f 6034  df-f1 6035  df-fo 6036  df-f1o 6037  df-fv 6038  df-ov 6798  df-oprab 6799  df-mpt2 6800  df-om 7216  df-1st 7318  df-2nd 7319  df-wrecs 7562  df-recs 7624  df-rdg 7662  df-1o 7716  df-oadd 7720  df-er 7899  df-ixp 8066  df-en 8113  df-dom 8114  df-fin 8116  df-fi 8476  df-top 20918  df-bases 20970
This theorem is referenced by:  ptval2  21624  xkoptsub  21677  ptcmplem1  22075  prdsxmslem2  22553
  Copyright terms: Public domain W3C validator