Metamath Proof Explorer


Theorem cnmpopc

Description: Piecewise definition of a continuous function on a real interval. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 5-Jun-2014)

Ref Expression
Hypotheses cnmpopc.r 𝑅 = ( topGen ‘ ran (,) )
cnmpopc.m 𝑀 = ( 𝑅t ( 𝐴 [,] 𝐵 ) )
cnmpopc.n 𝑁 = ( 𝑅t ( 𝐵 [,] 𝐶 ) )
cnmpopc.o 𝑂 = ( 𝑅t ( 𝐴 [,] 𝐶 ) )
cnmpopc.a ( 𝜑𝐴 ∈ ℝ )
cnmpopc.c ( 𝜑𝐶 ∈ ℝ )
cnmpopc.b ( 𝜑𝐵 ∈ ( 𝐴 [,] 𝐶 ) )
cnmpopc.j ( 𝜑𝐽 ∈ ( TopOn ‘ 𝑋 ) )
cnmpopc.q ( ( 𝜑 ∧ ( 𝑥 = 𝐵𝑦𝑋 ) ) → 𝐷 = 𝐸 )
cnmpopc.d ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , 𝑦𝑋𝐷 ) ∈ ( ( 𝑀 ×t 𝐽 ) Cn 𝐾 ) )
cnmpopc.e ( 𝜑 → ( 𝑥 ∈ ( 𝐵 [,] 𝐶 ) , 𝑦𝑋𝐸 ) ∈ ( ( 𝑁 ×t 𝐽 ) Cn 𝐾 ) )
Assertion cnmpopc ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐶 ) , 𝑦𝑋 ↦ if ( 𝑥𝐵 , 𝐷 , 𝐸 ) ) ∈ ( ( 𝑂 ×t 𝐽 ) Cn 𝐾 ) )

Proof

