Metamath Proof Explorer


Theorem ptrescn

Description: Restriction is a continuous function on product topologies. (Contributed by Mario Carneiro, 7-Feb-2015)

Ref Expression
Hypotheses ptrescn.1 𝑋 = 𝐽
ptrescn.2 𝐽 = ( ∏t𝐹 )
ptrescn.3 𝐾 = ( ∏t ‘ ( 𝐹𝐵 ) )
Assertion ptrescn ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) → ( 𝑥𝑋 ↦ ( 𝑥𝐵 ) ) ∈ ( 𝐽 Cn 𝐾 ) )

Proof

Step Hyp Ref Expression
1 ptrescn.1 𝑋 = 𝐽
2 ptrescn.2 𝐽 = ( ∏t𝐹 )
3 ptrescn.3 𝐾 = ( ∏t ‘ ( 𝐹𝐵 ) )
4 simpl3 ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) ∧ 𝑥𝑋 ) → 𝐵𝐴 )
5 2 ptuni ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) → X 𝑘𝐴 ( 𝐹𝑘 ) = 𝐽 )
6 5 3adant3 ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) → X 𝑘𝐴 ( 𝐹𝑘 ) = 𝐽 )
7 6 1 eqtr4di ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) → X 𝑘𝐴 ( 𝐹𝑘 ) = 𝑋 )
8 7 eleq2d ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) → ( 𝑥X 𝑘𝐴 ( 𝐹𝑘 ) ↔ 𝑥𝑋 ) )
9 8 biimpar ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) ∧ 𝑥𝑋 ) → 𝑥X 𝑘𝐴 ( 𝐹𝑘 ) )
10 resixp ( ( 𝐵𝐴𝑥X 𝑘𝐴 ( 𝐹𝑘 ) ) → ( 𝑥𝐵 ) ∈ X 𝑘𝐵 ( 𝐹𝑘 ) )
11 4 9 10 syl2anc ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) ∧ 𝑥𝑋 ) → ( 𝑥𝐵 ) ∈ X 𝑘𝐵 ( 𝐹𝑘 ) )
12 ixpeq2 ( ∀ 𝑘𝐵 ( ( 𝐹𝐵 ) ‘ 𝑘 ) = ( 𝐹𝑘 ) → X 𝑘𝐵 ( ( 𝐹𝐵 ) ‘ 𝑘 ) = X 𝑘𝐵 ( 𝐹𝑘 ) )
13 fvres ( 𝑘𝐵 → ( ( 𝐹𝐵 ) ‘ 𝑘 ) = ( 𝐹𝑘 ) )
14 13 unieqd ( 𝑘𝐵 ( ( 𝐹𝐵 ) ‘ 𝑘 ) = ( 𝐹𝑘 ) )
15 12 14 mprg X 𝑘𝐵 ( ( 𝐹𝐵 ) ‘ 𝑘 ) = X 𝑘𝐵 ( 𝐹𝑘 )
16 ssexg ( ( 𝐵𝐴𝐴𝑉 ) → 𝐵 ∈ V )
17 16 ancoms ( ( 𝐴𝑉𝐵𝐴 ) → 𝐵 ∈ V )
18 17 3adant2 ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) → 𝐵 ∈ V )
19 fssres ( ( 𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) → ( 𝐹𝐵 ) : 𝐵 ⟶ Top )
20 19 3adant1 ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) → ( 𝐹𝐵 ) : 𝐵 ⟶ Top )
21 3 ptuni ( ( 𝐵 ∈ V ∧ ( 𝐹𝐵 ) : 𝐵 ⟶ Top ) → X 𝑘𝐵 ( ( 𝐹𝐵 ) ‘ 𝑘 ) = 𝐾 )
22 18 20 21 syl2anc ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) → X 𝑘𝐵 ( ( 𝐹𝐵 ) ‘ 𝑘 ) = 𝐾 )
23 15 22 eqtr3id ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) → X 𝑘𝐵 ( 𝐹𝑘 ) = 𝐾 )
24 23 adantr ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) ∧ 𝑥𝑋 ) → X 𝑘𝐵 ( 𝐹𝑘 ) = 𝐾 )
25 11 24 eleqtrd ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) ∧ 𝑥𝑋 ) → ( 𝑥𝐵 ) ∈ 𝐾 )
26 25 fmpttd ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) → ( 𝑥𝑋 ↦ ( 𝑥𝐵 ) ) : 𝑋 𝐾 )
27 fimacnv ( ( 𝑥𝑋 ↦ ( 𝑥𝐵 ) ) : 𝑋 𝐾 → ( ( 𝑥𝑋 ↦ ( 𝑥𝐵 ) ) “ 𝐾 ) = 𝑋 )
28 26 27 syl ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) → ( ( 𝑥𝑋 ↦ ( 𝑥𝐵 ) ) “ 𝐾 ) = 𝑋 )
29 pttop ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) → ( ∏t𝐹 ) ∈ Top )
30 2 29 eqeltrid ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ) → 𝐽 ∈ Top )
31 30 3adant3 ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) → 𝐽 ∈ Top )
32 1 topopn ( 𝐽 ∈ Top → 𝑋𝐽 )
33 31 32 syl ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) → 𝑋𝐽 )
34 28 33 eqeltrd ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) → ( ( 𝑥𝑋 ↦ ( 𝑥𝐵 ) ) “ 𝐾 ) ∈ 𝐽 )
35 elsni ( 𝑣 ∈ { 𝐾 } → 𝑣 = 𝐾 )
36 35 imaeq2d ( 𝑣 ∈ { 𝐾 } → ( ( 𝑥𝑋 ↦ ( 𝑥𝐵 ) ) “ 𝑣 ) = ( ( 𝑥𝑋 ↦ ( 𝑥𝐵 ) ) “ 𝐾 ) )
37 36 eleq1d ( 𝑣 ∈ { 𝐾 } → ( ( ( 𝑥𝑋 ↦ ( 𝑥𝐵 ) ) “ 𝑣 ) ∈ 𝐽 ↔ ( ( 𝑥𝑋 ↦ ( 𝑥𝐵 ) ) “ 𝐾 ) ∈ 𝐽 ) )
38 34 37 syl5ibrcom ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) → ( 𝑣 ∈ { 𝐾 } → ( ( 𝑥𝑋 ↦ ( 𝑥𝐵 ) ) “ 𝑣 ) ∈ 𝐽 ) )
39 38 ralrimiv ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) → ∀ 𝑣 ∈ { 𝐾 } ( ( 𝑥𝑋 ↦ ( 𝑥𝐵 ) ) “ 𝑣 ) ∈ 𝐽 )
40 imaco ( ( ( 𝑥𝑋 ↦ ( 𝑥𝐵 ) ) ∘ ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) ) “ 𝑢 ) = ( ( 𝑥𝑋 ↦ ( 𝑥𝐵 ) ) “ ( ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) “ 𝑢 ) )
41 cnvco ( ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) ∘ ( 𝑥𝑋 ↦ ( 𝑥𝐵 ) ) ) = ( ( 𝑥𝑋 ↦ ( 𝑥𝐵 ) ) ∘ ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) )
42 25 adantlr ( ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) ∧ ( 𝑘𝐵𝑢 ∈ ( 𝐹𝑘 ) ) ) ∧ 𝑥𝑋 ) → ( 𝑥𝐵 ) ∈ 𝐾 )
43 eqidd ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) ∧ ( 𝑘𝐵𝑢 ∈ ( 𝐹𝑘 ) ) ) → ( 𝑥𝑋 ↦ ( 𝑥𝐵 ) ) = ( 𝑥𝑋 ↦ ( 𝑥𝐵 ) ) )
44 eqidd ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) ∧ ( 𝑘𝐵𝑢 ∈ ( 𝐹𝑘 ) ) ) → ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) = ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) )
45 fveq1 ( 𝑧 = ( 𝑥𝐵 ) → ( 𝑧𝑘 ) = ( ( 𝑥𝐵 ) ‘ 𝑘 ) )
46 42 43 44 45 fmptco ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) ∧ ( 𝑘𝐵𝑢 ∈ ( 𝐹𝑘 ) ) ) → ( ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) ∘ ( 𝑥𝑋 ↦ ( 𝑥𝐵 ) ) ) = ( 𝑥𝑋 ↦ ( ( 𝑥𝐵 ) ‘ 𝑘 ) ) )
47 fvres ( 𝑘𝐵 → ( ( 𝑥𝐵 ) ‘ 𝑘 ) = ( 𝑥𝑘 ) )
48 47 ad2antrl ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) ∧ ( 𝑘𝐵𝑢 ∈ ( 𝐹𝑘 ) ) ) → ( ( 𝑥𝐵 ) ‘ 𝑘 ) = ( 𝑥𝑘 ) )
49 48 mpteq2dv ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) ∧ ( 𝑘𝐵𝑢 ∈ ( 𝐹𝑘 ) ) ) → ( 𝑥𝑋 ↦ ( ( 𝑥𝐵 ) ‘ 𝑘 ) ) = ( 𝑥𝑋 ↦ ( 𝑥𝑘 ) ) )
50 46 49 eqtrd ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) ∧ ( 𝑘𝐵𝑢 ∈ ( 𝐹𝑘 ) ) ) → ( ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) ∘ ( 𝑥𝑋 ↦ ( 𝑥𝐵 ) ) ) = ( 𝑥𝑋 ↦ ( 𝑥𝑘 ) ) )
51 50 cnveqd ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) ∧ ( 𝑘𝐵𝑢 ∈ ( 𝐹𝑘 ) ) ) → ( ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) ∘ ( 𝑥𝑋 ↦ ( 𝑥𝐵 ) ) ) = ( 𝑥𝑋 ↦ ( 𝑥𝑘 ) ) )
52 41 51 eqtr3id ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) ∧ ( 𝑘𝐵𝑢 ∈ ( 𝐹𝑘 ) ) ) → ( ( 𝑥𝑋 ↦ ( 𝑥𝐵 ) ) ∘ ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) ) = ( 𝑥𝑋 ↦ ( 𝑥𝑘 ) ) )
53 52 imaeq1d ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) ∧ ( 𝑘𝐵𝑢 ∈ ( 𝐹𝑘 ) ) ) → ( ( ( 𝑥𝑋 ↦ ( 𝑥𝐵 ) ) ∘ ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) ) “ 𝑢 ) = ( ( 𝑥𝑋 ↦ ( 𝑥𝑘 ) ) “ 𝑢 ) )
54 40 53 eqtr3id ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) ∧ ( 𝑘𝐵𝑢 ∈ ( 𝐹𝑘 ) ) ) → ( ( 𝑥𝑋 ↦ ( 𝑥𝐵 ) ) “ ( ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) “ 𝑢 ) ) = ( ( 𝑥𝑋 ↦ ( 𝑥𝑘 ) ) “ 𝑢 ) )
55 simpl1 ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) ∧ ( 𝑘𝐵𝑢 ∈ ( 𝐹𝑘 ) ) ) → 𝐴𝑉 )
56 simpl2 ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) ∧ ( 𝑘𝐵𝑢 ∈ ( 𝐹𝑘 ) ) ) → 𝐹 : 𝐴 ⟶ Top )
57 simpl3 ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) ∧ ( 𝑘𝐵𝑢 ∈ ( 𝐹𝑘 ) ) ) → 𝐵𝐴 )
58 simprl ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) ∧ ( 𝑘𝐵𝑢 ∈ ( 𝐹𝑘 ) ) ) → 𝑘𝐵 )
59 57 58 sseldd ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) ∧ ( 𝑘𝐵𝑢 ∈ ( 𝐹𝑘 ) ) ) → 𝑘𝐴 )
60 1 2 ptpjcn ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝑘𝐴 ) → ( 𝑥𝑋 ↦ ( 𝑥𝑘 ) ) ∈ ( 𝐽 Cn ( 𝐹𝑘 ) ) )
61 55 56 59 60 syl3anc ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) ∧ ( 𝑘𝐵𝑢 ∈ ( 𝐹𝑘 ) ) ) → ( 𝑥𝑋 ↦ ( 𝑥𝑘 ) ) ∈ ( 𝐽 Cn ( 𝐹𝑘 ) ) )
62 simprr ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) ∧ ( 𝑘𝐵𝑢 ∈ ( 𝐹𝑘 ) ) ) → 𝑢 ∈ ( 𝐹𝑘 ) )
63 cnima ( ( ( 𝑥𝑋 ↦ ( 𝑥𝑘 ) ) ∈ ( 𝐽 Cn ( 𝐹𝑘 ) ) ∧ 𝑢 ∈ ( 𝐹𝑘 ) ) → ( ( 𝑥𝑋 ↦ ( 𝑥𝑘 ) ) “ 𝑢 ) ∈ 𝐽 )
64 61 62 63 syl2anc ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) ∧ ( 𝑘𝐵𝑢 ∈ ( 𝐹𝑘 ) ) ) → ( ( 𝑥𝑋 ↦ ( 𝑥𝑘 ) ) “ 𝑢 ) ∈ 𝐽 )
65 54 64 eqeltrd ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) ∧ ( 𝑘𝐵𝑢 ∈ ( 𝐹𝑘 ) ) ) → ( ( 𝑥𝑋 ↦ ( 𝑥𝐵 ) ) “ ( ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) “ 𝑢 ) ) ∈ 𝐽 )
66 imaeq2 ( 𝑣 = ( ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) “ 𝑢 ) → ( ( 𝑥𝑋 ↦ ( 𝑥𝐵 ) ) “ 𝑣 ) = ( ( 𝑥𝑋 ↦ ( 𝑥𝐵 ) ) “ ( ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) “ 𝑢 ) ) )
67 66 eleq1d ( 𝑣 = ( ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) “ 𝑢 ) → ( ( ( 𝑥𝑋 ↦ ( 𝑥𝐵 ) ) “ 𝑣 ) ∈ 𝐽 ↔ ( ( 𝑥𝑋 ↦ ( 𝑥𝐵 ) ) “ ( ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) “ 𝑢 ) ) ∈ 𝐽 ) )
68 65 67 syl5ibrcom ( ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) ∧ ( 𝑘𝐵𝑢 ∈ ( 𝐹𝑘 ) ) ) → ( 𝑣 = ( ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) “ 𝑢 ) → ( ( 𝑥𝑋 ↦ ( 𝑥𝐵 ) ) “ 𝑣 ) ∈ 𝐽 ) )
69 68 rexlimdvva ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) → ( ∃ 𝑘𝐵𝑢 ∈ ( 𝐹𝑘 ) 𝑣 = ( ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) “ 𝑢 ) → ( ( 𝑥𝑋 ↦ ( 𝑥𝐵 ) ) “ 𝑣 ) ∈ 𝐽 ) )
70 69 alrimiv ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) → ∀ 𝑣 ( ∃ 𝑘𝐵𝑢 ∈ ( 𝐹𝑘 ) 𝑣 = ( ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) “ 𝑢 ) → ( ( 𝑥𝑋 ↦ ( 𝑥𝐵 ) ) “ 𝑣 ) ∈ 𝐽 ) )
71 eqid ( 𝑘𝐵 , 𝑢 ∈ ( ( 𝐹𝐵 ) ‘ 𝑘 ) ↦ ( ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) “ 𝑢 ) ) = ( 𝑘𝐵 , 𝑢 ∈ ( ( 𝐹𝐵 ) ‘ 𝑘 ) ↦ ( ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) “ 𝑢 ) )
72 71 rnmpo ran ( 𝑘𝐵 , 𝑢 ∈ ( ( 𝐹𝐵 ) ‘ 𝑘 ) ↦ ( ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) “ 𝑢 ) ) = { 𝑦 ∣ ∃ 𝑘𝐵𝑢 ∈ ( ( 𝐹𝐵 ) ‘ 𝑘 ) 𝑦 = ( ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) “ 𝑢 ) }
73 72 raleqi ( ∀ 𝑣 ∈ ran ( 𝑘𝐵 , 𝑢 ∈ ( ( 𝐹𝐵 ) ‘ 𝑘 ) ↦ ( ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) “ 𝑢 ) ) ( ( 𝑥𝑋 ↦ ( 𝑥𝐵 ) ) “ 𝑣 ) ∈ 𝐽 ↔ ∀ 𝑣 ∈ { 𝑦 ∣ ∃ 𝑘𝐵𝑢 ∈ ( ( 𝐹𝐵 ) ‘ 𝑘 ) 𝑦 = ( ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) “ 𝑢 ) } ( ( 𝑥𝑋 ↦ ( 𝑥𝐵 ) ) “ 𝑣 ) ∈ 𝐽 )
74 13 rexeqdv ( 𝑘𝐵 → ( ∃ 𝑢 ∈ ( ( 𝐹𝐵 ) ‘ 𝑘 ) 𝑦 = ( ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) “ 𝑢 ) ↔ ∃ 𝑢 ∈ ( 𝐹𝑘 ) 𝑦 = ( ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) “ 𝑢 ) ) )
75 eqeq1 ( 𝑦 = 𝑣 → ( 𝑦 = ( ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) “ 𝑢 ) ↔ 𝑣 = ( ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) “ 𝑢 ) ) )
76 75 rexbidv ( 𝑦 = 𝑣 → ( ∃ 𝑢 ∈ ( 𝐹𝑘 ) 𝑦 = ( ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) “ 𝑢 ) ↔ ∃ 𝑢 ∈ ( 𝐹𝑘 ) 𝑣 = ( ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) “ 𝑢 ) ) )
77 74 76 sylan9bbr ( ( 𝑦 = 𝑣𝑘𝐵 ) → ( ∃ 𝑢 ∈ ( ( 𝐹𝐵 ) ‘ 𝑘 ) 𝑦 = ( ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) “ 𝑢 ) ↔ ∃ 𝑢 ∈ ( 𝐹𝑘 ) 𝑣 = ( ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) “ 𝑢 ) ) )
78 77 rexbidva ( 𝑦 = 𝑣 → ( ∃ 𝑘𝐵𝑢 ∈ ( ( 𝐹𝐵 ) ‘ 𝑘 ) 𝑦 = ( ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) “ 𝑢 ) ↔ ∃ 𝑘𝐵𝑢 ∈ ( 𝐹𝑘 ) 𝑣 = ( ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) “ 𝑢 ) ) )
79 78 ralab ( ∀ 𝑣 ∈ { 𝑦 ∣ ∃ 𝑘𝐵𝑢 ∈ ( ( 𝐹𝐵 ) ‘ 𝑘 ) 𝑦 = ( ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) “ 𝑢 ) } ( ( 𝑥𝑋 ↦ ( 𝑥𝐵 ) ) “ 𝑣 ) ∈ 𝐽 ↔ ∀ 𝑣 ( ∃ 𝑘𝐵𝑢 ∈ ( 𝐹𝑘 ) 𝑣 = ( ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) “ 𝑢 ) → ( ( 𝑥𝑋 ↦ ( 𝑥𝐵 ) ) “ 𝑣 ) ∈ 𝐽 ) )
80 73 79 bitri ( ∀ 𝑣 ∈ ran ( 𝑘𝐵 , 𝑢 ∈ ( ( 𝐹𝐵 ) ‘ 𝑘 ) ↦ ( ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) “ 𝑢 ) ) ( ( 𝑥𝑋 ↦ ( 𝑥𝐵 ) ) “ 𝑣 ) ∈ 𝐽 ↔ ∀ 𝑣 ( ∃ 𝑘𝐵𝑢 ∈ ( 𝐹𝑘 ) 𝑣 = ( ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) “ 𝑢 ) → ( ( 𝑥𝑋 ↦ ( 𝑥𝐵 ) ) “ 𝑣 ) ∈ 𝐽 ) )
81 70 80 sylibr ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) → ∀ 𝑣 ∈ ran ( 𝑘𝐵 , 𝑢 ∈ ( ( 𝐹𝐵 ) ‘ 𝑘 ) ↦ ( ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) “ 𝑢 ) ) ( ( 𝑥𝑋 ↦ ( 𝑥𝐵 ) ) “ 𝑣 ) ∈ 𝐽 )
82 ralunb ( ∀ 𝑣 ∈ ( { 𝐾 } ∪ ran ( 𝑘𝐵 , 𝑢 ∈ ( ( 𝐹𝐵 ) ‘ 𝑘 ) ↦ ( ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) “ 𝑢 ) ) ) ( ( 𝑥𝑋 ↦ ( 𝑥𝐵 ) ) “ 𝑣 ) ∈ 𝐽 ↔ ( ∀ 𝑣 ∈ { 𝐾 } ( ( 𝑥𝑋 ↦ ( 𝑥𝐵 ) ) “ 𝑣 ) ∈ 𝐽 ∧ ∀ 𝑣 ∈ ran ( 𝑘𝐵 , 𝑢 ∈ ( ( 𝐹𝐵 ) ‘ 𝑘 ) ↦ ( ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) “ 𝑢 ) ) ( ( 𝑥𝑋 ↦ ( 𝑥𝐵 ) ) “ 𝑣 ) ∈ 𝐽 ) )
83 39 81 82 sylanbrc ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) → ∀ 𝑣 ∈ ( { 𝐾 } ∪ ran ( 𝑘𝐵 , 𝑢 ∈ ( ( 𝐹𝐵 ) ‘ 𝑘 ) ↦ ( ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) “ 𝑢 ) ) ) ( ( 𝑥𝑋 ↦ ( 𝑥𝐵 ) ) “ 𝑣 ) ∈ 𝐽 )
84 1 toptopon ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
85 31 84 sylib ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
86 snex { 𝐾 } ∈ V
87 fvex ( ( 𝐹𝐵 ) ‘ 𝑘 ) ∈ V
88 87 abrexex { 𝑦 ∣ ∃ 𝑢 ∈ ( ( 𝐹𝐵 ) ‘ 𝑘 ) 𝑦 = ( ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) “ 𝑢 ) } ∈ V
89 88 rgenw 𝑘𝐵 { 𝑦 ∣ ∃ 𝑢 ∈ ( ( 𝐹𝐵 ) ‘ 𝑘 ) 𝑦 = ( ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) “ 𝑢 ) } ∈ V
90 abrexex2g ( ( 𝐵 ∈ V ∧ ∀ 𝑘𝐵 { 𝑦 ∣ ∃ 𝑢 ∈ ( ( 𝐹𝐵 ) ‘ 𝑘 ) 𝑦 = ( ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) “ 𝑢 ) } ∈ V ) → { 𝑦 ∣ ∃ 𝑘𝐵𝑢 ∈ ( ( 𝐹𝐵 ) ‘ 𝑘 ) 𝑦 = ( ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) “ 𝑢 ) } ∈ V )
91 18 89 90 sylancl ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) → { 𝑦 ∣ ∃ 𝑘𝐵𝑢 ∈ ( ( 𝐹𝐵 ) ‘ 𝑘 ) 𝑦 = ( ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) “ 𝑢 ) } ∈ V )
92 72 91 eqeltrid ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) → ran ( 𝑘𝐵 , 𝑢 ∈ ( ( 𝐹𝐵 ) ‘ 𝑘 ) ↦ ( ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) “ 𝑢 ) ) ∈ V )
93 unexg ( ( { 𝐾 } ∈ V ∧ ran ( 𝑘𝐵 , 𝑢 ∈ ( ( 𝐹𝐵 ) ‘ 𝑘 ) ↦ ( ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) “ 𝑢 ) ) ∈ V ) → ( { 𝐾 } ∪ ran ( 𝑘𝐵 , 𝑢 ∈ ( ( 𝐹𝐵 ) ‘ 𝑘 ) ↦ ( ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) “ 𝑢 ) ) ) ∈ V )
94 86 92 93 sylancr ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) → ( { 𝐾 } ∪ ran ( 𝑘𝐵 , 𝑢 ∈ ( ( 𝐹𝐵 ) ‘ 𝑘 ) ↦ ( ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) “ 𝑢 ) ) ) ∈ V )
95 eqid 𝐾 = 𝐾
96 3 95 71 ptval2 ( ( 𝐵 ∈ V ∧ ( 𝐹𝐵 ) : 𝐵 ⟶ Top ) → 𝐾 = ( topGen ‘ ( fi ‘ ( { 𝐾 } ∪ ran ( 𝑘𝐵 , 𝑢 ∈ ( ( 𝐹𝐵 ) ‘ 𝑘 ) ↦ ( ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) “ 𝑢 ) ) ) ) ) )
97 18 20 96 syl2anc ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) → 𝐾 = ( topGen ‘ ( fi ‘ ( { 𝐾 } ∪ ran ( 𝑘𝐵 , 𝑢 ∈ ( ( 𝐹𝐵 ) ‘ 𝑘 ) ↦ ( ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) “ 𝑢 ) ) ) ) ) )
98 pttop ( ( 𝐵 ∈ V ∧ ( 𝐹𝐵 ) : 𝐵 ⟶ Top ) → ( ∏t ‘ ( 𝐹𝐵 ) ) ∈ Top )
99 18 20 98 syl2anc ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) → ( ∏t ‘ ( 𝐹𝐵 ) ) ∈ Top )
100 3 99 eqeltrid ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) → 𝐾 ∈ Top )
101 95 toptopon ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ 𝐾 ) )
102 100 101 sylib ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) → 𝐾 ∈ ( TopOn ‘ 𝐾 ) )
103 85 94 97 102 subbascn ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) → ( ( 𝑥𝑋 ↦ ( 𝑥𝐵 ) ) ∈ ( 𝐽 Cn 𝐾 ) ↔ ( ( 𝑥𝑋 ↦ ( 𝑥𝐵 ) ) : 𝑋 𝐾 ∧ ∀ 𝑣 ∈ ( { 𝐾 } ∪ ran ( 𝑘𝐵 , 𝑢 ∈ ( ( 𝐹𝐵 ) ‘ 𝑘 ) ↦ ( ( 𝑧 𝐾 ↦ ( 𝑧𝑘 ) ) “ 𝑢 ) ) ) ( ( 𝑥𝑋 ↦ ( 𝑥𝐵 ) ) “ 𝑣 ) ∈ 𝐽 ) ) )
104 26 83 103 mpbir2and ( ( 𝐴𝑉𝐹 : 𝐴 ⟶ Top ∧ 𝐵𝐴 ) → ( 𝑥𝑋 ↦ ( 𝑥𝐵 ) ) ∈ ( 𝐽 Cn 𝐾 ) )