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 𝐾 ) )