Step Hyp Ref Expression
1 cnmpopc.r 𝑅 = ( topGen ‘ ran (,) )
2 cnmpopc.m 𝑀 = ( 𝑅t ( 𝐴 [,] 𝐵 ) )
3 cnmpopc.n 𝑁 = ( 𝑅t ( 𝐵 [,] 𝐶 ) )
4 cnmpopc.o 𝑂 = ( 𝑅t ( 𝐴 [,] 𝐶 ) )
5 cnmpopc.a ( 𝜑𝐴 ∈ ℝ )
6 cnmpopc.c ( 𝜑𝐶 ∈ ℝ )
7 cnmpopc.b ( 𝜑𝐵 ∈ ( 𝐴 [,] 𝐶 ) )
8 cnmpopc.j ( 𝜑𝐽 ∈ ( TopOn ‘ 𝑋 ) )
9 cnmpopc.q ( ( 𝜑 ∧ ( 𝑥 = 𝐵𝑦𝑋 ) ) → 𝐷 = 𝐸 )
10 cnmpopc.d ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , 𝑦𝑋𝐷 ) ∈ ( ( 𝑀 ×t 𝐽 ) Cn 𝐾 ) )
11 cnmpopc.e ( 𝜑 → ( 𝑥 ∈ ( 𝐵 [,] 𝐶 ) , 𝑦𝑋𝐸 ) ∈ ( ( 𝑁 ×t 𝐽 ) Cn 𝐾 ) )
12 eqid ( 𝑂 ×t 𝐽 ) = ( 𝑂 ×t 𝐽 )
13 eqid 𝐾 = 𝐾
14 iccssre ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 [,] 𝐶 ) ⊆ ℝ )
15 5 6 14 syl2anc ( 𝜑 → ( 𝐴 [,] 𝐶 ) ⊆ ℝ )
16 15 7 sseldd ( 𝜑𝐵 ∈ ℝ )
17 icccld ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) )
18 5 16 17 syl2anc ( 𝜑 → ( 𝐴 [,] 𝐵 ) ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) )
19 1 fveq2i ( Clsd ‘ 𝑅 ) = ( Clsd ‘ ( topGen ‘ ran (,) ) )
20 18 19 eleqtrrdi ( 𝜑 → ( 𝐴 [,] 𝐵 ) ∈ ( Clsd ‘ 𝑅 ) )
21 ssun1 ( 𝐴 [,] 𝐵 ) ⊆ ( ( 𝐴 [,] 𝐵 ) ∪ ( 𝐵 [,] 𝐶 ) )
22 iccsplit ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ 𝐵 ∈ ( 𝐴 [,] 𝐶 ) ) → ( 𝐴 [,] 𝐶 ) = ( ( 𝐴 [,] 𝐵 ) ∪ ( 𝐵 [,] 𝐶 ) ) )
23 5 6 7 22 syl3anc ( 𝜑 → ( 𝐴 [,] 𝐶 ) = ( ( 𝐴 [,] 𝐵 ) ∪ ( 𝐵 [,] 𝐶 ) ) )
24 21 23 sseqtrrid ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ( 𝐴 [,] 𝐶 ) )
25 uniretop ℝ = ( topGen ‘ ran (,) )
26 1 unieqi 𝑅 = ( topGen ‘ ran (,) )
27 25 26 eqtr4i ℝ = 𝑅
28 27 restcldi ( ( ( 𝐴 [,] 𝐶 ) ⊆ ℝ ∧ ( 𝐴 [,] 𝐵 ) ∈ ( Clsd ‘ 𝑅 ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ( 𝐴 [,] 𝐶 ) ) → ( 𝐴 [,] 𝐵 ) ∈ ( Clsd ‘ ( 𝑅t ( 𝐴 [,] 𝐶 ) ) ) )
29 15 20 24 28 syl3anc ( 𝜑 → ( 𝐴 [,] 𝐵 ) ∈ ( Clsd ‘ ( 𝑅t ( 𝐴 [,] 𝐶 ) ) ) )
30 4 fveq2i ( Clsd ‘ 𝑂 ) = ( Clsd ‘ ( 𝑅t ( 𝐴 [,] 𝐶 ) ) )
31 29 30 eleqtrrdi ( 𝜑 → ( 𝐴 [,] 𝐵 ) ∈ ( Clsd ‘ 𝑂 ) )
32 toponuni ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = 𝐽 )
33 8 32 syl ( 𝜑𝑋 = 𝐽 )
34 topontop ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
35 eqid 𝐽 = 𝐽
36 35 topcld ( 𝐽 ∈ Top → 𝐽 ∈ ( Clsd ‘ 𝐽 ) )
37 8 34 36 3syl ( 𝜑 𝐽 ∈ ( Clsd ‘ 𝐽 ) )
38 33 37 eqeltrd ( 𝜑𝑋 ∈ ( Clsd ‘ 𝐽 ) )
39 txcld ( ( ( 𝐴 [,] 𝐵 ) ∈ ( Clsd ‘ 𝑂 ) ∧ 𝑋 ∈ ( Clsd ‘ 𝐽 ) ) → ( ( 𝐴 [,] 𝐵 ) × 𝑋 ) ∈ ( Clsd ‘ ( 𝑂 ×t 𝐽 ) ) )
40 31 38 39 syl2anc ( 𝜑 → ( ( 𝐴 [,] 𝐵 ) × 𝑋 ) ∈ ( Clsd ‘ ( 𝑂 ×t 𝐽 ) ) )
41 icccld ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 [,] 𝐶 ) ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) )
42 16 6 41 syl2anc ( 𝜑 → ( 𝐵 [,] 𝐶 ) ∈ ( Clsd ‘ ( topGen ‘ ran (,) ) ) )
43 42 19 eleqtrrdi ( 𝜑 → ( 𝐵 [,] 𝐶 ) ∈ ( Clsd ‘ 𝑅 ) )
44 ssun2 ( 𝐵 [,] 𝐶 ) ⊆ ( ( 𝐴 [,] 𝐵 ) ∪ ( 𝐵 [,] 𝐶 ) )
45 44 23 sseqtrrid ( 𝜑 → ( 𝐵 [,] 𝐶 ) ⊆ ( 𝐴 [,] 𝐶 ) )
46 27 restcldi ( ( ( 𝐴 [,] 𝐶 ) ⊆ ℝ ∧ ( 𝐵 [,] 𝐶 ) ∈ ( Clsd ‘ 𝑅 ) ∧ ( 𝐵 [,] 𝐶 ) ⊆ ( 𝐴 [,] 𝐶 ) ) → ( 𝐵 [,] 𝐶 ) ∈ ( Clsd ‘ ( 𝑅t ( 𝐴 [,] 𝐶 ) ) ) )
47 15 43 45 46 syl3anc ( 𝜑 → ( 𝐵 [,] 𝐶 ) ∈ ( Clsd ‘ ( 𝑅t ( 𝐴 [,] 𝐶 ) ) ) )
48 47 30 eleqtrrdi ( 𝜑 → ( 𝐵 [,] 𝐶 ) ∈ ( Clsd ‘ 𝑂 ) )
49 txcld ( ( ( 𝐵 [,] 𝐶 ) ∈ ( Clsd ‘ 𝑂 ) ∧ 𝑋 ∈ ( Clsd ‘ 𝐽 ) ) → ( ( 𝐵 [,] 𝐶 ) × 𝑋 ) ∈ ( Clsd ‘ ( 𝑂 ×t 𝐽 ) ) )
50 48 38 49 syl2anc ( 𝜑 → ( ( 𝐵 [,] 𝐶 ) × 𝑋 ) ∈ ( Clsd ‘ ( 𝑂 ×t 𝐽 ) ) )
51 23 xpeq1d ( 𝜑 → ( ( 𝐴 [,] 𝐶 ) × 𝑋 ) = ( ( ( 𝐴 [,] 𝐵 ) ∪ ( 𝐵 [,] 𝐶 ) ) × 𝑋 ) )
52 xpundir ( ( ( 𝐴 [,] 𝐵 ) ∪ ( 𝐵 [,] 𝐶 ) ) × 𝑋 ) = ( ( ( 𝐴 [,] 𝐵 ) × 𝑋 ) ∪ ( ( 𝐵 [,] 𝐶 ) × 𝑋 ) )
53 51 52 eqtrdi ( 𝜑 → ( ( 𝐴 [,] 𝐶 ) × 𝑋 ) = ( ( ( 𝐴 [,] 𝐵 ) × 𝑋 ) ∪ ( ( 𝐵 [,] 𝐶 ) × 𝑋 ) ) )
54 retopon ( topGen ‘ ran (,) ) ∈ ( TopOn ‘ ℝ )
55 1 54 eqeltri 𝑅 ∈ ( TopOn ‘ ℝ )
56 resttopon ( ( 𝑅 ∈ ( TopOn ‘ ℝ ) ∧ ( 𝐴 [,] 𝐶 ) ⊆ ℝ ) → ( 𝑅t ( 𝐴 [,] 𝐶 ) ) ∈ ( TopOn ‘ ( 𝐴 [,] 𝐶 ) ) )
57 55 15 56 sylancr ( 𝜑 → ( 𝑅t ( 𝐴 [,] 𝐶 ) ) ∈ ( TopOn ‘ ( 𝐴 [,] 𝐶 ) ) )
58 4 57 eqeltrid ( 𝜑𝑂 ∈ ( TopOn ‘ ( 𝐴 [,] 𝐶 ) ) )
59 txtopon ( ( 𝑂 ∈ ( TopOn ‘ ( 𝐴 [,] 𝐶 ) ) ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) → ( 𝑂 ×t 𝐽 ) ∈ ( TopOn ‘ ( ( 𝐴 [,] 𝐶 ) × 𝑋 ) ) )
60 58 8 59 syl2anc ( 𝜑 → ( 𝑂 ×t 𝐽 ) ∈ ( TopOn ‘ ( ( 𝐴 [,] 𝐶 ) × 𝑋 ) ) )
61 toponuni ( ( 𝑂 ×t 𝐽 ) ∈ ( TopOn ‘ ( ( 𝐴 [,] 𝐶 ) × 𝑋 ) ) → ( ( 𝐴 [,] 𝐶 ) × 𝑋 ) = ( 𝑂 ×t 𝐽 ) )
62 60 61 syl ( 𝜑 → ( ( 𝐴 [,] 𝐶 ) × 𝑋 ) = ( 𝑂 ×t 𝐽 ) )
63 53 62 eqtr3d ( 𝜑 → ( ( ( 𝐴 [,] 𝐵 ) × 𝑋 ) ∪ ( ( 𝐵 [,] 𝐶 ) × 𝑋 ) ) = ( 𝑂 ×t 𝐽 ) )
64 24 15 sstrd ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
65 resttopon ( ( 𝑅 ∈ ( TopOn ‘ ℝ ) ∧ ( 𝐴 [,] 𝐵 ) ⊆ ℝ ) → ( 𝑅t ( 𝐴 [,] 𝐵 ) ) ∈ ( TopOn ‘ ( 𝐴 [,] 𝐵 ) ) )
66 55 64 65 sylancr ( 𝜑 → ( 𝑅t ( 𝐴 [,] 𝐵 ) ) ∈ ( TopOn ‘ ( 𝐴 [,] 𝐵 ) ) )
67 2 66 eqeltrid ( 𝜑𝑀 ∈ ( TopOn ‘ ( 𝐴 [,] 𝐵 ) ) )
68 txtopon ( ( 𝑀 ∈ ( TopOn ‘ ( 𝐴 [,] 𝐵 ) ) ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) → ( 𝑀 ×t 𝐽 ) ∈ ( TopOn ‘ ( ( 𝐴 [,] 𝐵 ) × 𝑋 ) ) )
69 67 8 68 syl2anc ( 𝜑 → ( 𝑀 ×t 𝐽 ) ∈ ( TopOn ‘ ( ( 𝐴 [,] 𝐵 ) × 𝑋 ) ) )
70 cntop2 ( ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , 𝑦𝑋𝐷 ) ∈ ( ( 𝑀 ×t 𝐽 ) Cn 𝐾 ) → 𝐾 ∈ Top )
71 10 70 syl ( 𝜑𝐾 ∈ Top )
72 toptopon2 ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ 𝐾 ) )
73 71 72 sylib ( 𝜑𝐾 ∈ ( TopOn ‘ 𝐾 ) )
74 elicc2 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐵 ) ) )
75 5 16 74 syl2anc ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐵 ) ) )
76 75 biimpa ( ( 𝜑𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑥 ∈ ℝ ∧ 𝐴𝑥𝑥𝐵 ) )
77 76 simp3d ( ( 𝜑𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑥𝐵 )
78 77 3adant3 ( ( 𝜑𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦𝑋 ) → 𝑥𝐵 )
79 78 iftrued ( ( 𝜑𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦𝑋 ) → if ( 𝑥𝐵 , 𝐷 , 𝐸 ) = 𝐷 )
80 79 mpoeq3dva ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , 𝑦𝑋 ↦ if ( 𝑥𝐵 , 𝐷 , 𝐸 ) ) = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , 𝑦𝑋𝐷 ) )
81 80 10 eqeltrd ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , 𝑦𝑋 ↦ if ( 𝑥𝐵 , 𝐷 , 𝐸 ) ) ∈ ( ( 𝑀 ×t 𝐽 ) Cn 𝐾 ) )
82 cnf2 ( ( ( 𝑀 ×t 𝐽 ) ∈ ( TopOn ‘ ( ( 𝐴 [,] 𝐵 ) × 𝑋 ) ) ∧ 𝐾 ∈ ( TopOn ‘ 𝐾 ) ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , 𝑦𝑋 ↦ if ( 𝑥𝐵 , 𝐷 , 𝐸 ) ) ∈ ( ( 𝑀 ×t 𝐽 ) Cn 𝐾 ) ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , 𝑦𝑋 ↦ if ( 𝑥𝐵 , 𝐷 , 𝐸 ) ) : ( ( 𝐴 [,] 𝐵 ) × 𝑋 ) ⟶ 𝐾 )
83 69 73 81 82 syl3anc ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , 𝑦𝑋 ↦ if ( 𝑥𝐵 , 𝐷 , 𝐸 ) ) : ( ( 𝐴 [,] 𝐵 ) × 𝑋 ) ⟶ 𝐾 )
84 eqid ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , 𝑦𝑋 ↦ if ( 𝑥𝐵 , 𝐷 , 𝐸 ) ) = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , 𝑦𝑋 ↦ if ( 𝑥𝐵 , 𝐷 , 𝐸 ) )
85 84 fmpo ( ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦𝑋 if ( 𝑥𝐵 , 𝐷 , 𝐸 ) ∈ 𝐾 ↔ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , 𝑦𝑋 ↦ if ( 𝑥𝐵 , 𝐷 , 𝐸 ) ) : ( ( 𝐴 [,] 𝐵 ) × 𝑋 ) ⟶ 𝐾 )
86 83 85 sylibr ( 𝜑 → ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦𝑋 if ( 𝑥𝐵 , 𝐷 , 𝐸 ) ∈ 𝐾 )
87 45 15 sstrd ( 𝜑 → ( 𝐵 [,] 𝐶 ) ⊆ ℝ )
88 resttopon ( ( 𝑅 ∈ ( TopOn ‘ ℝ ) ∧ ( 𝐵 [,] 𝐶 ) ⊆ ℝ ) → ( 𝑅t ( 𝐵 [,] 𝐶 ) ) ∈ ( TopOn ‘ ( 𝐵 [,] 𝐶 ) ) )
89 55 87 88 sylancr ( 𝜑 → ( 𝑅t ( 𝐵 [,] 𝐶 ) ) ∈ ( TopOn ‘ ( 𝐵 [,] 𝐶 ) ) )
90 3 89 eqeltrid ( 𝜑𝑁 ∈ ( TopOn ‘ ( 𝐵 [,] 𝐶 ) ) )
91 txtopon ( ( 𝑁 ∈ ( TopOn ‘ ( 𝐵 [,] 𝐶 ) ) ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) → ( 𝑁 ×t 𝐽 ) ∈ ( TopOn ‘ ( ( 𝐵 [,] 𝐶 ) × 𝑋 ) ) )
92 90 8 91 syl2anc ( 𝜑 → ( 𝑁 ×t 𝐽 ) ∈ ( TopOn ‘ ( ( 𝐵 [,] 𝐶 ) × 𝑋 ) ) )
93 elicc2 ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝑥 ∈ ( 𝐵 [,] 𝐶 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐵𝑥𝑥𝐶 ) ) )
94 16 6 93 syl2anc ( 𝜑 → ( 𝑥 ∈ ( 𝐵 [,] 𝐶 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝐵𝑥𝑥𝐶 ) ) )
95 94 biimpa ( ( 𝜑𝑥 ∈ ( 𝐵 [,] 𝐶 ) ) → ( 𝑥 ∈ ℝ ∧ 𝐵𝑥𝑥𝐶 ) )
96 95 simp2d ( ( 𝜑𝑥 ∈ ( 𝐵 [,] 𝐶 ) ) → 𝐵𝑥 )
97 96 biantrud ( ( 𝜑𝑥 ∈ ( 𝐵 [,] 𝐶 ) ) → ( 𝑥𝐵 ↔ ( 𝑥𝐵𝐵𝑥 ) ) )
98 95 simp1d ( ( 𝜑𝑥 ∈ ( 𝐵 [,] 𝐶 ) ) → 𝑥 ∈ ℝ )
99 16 adantr ( ( 𝜑𝑥 ∈ ( 𝐵 [,] 𝐶 ) ) → 𝐵 ∈ ℝ )
100 98 99 letri3d ( ( 𝜑𝑥 ∈ ( 𝐵 [,] 𝐶 ) ) → ( 𝑥 = 𝐵 ↔ ( 𝑥𝐵𝐵𝑥 ) ) )
101 97 100 bitr4d ( ( 𝜑𝑥 ∈ ( 𝐵 [,] 𝐶 ) ) → ( 𝑥𝐵𝑥 = 𝐵 ) )
102 101 3adant3 ( ( 𝜑𝑥 ∈ ( 𝐵 [,] 𝐶 ) ∧ 𝑦𝑋 ) → ( 𝑥𝐵𝑥 = 𝐵 ) )
103 9 ancom2s ( ( 𝜑 ∧ ( 𝑦𝑋𝑥 = 𝐵 ) ) → 𝐷 = 𝐸 )
104 103 ifeq1d ( ( 𝜑 ∧ ( 𝑦𝑋𝑥 = 𝐵 ) ) → if ( 𝑥𝐵 , 𝐷 , 𝐸 ) = if ( 𝑥𝐵 , 𝐸 , 𝐸 ) )
105 ifid if ( 𝑥𝐵 , 𝐸 , 𝐸 ) = 𝐸
106 104 105 eqtrdi ( ( 𝜑 ∧ ( 𝑦𝑋𝑥 = 𝐵 ) ) → if ( 𝑥𝐵 , 𝐷 , 𝐸 ) = 𝐸 )
107 106 expr ( ( 𝜑𝑦𝑋 ) → ( 𝑥 = 𝐵 → if ( 𝑥𝐵 , 𝐷 , 𝐸 ) = 𝐸 ) )
108 107 3adant2 ( ( 𝜑𝑥 ∈ ( 𝐵 [,] 𝐶 ) ∧ 𝑦𝑋 ) → ( 𝑥 = 𝐵 → if ( 𝑥𝐵 , 𝐷 , 𝐸 ) = 𝐸 ) )
109 102 108 sylbid ( ( 𝜑𝑥 ∈ ( 𝐵 [,] 𝐶 ) ∧ 𝑦𝑋 ) → ( 𝑥𝐵 → if ( 𝑥𝐵 , 𝐷 , 𝐸 ) = 𝐸 ) )
110 iffalse ( ¬ 𝑥𝐵 → if ( 𝑥𝐵 , 𝐷 , 𝐸 ) = 𝐸 )
111 109 110 pm2.61d1 ( ( 𝜑𝑥 ∈ ( 𝐵 [,] 𝐶 ) ∧ 𝑦𝑋 ) → if ( 𝑥𝐵 , 𝐷 , 𝐸 ) = 𝐸 )
112 111 mpoeq3dva ( 𝜑 → ( 𝑥 ∈ ( 𝐵 [,] 𝐶 ) , 𝑦𝑋 ↦ if ( 𝑥𝐵 , 𝐷 , 𝐸 ) ) = ( 𝑥 ∈ ( 𝐵 [,] 𝐶 ) , 𝑦𝑋𝐸 ) )
113 112 11 eqeltrd ( 𝜑 → ( 𝑥 ∈ ( 𝐵 [,] 𝐶 ) , 𝑦𝑋 ↦ if ( 𝑥𝐵 , 𝐷 , 𝐸 ) ) ∈ ( ( 𝑁 ×t 𝐽 ) Cn 𝐾 ) )
114 cnf2 ( ( ( 𝑁 ×t 𝐽 ) ∈ ( TopOn ‘ ( ( 𝐵 [,] 𝐶 ) × 𝑋 ) ) ∧ 𝐾 ∈ ( TopOn ‘ 𝐾 ) ∧ ( 𝑥 ∈ ( 𝐵 [,] 𝐶 ) , 𝑦𝑋 ↦ if ( 𝑥𝐵 , 𝐷 , 𝐸 ) ) ∈ ( ( 𝑁 ×t 𝐽 ) Cn 𝐾 ) ) → ( 𝑥 ∈ ( 𝐵 [,] 𝐶 ) , 𝑦𝑋 ↦ if ( 𝑥𝐵 , 𝐷 , 𝐸 ) ) : ( ( 𝐵 [,] 𝐶 ) × 𝑋 ) ⟶ 𝐾 )
115 92 73 113 114 syl3anc ( 𝜑 → ( 𝑥 ∈ ( 𝐵 [,] 𝐶 ) , 𝑦𝑋 ↦ if ( 𝑥𝐵 , 𝐷 , 𝐸 ) ) : ( ( 𝐵 [,] 𝐶 ) × 𝑋 ) ⟶ 𝐾 )
116 eqid ( 𝑥 ∈ ( 𝐵 [,] 𝐶 ) , 𝑦𝑋 ↦ if ( 𝑥𝐵 , 𝐷 , 𝐸 ) ) = ( 𝑥 ∈ ( 𝐵 [,] 𝐶 ) , 𝑦𝑋 ↦ if ( 𝑥𝐵 , 𝐷 , 𝐸 ) )
117 116 fmpo ( ∀ 𝑥 ∈ ( 𝐵 [,] 𝐶 ) ∀ 𝑦𝑋 if ( 𝑥𝐵 , 𝐷 , 𝐸 ) ∈ 𝐾 ↔ ( 𝑥 ∈ ( 𝐵 [,] 𝐶 ) , 𝑦𝑋 ↦ if ( 𝑥𝐵 , 𝐷 , 𝐸 ) ) : ( ( 𝐵 [,] 𝐶 ) × 𝑋 ) ⟶ 𝐾 )
118 115 117 sylibr ( 𝜑 → ∀ 𝑥 ∈ ( 𝐵 [,] 𝐶 ) ∀ 𝑦𝑋 if ( 𝑥𝐵 , 𝐷 , 𝐸 ) ∈ 𝐾 )
119 ralun ( ( ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑦𝑋 if ( 𝑥𝐵 , 𝐷 , 𝐸 ) ∈ 𝐾 ∧ ∀ 𝑥 ∈ ( 𝐵 [,] 𝐶 ) ∀ 𝑦𝑋 if ( 𝑥𝐵 , 𝐷 , 𝐸 ) ∈ 𝐾 ) → ∀ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∪ ( 𝐵 [,] 𝐶 ) ) ∀ 𝑦𝑋 if ( 𝑥𝐵 , 𝐷 , 𝐸 ) ∈ 𝐾 )
120 86 118 119 syl2anc ( 𝜑 → ∀ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∪ ( 𝐵 [,] 𝐶 ) ) ∀ 𝑦𝑋 if ( 𝑥𝐵 , 𝐷 , 𝐸 ) ∈ 𝐾 )
121 23 raleqdv ( 𝜑 → ( ∀ 𝑥 ∈ ( 𝐴 [,] 𝐶 ) ∀ 𝑦𝑋 if ( 𝑥𝐵 , 𝐷 , 𝐸 ) ∈ 𝐾 ↔ ∀ 𝑥 ∈ ( ( 𝐴 [,] 𝐵 ) ∪ ( 𝐵 [,] 𝐶 ) ) ∀ 𝑦𝑋 if ( 𝑥𝐵 , 𝐷 , 𝐸 ) ∈ 𝐾 ) )
122 120 121 mpbird ( 𝜑 → ∀ 𝑥 ∈ ( 𝐴 [,] 𝐶 ) ∀ 𝑦𝑋 if ( 𝑥𝐵 , 𝐷 , 𝐸 ) ∈ 𝐾 )
123 eqid ( 𝑥 ∈ ( 𝐴 [,] 𝐶 ) , 𝑦𝑋 ↦ if ( 𝑥𝐵 , 𝐷 , 𝐸 ) ) = ( 𝑥 ∈ ( 𝐴 [,] 𝐶 ) , 𝑦𝑋 ↦ if ( 𝑥𝐵 , 𝐷 , 𝐸 ) )
124 123 fmpo ( ∀ 𝑥 ∈ ( 𝐴 [,] 𝐶 ) ∀ 𝑦𝑋 if ( 𝑥𝐵 , 𝐷 , 𝐸 ) ∈ 𝐾 ↔ ( 𝑥 ∈ ( 𝐴 [,] 𝐶 ) , 𝑦𝑋 ↦ if ( 𝑥𝐵 , 𝐷 , 𝐸 ) ) : ( ( 𝐴 [,] 𝐶 ) × 𝑋 ) ⟶ 𝐾 )
125 122 124 sylib ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐶 ) , 𝑦𝑋 ↦ if ( 𝑥𝐵 , 𝐷 , 𝐸 ) ) : ( ( 𝐴 [,] 𝐶 ) × 𝑋 ) ⟶ 𝐾 )
126 62 feq2d ( 𝜑 → ( ( 𝑥 ∈ ( 𝐴 [,] 𝐶 ) , 𝑦𝑋 ↦ if ( 𝑥𝐵 , 𝐷 , 𝐸 ) ) : ( ( 𝐴 [,] 𝐶 ) × 𝑋 ) ⟶ 𝐾 ↔ ( 𝑥 ∈ ( 𝐴 [,] 𝐶 ) , 𝑦𝑋 ↦ if ( 𝑥𝐵 , 𝐷 , 𝐸 ) ) : ( 𝑂 ×t 𝐽 ) ⟶ 𝐾 ) )
127 125 126 mpbid ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐶 ) , 𝑦𝑋 ↦ if ( 𝑥𝐵 , 𝐷 , 𝐸 ) ) : ( 𝑂 ×t 𝐽 ) ⟶ 𝐾 )
128 ssid 𝑋𝑋
129 resmpo ( ( ( 𝐴 [,] 𝐵 ) ⊆ ( 𝐴 [,] 𝐶 ) ∧ 𝑋𝑋 ) → ( ( 𝑥 ∈ ( 𝐴 [,] 𝐶 ) , 𝑦𝑋 ↦ if ( 𝑥𝐵 , 𝐷 , 𝐸 ) ) ↾ ( ( 𝐴 [,] 𝐵 ) × 𝑋 ) ) = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , 𝑦𝑋 ↦ if ( 𝑥𝐵 , 𝐷 , 𝐸 ) ) )
130 24 128 129 sylancl ( 𝜑 → ( ( 𝑥 ∈ ( 𝐴 [,] 𝐶 ) , 𝑦𝑋 ↦ if ( 𝑥𝐵 , 𝐷 , 𝐸 ) ) ↾ ( ( 𝐴 [,] 𝐵 ) × 𝑋 ) ) = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , 𝑦𝑋 ↦ if ( 𝑥𝐵 , 𝐷 , 𝐸 ) ) )
131 retop ( topGen ‘ ran (,) ) ∈ Top
132 1 131 eqeltri 𝑅 ∈ Top
133 ovex ( 𝐴 [,] 𝐶 ) ∈ V
134 resttop ( ( 𝑅 ∈ Top ∧ ( 𝐴 [,] 𝐶 ) ∈ V ) → ( 𝑅t ( 𝐴 [,] 𝐶 ) ) ∈ Top )
135 132 133 134 mp2an ( 𝑅t ( 𝐴 [,] 𝐶 ) ) ∈ Top
136 4 135 eqeltri 𝑂 ∈ Top
137 136 a1i ( 𝜑𝑂 ∈ Top )
138 ovexd ( 𝜑 → ( 𝐴 [,] 𝐵 ) ∈ V )
139 txrest ( ( ( 𝑂 ∈ Top ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ( ( 𝐴 [,] 𝐵 ) ∈ V ∧ 𝑋 ∈ ( Clsd ‘ 𝐽 ) ) ) → ( ( 𝑂 ×t 𝐽 ) ↾t ( ( 𝐴 [,] 𝐵 ) × 𝑋 ) ) = ( ( 𝑂t ( 𝐴 [,] 𝐵 ) ) ×t ( 𝐽t 𝑋 ) ) )
140 137 8 138 38 139 syl22anc ( 𝜑 → ( ( 𝑂 ×t 𝐽 ) ↾t ( ( 𝐴 [,] 𝐵 ) × 𝑋 ) ) = ( ( 𝑂t ( 𝐴 [,] 𝐵 ) ) ×t ( 𝐽t 𝑋 ) ) )
141 132 a1i ( 𝜑𝑅 ∈ Top )
142 ovexd ( 𝜑 → ( 𝐴 [,] 𝐶 ) ∈ V )
143 restabs ( ( 𝑅 ∈ Top ∧ ( 𝐴 [,] 𝐵 ) ⊆ ( 𝐴 [,] 𝐶 ) ∧ ( 𝐴 [,] 𝐶 ) ∈ V ) → ( ( 𝑅t ( 𝐴 [,] 𝐶 ) ) ↾t ( 𝐴 [,] 𝐵 ) ) = ( 𝑅t ( 𝐴 [,] 𝐵 ) ) )
144 141 24 142 143 syl3anc ( 𝜑 → ( ( 𝑅t ( 𝐴 [,] 𝐶 ) ) ↾t ( 𝐴 [,] 𝐵 ) ) = ( 𝑅t ( 𝐴 [,] 𝐵 ) ) )
145 4 oveq1i ( 𝑂t ( 𝐴 [,] 𝐵 ) ) = ( ( 𝑅t ( 𝐴 [,] 𝐶 ) ) ↾t ( 𝐴 [,] 𝐵 ) )
146 144 145 2 3eqtr4g ( 𝜑 → ( 𝑂t ( 𝐴 [,] 𝐵 ) ) = 𝑀 )
147 33 oveq2d ( 𝜑 → ( 𝐽t 𝑋 ) = ( 𝐽t 𝐽 ) )
148 35 restid ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐽t 𝐽 ) = 𝐽 )
149 8 148 syl ( 𝜑 → ( 𝐽t 𝐽 ) = 𝐽 )
150 147 149 eqtrd ( 𝜑 → ( 𝐽t 𝑋 ) = 𝐽 )
151 146 150 oveq12d ( 𝜑 → ( ( 𝑂t ( 𝐴 [,] 𝐵 ) ) ×t ( 𝐽t 𝑋 ) ) = ( 𝑀 ×t 𝐽 ) )
152 140 151 eqtrd ( 𝜑 → ( ( 𝑂 ×t 𝐽 ) ↾t ( ( 𝐴 [,] 𝐵 ) × 𝑋 ) ) = ( 𝑀 ×t 𝐽 ) )
153 152 oveq1d ( 𝜑 → ( ( ( 𝑂 ×t 𝐽 ) ↾t ( ( 𝐴 [,] 𝐵 ) × 𝑋 ) ) Cn 𝐾 ) = ( ( 𝑀 ×t 𝐽 ) Cn 𝐾 ) )
154 81 130 153 3eltr4d ( 𝜑 → ( ( 𝑥 ∈ ( 𝐴 [,] 𝐶 ) , 𝑦𝑋 ↦ if ( 𝑥𝐵 , 𝐷 , 𝐸 ) ) ↾ ( ( 𝐴 [,] 𝐵 ) × 𝑋 ) ) ∈ ( ( ( 𝑂 ×t 𝐽 ) ↾t ( ( 𝐴 [,] 𝐵 ) × 𝑋 ) ) Cn 𝐾 ) )
155 resmpo ( ( ( 𝐵 [,] 𝐶 ) ⊆ ( 𝐴 [,] 𝐶 ) ∧ 𝑋𝑋 ) → ( ( 𝑥 ∈ ( 𝐴 [,] 𝐶 ) , 𝑦𝑋 ↦ if ( 𝑥𝐵 , 𝐷 , 𝐸 ) ) ↾ ( ( 𝐵 [,] 𝐶 ) × 𝑋 ) ) = ( 𝑥 ∈ ( 𝐵 [,] 𝐶 ) , 𝑦𝑋 ↦ if ( 𝑥𝐵 , 𝐷 , 𝐸 ) ) )
156 45 128 155 sylancl ( 𝜑 → ( ( 𝑥 ∈ ( 𝐴 [,] 𝐶 ) , 𝑦𝑋 ↦ if ( 𝑥𝐵 , 𝐷 , 𝐸 ) ) ↾ ( ( 𝐵 [,] 𝐶 ) × 𝑋 ) ) = ( 𝑥 ∈ ( 𝐵 [,] 𝐶 ) , 𝑦𝑋 ↦ if ( 𝑥𝐵 , 𝐷 , 𝐸 ) ) )
157 ovexd ( 𝜑 → ( 𝐵 [,] 𝐶 ) ∈ V )
158 txrest ( ( ( 𝑂 ∈ Top ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ( ( 𝐵 [,] 𝐶 ) ∈ V ∧ 𝑋 ∈ ( Clsd ‘ 𝐽 ) ) ) → ( ( 𝑂 ×t 𝐽 ) ↾t ( ( 𝐵 [,] 𝐶 ) × 𝑋 ) ) = ( ( 𝑂t ( 𝐵 [,] 𝐶 ) ) ×t ( 𝐽t 𝑋 ) ) )
159 137 8 157 38 158 syl22anc ( 𝜑 → ( ( 𝑂 ×t 𝐽 ) ↾t ( ( 𝐵 [,] 𝐶 ) × 𝑋 ) ) = ( ( 𝑂t ( 𝐵 [,] 𝐶 ) ) ×t ( 𝐽t 𝑋 ) ) )
160 restabs ( ( 𝑅 ∈ Top ∧ ( 𝐵 [,] 𝐶 ) ⊆ ( 𝐴 [,] 𝐶 ) ∧ ( 𝐴 [,] 𝐶 ) ∈ V ) → ( ( 𝑅t ( 𝐴 [,] 𝐶 ) ) ↾t ( 𝐵 [,] 𝐶 ) ) = ( 𝑅t ( 𝐵 [,] 𝐶 ) ) )
161 141 45 142 160 syl3anc ( 𝜑 → ( ( 𝑅t ( 𝐴 [,] 𝐶 ) ) ↾t ( 𝐵 [,] 𝐶 ) ) = ( 𝑅t ( 𝐵 [,] 𝐶 ) ) )
162 4 oveq1i ( 𝑂t ( 𝐵 [,] 𝐶 ) ) = ( ( 𝑅t ( 𝐴 [,] 𝐶 ) ) ↾t ( 𝐵 [,] 𝐶 ) )
163 161 162 3 3eqtr4g ( 𝜑 → ( 𝑂t ( 𝐵 [,] 𝐶 ) ) = 𝑁 )
164 163 150 oveq12d ( 𝜑 → ( ( 𝑂t ( 𝐵 [,] 𝐶 ) ) ×t ( 𝐽t 𝑋 ) ) = ( 𝑁 ×t 𝐽 ) )
165 159 164 eqtrd ( 𝜑 → ( ( 𝑂 ×t 𝐽 ) ↾t ( ( 𝐵 [,] 𝐶 ) × 𝑋 ) ) = ( 𝑁 ×t 𝐽 ) )
166 165 oveq1d ( 𝜑 → ( ( ( 𝑂 ×t 𝐽 ) ↾t ( ( 𝐵 [,] 𝐶 ) × 𝑋 ) ) Cn 𝐾 ) = ( ( 𝑁 ×t 𝐽 ) Cn 𝐾 ) )
167 113 156 166 3eltr4d ( 𝜑 → ( ( 𝑥 ∈ ( 𝐴 [,] 𝐶 ) , 𝑦𝑋 ↦ if ( 𝑥𝐵 , 𝐷 , 𝐸 ) ) ↾ ( ( 𝐵 [,] 𝐶 ) × 𝑋 ) ) ∈ ( ( ( 𝑂 ×t 𝐽 ) ↾t ( ( 𝐵 [,] 𝐶 ) × 𝑋 ) ) Cn 𝐾 ) )
168 12 13 40 50 63 127 154 167 paste ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐶 ) , 𝑦𝑋 ↦ if ( 𝑥𝐵 , 𝐷 , 𝐸 ) ) ∈ ( ( 𝑂 ×t 𝐽 ) Cn 𝐾 ) )