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

Theorem ptbasfi 21194
 Description: The basis for the product topology can also be written as the set of finite intersections of "cylinder sets", the preimages of projections into one factor from open sets in the factor. (We have to add 𝑋 itself to the list because if 𝐴 is empty we get (fi‘∅) = ∅ while 𝐵 = {∅}.) (Contributed by Mario Carneiro, 3-Feb-2015.)
Hypotheses
Ref Expression
ptbas.1 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑥 = X𝑦𝐴 (𝑔𝑦))}
ptbasfi.2 𝑋 = X𝑛𝐴 (𝐹𝑛)
Assertion
Ref Expression
ptbasfi ((𝐴𝑉𝐹:𝐴⟶Top) → 𝐵 = (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
Distinct variable groups:   𝑘,𝑛,𝑢,𝐵   𝑤,𝑔,𝑥,𝑦,𝑛,𝑘,𝑢,𝑧,𝐴   𝑔,𝐹,𝑘,𝑛,𝑢,𝑤,𝑥,𝑦,𝑧   𝑔,𝑋,𝑘,𝑢,𝑤,𝑥,𝑧   𝑔,𝑉,𝑘,𝑛,𝑢,𝑤,𝑥,𝑦,𝑧
Allowed substitution hints:   𝐵(𝑥,𝑦,𝑧,𝑤,𝑔)   𝑋(𝑦,𝑛)

Proof of Theorem ptbasfi
Dummy variables 𝑠 𝑚 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ptbas.1 . . . . 5 𝐵 = {𝑥 ∣ ∃𝑔((𝑔 Fn 𝐴 ∧ ∀𝑦𝐴 (𝑔𝑦) ∈ (𝐹𝑦) ∧ ∃𝑧 ∈ Fin ∀𝑦 ∈ (𝐴𝑧)(𝑔𝑦) = (𝐹𝑦)) ∧ 𝑥 = X𝑦𝐴 (𝑔𝑦))}
21elpt 21185 . . . 4 (𝑠𝐵 ↔ ∃(( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑦)))
3 df-3an 1033 . . . . . . . 8 (( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦)) ↔ (( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦)) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦)))
4 simprr 792 . . . . . . . . . . . . . 14 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))
5 disjdif2 3999 . . . . . . . . . . . . . . . . . 18 ((𝐴𝑚) = ∅ → (𝐴𝑚) = 𝐴)
65raleqdv 3121 . . . . . . . . . . . . . . . . 17 ((𝐴𝑚) = ∅ → (∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦) ↔ ∀𝑦𝐴 (𝑦) = (𝐹𝑦)))
76biimpac 502 . . . . . . . . . . . . . . . 16 ((∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦) ∧ (𝐴𝑚) = ∅) → ∀𝑦𝐴 (𝑦) = (𝐹𝑦))
8 ixpeq2 7808 . . . . . . . . . . . . . . . 16 (∀𝑦𝐴 (𝑦) = (𝐹𝑦) → X𝑦𝐴 (𝑦) = X𝑦𝐴 (𝐹𝑦))
97, 8syl 17 . . . . . . . . . . . . . . 15 ((∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦) ∧ (𝐴𝑚) = ∅) → X𝑦𝐴 (𝑦) = X𝑦𝐴 (𝐹𝑦))
10 ptbasfi.2 . . . . . . . . . . . . . . . 16 𝑋 = X𝑛𝐴 (𝐹𝑛)
11 fveq2 6103 . . . . . . . . . . . . . . . . . 18 (𝑛 = 𝑦 → (𝐹𝑛) = (𝐹𝑦))
1211unieqd 4382 . . . . . . . . . . . . . . . . 17 (𝑛 = 𝑦 (𝐹𝑛) = (𝐹𝑦))
1312cbvixpv 7812 . . . . . . . . . . . . . . . 16 X𝑛𝐴 (𝐹𝑛) = X𝑦𝐴 (𝐹𝑦)
1410, 13eqtri 2632 . . . . . . . . . . . . . . 15 𝑋 = X𝑦𝐴 (𝐹𝑦)
159, 14syl6eqr 2662 . . . . . . . . . . . . . 14 ((∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦) ∧ (𝐴𝑚) = ∅) → X𝑦𝐴 (𝑦) = 𝑋)
164, 15sylan 487 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) = ∅) → X𝑦𝐴 (𝑦) = 𝑋)
17 ssv 3588 . . . . . . . . . . . . . . . 16 𝑋 ⊆ V
18 iineq1 4471 . . . . . . . . . . . . . . . . 17 ((𝐴𝑚) = ∅ → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) = 𝑛 ∈ ∅ ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
19 0iin 4514 . . . . . . . . . . . . . . . . 17 𝑛 ∈ ∅ ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) = V
2018, 19syl6eq 2660 . . . . . . . . . . . . . . . 16 ((𝐴𝑚) = ∅ → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) = V)
2117, 20syl5sseqr 3617 . . . . . . . . . . . . . . 15 ((𝐴𝑚) = ∅ → 𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
2221adantl 481 . . . . . . . . . . . . . 14 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) = ∅) → 𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
23 df-ss 3554 . . . . . . . . . . . . . 14 (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ↔ (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) = 𝑋)
2422, 23sylib 207 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) = ∅) → (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) = 𝑋)
2516, 24eqtr4d 2647 . . . . . . . . . . . 12 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) = ∅) → X𝑦𝐴 (𝑦) = (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))))
26 simplll 794 . . . . . . . . . . . . . . . 16 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → (𝐴𝑉𝐹:𝐴⟶Top))
27 inss1 3795 . . . . . . . . . . . . . . . . 17 (𝐴𝑚) ⊆ 𝐴
28 simpr 476 . . . . . . . . . . . . . . . . 17 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → 𝑛 ∈ (𝐴𝑚))
2927, 28sseldi 3566 . . . . . . . . . . . . . . . 16 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → 𝑛𝐴)
30 simprr 792 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) → ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))
3130ad2antrr 758 . . . . . . . . . . . . . . . . 17 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))
32 fveq2 6103 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑛 → (𝑦) = (𝑛))
33 fveq2 6103 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑛 → (𝐹𝑦) = (𝐹𝑛))
3432, 33eleq12d 2682 . . . . . . . . . . . . . . . . . 18 (𝑦 = 𝑛 → ((𝑦) ∈ (𝐹𝑦) ↔ (𝑛) ∈ (𝐹𝑛)))
3534rspcv 3278 . . . . . . . . . . . . . . . . 17 (𝑛𝐴 → (∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦) → (𝑛) ∈ (𝐹𝑛)))
3629, 31, 35sylc 63 . . . . . . . . . . . . . . . 16 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → (𝑛) ∈ (𝐹𝑛))
3714ptpjpre1 21184 . . . . . . . . . . . . . . . 16 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝑛𝐴 ∧ (𝑛) ∈ (𝐹𝑛))) → ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) = X𝑦𝐴 if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
3826, 29, 36, 37syl12anc 1316 . . . . . . . . . . . . . . 15 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) = X𝑦𝐴 if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
3938adantlr 747 . . . . . . . . . . . . . 14 ((((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) ∧ 𝑛 ∈ (𝐴𝑚)) → ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) = X𝑦𝐴 if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
4039iineq2dv 4479 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) = 𝑛 ∈ (𝐴𝑚)X𝑦𝐴 if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
41 simpr 476 . . . . . . . . . . . . . . . . 17 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → (𝐴𝑚) ≠ ∅)
42 cnvimass 5404 . . . . . . . . . . . . . . . . . . . 20 ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ dom (𝑤𝑋 ↦ (𝑤𝑛))
43 eqid 2610 . . . . . . . . . . . . . . . . . . . . 21 (𝑤𝑋 ↦ (𝑤𝑛)) = (𝑤𝑋 ↦ (𝑤𝑛))
4443dmmptss 5548 . . . . . . . . . . . . . . . . . . . 20 dom (𝑤𝑋 ↦ (𝑤𝑛)) ⊆ 𝑋
4542, 44sstri 3577 . . . . . . . . . . . . . . . . . . 19 ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ 𝑋
4645, 14sseqtri 3600 . . . . . . . . . . . . . . . . . 18 ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ X𝑦𝐴 (𝐹𝑦)
4746rgenw 2908 . . . . . . . . . . . . . . . . 17 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ X𝑦𝐴 (𝐹𝑦)
48 r19.2z 4012 . . . . . . . . . . . . . . . . 17 (((𝐴𝑚) ≠ ∅ ∧ ∀𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ X𝑦𝐴 (𝐹𝑦)) → ∃𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ X𝑦𝐴 (𝐹𝑦))
4941, 47, 48sylancl 693 . . . . . . . . . . . . . . . 16 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → ∃𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ X𝑦𝐴 (𝐹𝑦))
50 iinss 4507 . . . . . . . . . . . . . . . 16 (∃𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ X𝑦𝐴 (𝐹𝑦) → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ X𝑦𝐴 (𝐹𝑦))
5149, 50syl 17 . . . . . . . . . . . . . . 15 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ X𝑦𝐴 (𝐹𝑦))
5251, 14syl6sseqr 3615 . . . . . . . . . . . . . 14 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ 𝑋)
53 sseqin2 3779 . . . . . . . . . . . . . 14 ( 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ 𝑋 ↔ (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) = 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
5452, 53sylib 207 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) = 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
5530ad2antrr 758 . . . . . . . . . . . . . . . . 17 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))
56 ssralv 3629 . . . . . . . . . . . . . . . . . 18 ((𝐴𝑚) ⊆ 𝐴 → (∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦) → ∀𝑦 ∈ (𝐴𝑚)(𝑦) ∈ (𝐹𝑦)))
5727, 56ax-mp 5 . . . . . . . . . . . . . . . . 17 (∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦) → ∀𝑦 ∈ (𝐴𝑚)(𝑦) ∈ (𝐹𝑦))
58 elssuni 4403 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑦) ∈ (𝐹𝑦) → (𝑦) ⊆ (𝐹𝑦))
59 iffalse 4045 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑦 = 𝑛 → if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) = (𝐹𝑦))
6059sseq2d 3596 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑦 = 𝑛 → ((𝑦) ⊆ if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ↔ (𝑦) ⊆ (𝐹𝑦)))
6158, 60syl5ibrcom 236 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦) ∈ (𝐹𝑦) → (¬ 𝑦 = 𝑛 → (𝑦) ⊆ if(𝑦 = 𝑛, (𝑛), (𝐹𝑦))))
62 ssid 3587 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦) ⊆ (𝑦)
63 iftrue 4042 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑦 = 𝑛 → if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) = (𝑛))
6463, 32eqtr4d 2647 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = 𝑛 → if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) = (𝑦))
6562, 64syl5sseqr 3617 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦 = 𝑛 → (𝑦) ⊆ if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
6661, 65pm2.61d2 171 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦) ∈ (𝐹𝑦) → (𝑦) ⊆ if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
6766ralrimivw 2950 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦) ∈ (𝐹𝑦) → ∀𝑛 ∈ (𝐴𝑚)(𝑦) ⊆ if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
68 ssiin 4506 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦) ⊆ 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ↔ ∀𝑛 ∈ (𝐴𝑚)(𝑦) ⊆ if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
6967, 68sylibr 223 . . . . . . . . . . . . . . . . . . . 20 ((𝑦) ∈ (𝐹𝑦) → (𝑦) ⊆ 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
7069adantl 481 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ (𝐴𝑚) ∧ (𝑦) ∈ (𝐹𝑦)) → (𝑦) ⊆ 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
7163equcoms 1934 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = 𝑦 → if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) = (𝑛))
72 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑛 = 𝑦 → (𝑛) = (𝑦))
7371, 72eqtrd 2644 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛 = 𝑦 → if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) = (𝑦))
7473sseq1d 3595 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑦 → (if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ⊆ (𝑦) ↔ (𝑦) ⊆ (𝑦)))
7574rspcev 3282 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦 ∈ (𝐴𝑚) ∧ (𝑦) ⊆ (𝑦)) → ∃𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ⊆ (𝑦))
7662, 75mpan2 703 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 ∈ (𝐴𝑚) → ∃𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ⊆ (𝑦))
77 iinss 4507 . . . . . . . . . . . . . . . . . . . . 21 (∃𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ⊆ (𝑦) → 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ⊆ (𝑦))
7876, 77syl 17 . . . . . . . . . . . . . . . . . . . 20 (𝑦 ∈ (𝐴𝑚) → 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ⊆ (𝑦))
7978adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝑦 ∈ (𝐴𝑚) ∧ (𝑦) ∈ (𝐹𝑦)) → 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ⊆ (𝑦))
8070, 79eqssd 3585 . . . . . . . . . . . . . . . . . 18 ((𝑦 ∈ (𝐴𝑚) ∧ (𝑦) ∈ (𝐹𝑦)) → (𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
8180ralimiaa 2935 . . . . . . . . . . . . . . . . 17 (∀𝑦 ∈ (𝐴𝑚)(𝑦) ∈ (𝐹𝑦) → ∀𝑦 ∈ (𝐴𝑚)(𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
8255, 57, 813syl 18 . . . . . . . . . . . . . . . 16 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → ∀𝑦 ∈ (𝐴𝑚)(𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
83 eldifn 3695 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 ∈ (𝐴𝑚) → ¬ 𝑦𝑚)
8483ad2antlr 759 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐴𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴𝑚)) ∧ 𝑛 ∈ (𝐴𝑚)) → ¬ 𝑦𝑚)
85 inss2 3796 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐴𝑚) ⊆ 𝑚
86 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝐴𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴𝑚)) ∧ 𝑛 ∈ (𝐴𝑚)) → 𝑛 ∈ (𝐴𝑚))
8785, 86sseldi 3566 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝐴𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴𝑚)) ∧ 𝑛 ∈ (𝐴𝑚)) → 𝑛𝑚)
88 eleq1 2676 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = 𝑛 → (𝑦𝑚𝑛𝑚))
8987, 88syl5ibrcom 236 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝐴𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴𝑚)) ∧ 𝑛 ∈ (𝐴𝑚)) → (𝑦 = 𝑛𝑦𝑚))
9084, 89mtod 188 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴𝑚)) ∧ 𝑛 ∈ (𝐴𝑚)) → ¬ 𝑦 = 𝑛)
9190, 59syl 17 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴𝑚)) ∧ 𝑛 ∈ (𝐴𝑚)) → if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) = (𝐹𝑦))
9291iineq2dv 4479 . . . . . . . . . . . . . . . . . . . 20 (((𝐴𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴𝑚)) → 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) = 𝑛 ∈ (𝐴𝑚) (𝐹𝑦))
93 iinconst 4466 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴𝑚) ≠ ∅ → 𝑛 ∈ (𝐴𝑚) (𝐹𝑦) = (𝐹𝑦))
9493adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝐴𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴𝑚)) → 𝑛 ∈ (𝐴𝑚) (𝐹𝑦) = (𝐹𝑦))
9592, 94eqtr2d 2645 . . . . . . . . . . . . . . . . . . 19 (((𝐴𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴𝑚)) → (𝐹𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
96 eqeq1 2614 . . . . . . . . . . . . . . . . . . 19 ((𝑦) = (𝐹𝑦) → ((𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ↔ (𝐹𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦))))
9795, 96syl5ibrcom 236 . . . . . . . . . . . . . . . . . 18 (((𝐴𝑚) ≠ ∅ ∧ 𝑦 ∈ (𝐴𝑚)) → ((𝑦) = (𝐹𝑦) → (𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦))))
9897ralimdva 2945 . . . . . . . . . . . . . . . . 17 ((𝐴𝑚) ≠ ∅ → (∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦) → ∀𝑦 ∈ (𝐴𝑚)(𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦))))
994, 98mpan9 485 . . . . . . . . . . . . . . . 16 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → ∀𝑦 ∈ (𝐴𝑚)(𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
100 inundif 3998 . . . . . . . . . . . . . . . . . 18 ((𝐴𝑚) ∪ (𝐴𝑚)) = 𝐴
101100raleqi 3119 . . . . . . . . . . . . . . . . 17 (∀𝑦 ∈ ((𝐴𝑚) ∪ (𝐴𝑚))(𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ↔ ∀𝑦𝐴 (𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
102 ralunb 3756 . . . . . . . . . . . . . . . . 17 (∀𝑦 ∈ ((𝐴𝑚) ∪ (𝐴𝑚))(𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ↔ (∀𝑦 ∈ (𝐴𝑚)(𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦))))
103101, 102bitr3i 265 . . . . . . . . . . . . . . . 16 (∀𝑦𝐴 (𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ↔ (∀𝑦 ∈ (𝐴𝑚)(𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦))))
10482, 99, 103sylanbrc 695 . . . . . . . . . . . . . . 15 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → ∀𝑦𝐴 (𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
105 ixpeq2 7808 . . . . . . . . . . . . . . 15 (∀𝑦𝐴 (𝑦) = 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) → X𝑦𝐴 (𝑦) = X𝑦𝐴 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
106104, 105syl 17 . . . . . . . . . . . . . 14 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → X𝑦𝐴 (𝑦) = X𝑦𝐴 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
107 ixpiin 7820 . . . . . . . . . . . . . . 15 ((𝐴𝑚) ≠ ∅ → X𝑦𝐴 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) = 𝑛 ∈ (𝐴𝑚)X𝑦𝐴 if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
108107adantl 481 . . . . . . . . . . . . . 14 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → X𝑦𝐴 𝑛 ∈ (𝐴𝑚)if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)) = 𝑛 ∈ (𝐴𝑚)X𝑦𝐴 if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
109106, 108eqtrd 2644 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → X𝑦𝐴 (𝑦) = 𝑛 ∈ (𝐴𝑚)X𝑦𝐴 if(𝑦 = 𝑛, (𝑛), (𝐹𝑦)))
11040, 54, 1093eqtr4rd 2655 . . . . . . . . . . . 12 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ (𝐴𝑚) ≠ ∅) → X𝑦𝐴 (𝑦) = (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))))
11125, 110pm2.61dane 2869 . . . . . . . . . . 11 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → X𝑦𝐴 (𝑦) = (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))))
112 ixpexg 7818 . . . . . . . . . . . . . . . . . . . . . . . 24 (∀𝑛𝐴 (𝐹𝑛) ∈ V → X𝑛𝐴 (𝐹𝑛) ∈ V)
113 fvex 6113 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝐹𝑛) ∈ V
114113uniex 6851 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝐹𝑛) ∈ V
115114a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑛𝐴 (𝐹𝑛) ∈ V)
116112, 115mprg 2910 . . . . . . . . . . . . . . . . . . . . . . 23 X𝑛𝐴 (𝐹𝑛) ∈ V
11710, 116eqeltri 2684 . . . . . . . . . . . . . . . . . . . . . 22 𝑋 ∈ V
118117mptex 6390 . . . . . . . . . . . . . . . . . . . . 21 (𝑤𝑋 ↦ (𝑤𝑛)) ∈ V
119118cnvex 7006 . . . . . . . . . . . . . . . . . . . 20 (𝑤𝑋 ↦ (𝑤𝑛)) ∈ V
120119imaex 6996 . . . . . . . . . . . . . . . . . . 19 ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ∈ V
121120dfiin2 4491 . . . . . . . . . . . . . . . . . 18 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) = {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))}
122 inteq 4413 . . . . . . . . . . . . . . . . . 18 ({𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} = ∅ → {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} = ∅)
123121, 122syl5eq 2656 . . . . . . . . . . . . . . . . 17 ({𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} = ∅ → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) = ∅)
124 int0 4425 . . . . . . . . . . . . . . . . 17 ∅ = V
125123, 124syl6eq 2660 . . . . . . . . . . . . . . . 16 ({𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} = ∅ → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) = V)
126125ineq2d 3776 . . . . . . . . . . . . . . 15 ({𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} = ∅ → (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) = (𝑋 ∩ V))
127 inv1 3922 . . . . . . . . . . . . . . 15 (𝑋 ∩ V) = 𝑋
128126, 127syl6eq 2660 . . . . . . . . . . . . . 14 ({𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} = ∅ → (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) = 𝑋)
129128adantl 481 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} = ∅) → (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) = 𝑋)
130 snex 4835 . . . . . . . . . . . . . . . . . 18 {𝑋} ∈ V
1311ptbas 21192 . . . . . . . . . . . . . . . . . . 19 ((𝐴𝑉𝐹:𝐴⟶Top) → 𝐵 ∈ TopBases)
1321, 10ptpjpre2 21193 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (𝑘𝐴𝑢 ∈ (𝐹𝑘))) → ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) ∈ 𝐵)
133132ralrimivva 2954 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴𝑉𝐹:𝐴⟶Top) → ∀𝑘𝐴𝑢 ∈ (𝐹𝑘)((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) ∈ 𝐵)
134 eqid 2610 . . . . . . . . . . . . . . . . . . . . . 22 (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)) = (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))
135134fmpt2x 7125 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑘𝐴𝑢 ∈ (𝐹𝑘)((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) ∈ 𝐵 ↔ (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)): 𝑘𝐴 ({𝑘} × (𝐹𝑘))⟶𝐵)
136133, 135sylib 207 . . . . . . . . . . . . . . . . . . . 20 ((𝐴𝑉𝐹:𝐴⟶Top) → (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)): 𝑘𝐴 ({𝑘} × (𝐹𝑘))⟶𝐵)
137 frn 5966 . . . . . . . . . . . . . . . . . . . 20 ((𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)): 𝑘𝐴 ({𝑘} × (𝐹𝑘))⟶𝐵 → ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)) ⊆ 𝐵)
138136, 137syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝐴𝑉𝐹:𝐴⟶Top) → ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)) ⊆ 𝐵)
139131, 138ssexd 4733 . . . . . . . . . . . . . . . . . 18 ((𝐴𝑉𝐹:𝐴⟶Top) → ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)) ∈ V)
140 unexg 6857 . . . . . . . . . . . . . . . . . 18 (({𝑋} ∈ V ∧ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)) ∈ V) → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ∈ V)
141130, 139, 140sylancr 694 . . . . . . . . . . . . . . . . 17 ((𝐴𝑉𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ∈ V)
142 ssfii 8208 . . . . . . . . . . . . . . . . 17 (({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ∈ V → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ⊆ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
143141, 142syl 17 . . . . . . . . . . . . . . . 16 ((𝐴𝑉𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ⊆ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
144143ad2antrr 758 . . . . . . . . . . . . . . 15 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ⊆ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
145 ssun1 3738 . . . . . . . . . . . . . . . . 17 {𝑋} ⊆ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))
146117snss 4259 . . . . . . . . . . . . . . . . 17 (𝑋 ∈ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ↔ {𝑋} ⊆ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))
147145, 146mpbir 220 . . . . . . . . . . . . . . . 16 𝑋 ∈ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))
148147a1i 11 . . . . . . . . . . . . . . 15 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → 𝑋 ∈ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))
149144, 148sseldd 3569 . . . . . . . . . . . . . 14 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → 𝑋 ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
150149adantr 480 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} = ∅) → 𝑋 ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
151129, 150eqeltrd 2688 . . . . . . . . . . . 12 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} = ∅) → (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
152141ad3antrrr 762 . . . . . . . . . . . . . . . . . 18 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ∈ V)
153 nfv 1830 . . . . . . . . . . . . . . . . . . . . . 22 𝑛(((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦)))
154 nfcv 2751 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑛𝐴
155 nfcv 2751 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑛(𝐹𝑘)
156 nfixp1 7814 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 𝑛X𝑛𝐴 (𝐹𝑛)
15710, 156nfcxfr 2749 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑛𝑋
158 nfcv 2751 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝑛(𝑤𝑘)
159157, 158nfmpt 4674 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑛(𝑤𝑋 ↦ (𝑤𝑘))
160159nfcnv 5223 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑛(𝑤𝑋 ↦ (𝑤𝑘))
161 nfcv 2751 . . . . . . . . . . . . . . . . . . . . . . . . . 26 𝑛𝑢
162160, 161nfima 5393 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑛((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)
163154, 155, 162nfmpt2 6622 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑛(𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))
164163nfrn 5289 . . . . . . . . . . . . . . . . . . . . . . 23 𝑛ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))
165164nfcri 2745 . . . . . . . . . . . . . . . . . . . . . 22 𝑛 𝑧 ∈ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))
166 df-ov 6552 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑛(𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))(𝑛)) = ((𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))‘⟨𝑛, (𝑛)⟩)
167120a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ∈ V)
168 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (𝑘 = 𝑛 → (𝑤𝑘) = (𝑤𝑛))
169168mpteq2dv 4673 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (𝑘 = 𝑛 → (𝑤𝑋 ↦ (𝑤𝑘)) = (𝑤𝑋 ↦ (𝑤𝑛)))
170169cnveqd 5220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (𝑘 = 𝑛(𝑤𝑋 ↦ (𝑤𝑘)) = (𝑤𝑋 ↦ (𝑤𝑛)))
171170imaeq1d 5384 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑘 = 𝑛 → ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) = ((𝑤𝑋 ↦ (𝑤𝑛)) “ 𝑢))
172 imaeq2 5381 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑢 = (𝑛) → ((𝑤𝑋 ↦ (𝑤𝑛)) “ 𝑢) = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
173171, 172sylan9eq 2664 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝑘 = 𝑛𝑢 = (𝑛)) → ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
174 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑘 = 𝑛 → (𝐹𝑘) = (𝐹𝑛))
175173, 174, 134ovmpt2x 6687 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑛𝐴 ∧ (𝑛) ∈ (𝐹𝑛) ∧ ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ∈ V) → (𝑛(𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))(𝑛)) = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
17629, 36, 167, 175syl3anc 1318 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → (𝑛(𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))(𝑛)) = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
177166, 176syl5eqr 2658 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → ((𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))‘⟨𝑛, (𝑛)⟩) = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
178136ad3antrrr 762 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)): 𝑘𝐴 ({𝑘} × (𝐹𝑘))⟶𝐵)
179178ffnd 5959 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)) Fn 𝑘𝐴 ({𝑘} × (𝐹𝑘)))
180 opeliunxp 5093 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (⟨𝑛, (𝑛)⟩ ∈ 𝑛𝐴 ({𝑛} × (𝐹𝑛)) ↔ (𝑛𝐴 ∧ (𝑛) ∈ (𝐹𝑛)))
18129, 36, 180sylanbrc 695 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → ⟨𝑛, (𝑛)⟩ ∈ 𝑛𝐴 ({𝑛} × (𝐹𝑛)))
182 sneq 4135 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 = 𝑘 → {𝑛} = {𝑘})
183 fveq2 6103 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑛 = 𝑘 → (𝐹𝑛) = (𝐹𝑘))
184182, 183xpeq12d 5064 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑛 = 𝑘 → ({𝑛} × (𝐹𝑛)) = ({𝑘} × (𝐹𝑘)))
185184cbviunv 4495 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝑛𝐴 ({𝑛} × (𝐹𝑛)) = 𝑘𝐴 ({𝑘} × (𝐹𝑘))
186181, 185syl6eleq 2698 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → ⟨𝑛, (𝑛)⟩ ∈ 𝑘𝐴 ({𝑘} × (𝐹𝑘)))
187 fnfvelrn 6264 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)) Fn 𝑘𝐴 ({𝑘} × (𝐹𝑘)) ∧ ⟨𝑛, (𝑛)⟩ ∈ 𝑘𝐴 ({𝑘} × (𝐹𝑘))) → ((𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))‘⟨𝑛, (𝑛)⟩) ∈ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))
188179, 186, 187syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → ((𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))‘⟨𝑛, (𝑛)⟩) ∈ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))
189177, 188eqeltrrd 2689 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ∈ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))
190 eleq1 2676 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) → (𝑧 ∈ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)) ↔ ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ∈ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))
191189, 190syl5ibrcom 236 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ 𝑛 ∈ (𝐴𝑚)) → (𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) → 𝑧 ∈ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))
192191ex 449 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → (𝑛 ∈ (𝐴𝑚) → (𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) → 𝑧 ∈ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
193153, 165, 192rexlimd 3008 . . . . . . . . . . . . . . . . . . . . 21 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → (∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) → 𝑧 ∈ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))
194193abssdv 3639 . . . . . . . . . . . . . . . . . . . 20 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ⊆ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))
195 ssun2 3739 . . . . . . . . . . . . . . . . . . . 20 ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)) ⊆ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))
196194, 195syl6ss 3580 . . . . . . . . . . . . . . . . . . 19 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ⊆ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))
197196adantr 480 . . . . . . . . . . . . . . . . . 18 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ⊆ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))
198 simpr 476 . . . . . . . . . . . . . . . . . 18 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅)
199 simplrl 796 . . . . . . . . . . . . . . . . . . . 20 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → 𝑚 ∈ Fin)
200 ssfi 8065 . . . . . . . . . . . . . . . . . . . 20 ((𝑚 ∈ Fin ∧ (𝐴𝑚) ⊆ 𝑚) → (𝐴𝑚) ∈ Fin)
201199, 85, 200sylancl 693 . . . . . . . . . . . . . . . . . . 19 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → (𝐴𝑚) ∈ Fin)
202 abrexfi 8149 . . . . . . . . . . . . . . . . . . 19 ((𝐴𝑚) ∈ Fin → {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ∈ Fin)
203201, 202syl 17 . . . . . . . . . . . . . . . . . 18 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ∈ Fin)
204 elfir 8204 . . . . . . . . . . . . . . . . . 18 ((({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ∈ V ∧ ({𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ⊆ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅ ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ∈ Fin)) → {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
205152, 197, 198, 203, 204syl13anc 1320 . . . . . . . . . . . . . . . . 17 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
206121, 205syl5eqel 2692 . . . . . . . . . . . . . . . 16 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
207 elssuni 4403 . . . . . . . . . . . . . . . 16 ( 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))) → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
208206, 207syl 17 . . . . . . . . . . . . . . 15 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
209 fiuni 8217 . . . . . . . . . . . . . . . . . 18 (({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ∈ V → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) = (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
210141, 209syl 17 . . . . . . . . . . . . . . . . 17 ((𝐴𝑉𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) = (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
211117pwid 4122 . . . . . . . . . . . . . . . . . . . . . 22 𝑋 ∈ 𝒫 𝑋
212211a1i 11 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴𝑉𝐹:𝐴⟶Top) → 𝑋 ∈ 𝒫 𝑋)
213212snssd 4281 . . . . . . . . . . . . . . . . . . . 20 ((𝐴𝑉𝐹:𝐴⟶Top) → {𝑋} ⊆ 𝒫 𝑋)
2141ptuni2 21189 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐴𝑉𝐹:𝐴⟶Top) → X𝑛𝐴 (𝐹𝑛) = 𝐵)
21510, 214syl5eq 2656 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴𝑉𝐹:𝐴⟶Top) → 𝑋 = 𝐵)
216 eqimss2 3621 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑋 = 𝐵 𝐵𝑋)
217215, 216syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴𝑉𝐹:𝐴⟶Top) → 𝐵𝑋)
218 sspwuni 4547 . . . . . . . . . . . . . . . . . . . . . 22 (𝐵 ⊆ 𝒫 𝑋 𝐵𝑋)
219217, 218sylibr 223 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴𝑉𝐹:𝐴⟶Top) → 𝐵 ⊆ 𝒫 𝑋)
220138, 219sstrd 3578 . . . . . . . . . . . . . . . . . . . 20 ((𝐴𝑉𝐹:𝐴⟶Top) → ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)) ⊆ 𝒫 𝑋)
221213, 220unssd 3751 . . . . . . . . . . . . . . . . . . 19 ((𝐴𝑉𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ⊆ 𝒫 𝑋)
222 sspwuni 4547 . . . . . . . . . . . . . . . . . . 19 (({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ⊆ 𝒫 𝑋 ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ⊆ 𝑋)
223221, 222sylib 207 . . . . . . . . . . . . . . . . . 18 ((𝐴𝑉𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ⊆ 𝑋)
224 elssuni 4403 . . . . . . . . . . . . . . . . . . 19 (𝑋 ∈ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) → 𝑋 ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))
225147, 224mp1i 13 . . . . . . . . . . . . . . . . . 18 ((𝐴𝑉𝐹:𝐴⟶Top) → 𝑋 ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))
226223, 225eqssd 3585 . . . . . . . . . . . . . . . . 17 ((𝐴𝑉𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) = 𝑋)
227210, 226eqtr3d 2646 . . . . . . . . . . . . . . . 16 ((𝐴𝑉𝐹:𝐴⟶Top) → (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))) = 𝑋)
228227ad3antrrr 762 . . . . . . . . . . . . . . 15 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))) = 𝑋)
229208, 228sseqtrd 3604 . . . . . . . . . . . . . 14 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)) ⊆ 𝑋)
230229, 53sylib 207 . . . . . . . . . . . . 13 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) = 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛)))
231230, 206eqeltrd 2688 . . . . . . . . . . . 12 (((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) ∧ {𝑧 ∣ ∃𝑛 ∈ (𝐴𝑚)𝑧 = ((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))} ≠ ∅) → (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
232151, 231pm2.61dane 2869 . . . . . . . . . . 11 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → (𝑋 𝑛 ∈ (𝐴𝑚)((𝑤𝑋 ↦ (𝑤𝑛)) “ (𝑛))) ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
233111, 232eqeltrd 2688 . . . . . . . . . 10 ((((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) ∧ (𝑚 ∈ Fin ∧ ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → X𝑦𝐴 (𝑦) ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
234233rexlimdvaa 3014 . . . . . . . . 9 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦))) → (∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦) → X𝑦𝐴 (𝑦) ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))))
235234impr 647 . . . . . . . 8 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ (( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦)) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → X𝑦𝐴 (𝑦) ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
2363, 235sylan2b 491 . . . . . . 7 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → X𝑦𝐴 (𝑦) ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
237 eleq1 2676 . . . . . . 7 (𝑠 = X𝑦𝐴 (𝑦) → (𝑠 ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))) ↔ X𝑦𝐴 (𝑦) ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))))
238236, 237syl5ibrcom 236 . . . . . 6 (((𝐴𝑉𝐹:𝐴⟶Top) ∧ ( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦))) → (𝑠 = X𝑦𝐴 (𝑦) → 𝑠 ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))))
239238expimpd 627 . . . . 5 ((𝐴𝑉𝐹:𝐴⟶Top) → ((( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑦)) → 𝑠 ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))))
240239exlimdv 1848 . . . 4 ((𝐴𝑉𝐹:𝐴⟶Top) → (∃(( Fn 𝐴 ∧ ∀𝑦𝐴 (𝑦) ∈ (𝐹𝑦) ∧ ∃𝑚 ∈ Fin ∀𝑦 ∈ (𝐴𝑚)(𝑦) = (𝐹𝑦)) ∧ 𝑠 = X𝑦𝐴 (𝑦)) → 𝑠 ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))))
2412, 240syl5bi 231 . . 3 ((𝐴𝑉𝐹:𝐴⟶Top) → (𝑠𝐵𝑠 ∈ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))))))
242241ssrdv 3574 . 2 ((𝐴𝑉𝐹:𝐴⟶Top) → 𝐵 ⊆ (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
2431ptbasid 21188 . . . . . . 7 ((𝐴𝑉𝐹:𝐴⟶Top) → X𝑛𝐴 (𝐹𝑛) ∈ 𝐵)
24410, 243syl5eqel 2692 . . . . . 6 ((𝐴𝑉𝐹:𝐴⟶Top) → 𝑋𝐵)
245244snssd 4281 . . . . 5 ((𝐴𝑉𝐹:𝐴⟶Top) → {𝑋} ⊆ 𝐵)
246245, 138unssd 3751 . . . 4 ((𝐴𝑉𝐹:𝐴⟶Top) → ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ⊆ 𝐵)
247 fiss 8213 . . . 4 ((𝐵 ∈ TopBases ∧ ({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))) ⊆ 𝐵) → (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))) ⊆ (fi‘𝐵))
248131, 246, 247syl2anc 691 . . 3 ((𝐴𝑉𝐹:𝐴⟶Top) → (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))) ⊆ (fi‘𝐵))
2491ptbasin2 21191 . . 3 ((𝐴𝑉𝐹:𝐴⟶Top) → (fi‘𝐵) = 𝐵)
250248, 249sseqtrd 3604 . 2 ((𝐴𝑉𝐹:𝐴⟶Top) → (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))) ⊆ 𝐵)
251242, 250eqssd 3585 1 ((𝐴𝑉𝐹:𝐴⟶Top) → 𝐵 = (fi‘({𝑋} ∪ ran (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢)))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383   ∧ w3a 1031   = wceq 1475  ∃wex 1695   ∈ wcel 1977  {cab 2596   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  Vcvv 3173   ∖ cdif 3537   ∪ cun 3538   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874  ifcif 4036  𝒫 cpw 4108  {csn 4125  ⟨cop 4131  ∪ cuni 4372  ∩ cint 4410  ∪ ciun 4455  ∩ ciin 4456   ↦ cmpt 4643   × cxp 5036  ◡ccnv 5037  dom cdm 5038  ran crn 5039   “ cima 5041   Fn wfn 5799  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549   ↦ cmpt2 6551  Xcixp 7794  Fincfn 7841  ficfi 8199  Topctop 20517  TopBasesctb 20520 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-iin 4458  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-ixp 7795  df-en 7842  df-dom 7843  df-fin 7845  df-fi 8200  df-top 20521  df-bases 20522 This theorem is referenced by:  ptval2  21214  xkoptsub  21267  ptcmplem1  21666  prdsxmslem2  22144
 Copyright terms: Public domain W3C validator