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 120 23 raleqtrrdv ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝐴 [,] 𝐶 ) ∀ 𝑦 ∈ 𝑋 if ( 𝑥 ≤ 𝐵 , 𝐷 , 𝐸 ) ∈ ∪ 𝐾 )
122 eqid ⊢ ( 𝑥 ∈ ( 𝐴 [,] 𝐶 ) , 𝑦 ∈ 𝑋 ↦ if ( 𝑥 ≤ 𝐵 , 𝐷 , 𝐸 ) ) = ( 𝑥 ∈ ( 𝐴 [,] 𝐶 ) , 𝑦 ∈ 𝑋 ↦ if ( 𝑥 ≤ 𝐵 , 𝐷 , 𝐸 ) )
123 122 fmpo ⊢ ( ∀ 𝑥 ∈ ( 𝐴 [,] 𝐶 ) ∀ 𝑦 ∈ 𝑋 if ( 𝑥 ≤ 𝐵 , 𝐷 , 𝐸 ) ∈ ∪ 𝐾 ↔ ( 𝑥 ∈ ( 𝐴 [,] 𝐶 ) , 𝑦 ∈ 𝑋 ↦ if ( 𝑥 ≤ 𝐵 , 𝐷 , 𝐸 ) ) : ( ( 𝐴 [,] 𝐶 ) × 𝑋 ) ⟶ ∪ 𝐾 )
124 121 123 sylib ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐶 ) , 𝑦 ∈ 𝑋 ↦ if ( 𝑥 ≤ 𝐵 , 𝐷 , 𝐸 ) ) : ( ( 𝐴 [,] 𝐶 ) × 𝑋 ) ⟶ ∪ 𝐾 )
125 62 feq2d ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝐴 [,] 𝐶 ) , 𝑦 ∈ 𝑋 ↦ if ( 𝑥 ≤ 𝐵 , 𝐷 , 𝐸 ) ) : ( ( 𝐴 [,] 𝐶 ) × 𝑋 ) ⟶ ∪ 𝐾 ↔ ( 𝑥 ∈ ( 𝐴 [,] 𝐶 ) , 𝑦 ∈ 𝑋 ↦ if ( 𝑥 ≤ 𝐵 , 𝐷 , 𝐸 ) ) : ∪ ( 𝑂 ×t 𝐽 ) ⟶ ∪ 𝐾 ) )
126 124 125 mpbid ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐶 ) , 𝑦 ∈ 𝑋 ↦ if ( 𝑥 ≤ 𝐵 , 𝐷 , 𝐸 ) ) : ∪ ( 𝑂 ×t 𝐽 ) ⟶ ∪ 𝐾 )
127 ssid ⊢ 𝑋 ⊆ 𝑋
128 resmpo ⊢ ( ( ( 𝐴 [,] 𝐵 ) ⊆ ( 𝐴 [,] 𝐶 ) ∧ 𝑋 ⊆ 𝑋 ) → ( ( 𝑥 ∈ ( 𝐴 [,] 𝐶 ) , 𝑦 ∈ 𝑋 ↦ if ( 𝑥 ≤ 𝐵 , 𝐷 , 𝐸 ) ) ↾ ( ( 𝐴 [,] 𝐵 ) × 𝑋 ) ) = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , 𝑦 ∈ 𝑋 ↦ if ( 𝑥 ≤ 𝐵 , 𝐷 , 𝐸 ) ) )
129 24 127 128 sylancl ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝐴 [,] 𝐶 ) , 𝑦 ∈ 𝑋 ↦ if ( 𝑥 ≤ 𝐵 , 𝐷 , 𝐸 ) ) ↾ ( ( 𝐴 [,] 𝐵 ) × 𝑋 ) ) = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , 𝑦 ∈ 𝑋 ↦ if ( 𝑥 ≤ 𝐵 , 𝐷 , 𝐸 ) ) )
130 retop ⊢ ( topGen ‘ ran (,) ) ∈ Top
131 1 130 eqeltri ⊢ 𝑅 ∈ Top
132 ovex ⊢ ( 𝐴 [,] 𝐶 ) ∈ V
133 resttop ⊢ ( ( 𝑅 ∈ Top ∧ ( 𝐴 [,] 𝐶 ) ∈ V ) → ( 𝑅 ↾t ( 𝐴 [,] 𝐶 ) ) ∈ Top )
134 131 132 133 mp2an ⊢ ( 𝑅 ↾t ( 𝐴 [,] 𝐶 ) ) ∈ Top
135 4 134 eqeltri ⊢ 𝑂 ∈ Top
136 135 a1i ⊢ ( 𝜑 → 𝑂 ∈ Top )
137 ovexd ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ∈ V )
138 txrest ⊢ ( ( ( 𝑂 ∈ Top ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ( ( 𝐴 [,] 𝐵 ) ∈ V ∧ 𝑋 ∈ ( Clsd ‘ 𝐽 ) ) ) → ( ( 𝑂 ×t 𝐽 ) ↾t ( ( 𝐴 [,] 𝐵 ) × 𝑋 ) ) = ( ( 𝑂 ↾t ( 𝐴 [,] 𝐵 ) ) ×t ( 𝐽 ↾t 𝑋 ) ) )
139 136 8 137 38 138 syl22anc ⊢ ( 𝜑 → ( ( 𝑂 ×t 𝐽 ) ↾t ( ( 𝐴 [,] 𝐵 ) × 𝑋 ) ) = ( ( 𝑂 ↾t ( 𝐴 [,] 𝐵 ) ) ×t ( 𝐽 ↾t 𝑋 ) ) )
140 131 a1i ⊢ ( 𝜑 → 𝑅 ∈ Top )
141 ovexd ⊢ ( 𝜑 → ( 𝐴 [,] 𝐶 ) ∈ V )
142 restabs ⊢ ( ( 𝑅 ∈ Top ∧ ( 𝐴 [,] 𝐵 ) ⊆ ( 𝐴 [,] 𝐶 ) ∧ ( 𝐴 [,] 𝐶 ) ∈ V ) → ( ( 𝑅 ↾t ( 𝐴 [,] 𝐶 ) ) ↾t ( 𝐴 [,] 𝐵 ) ) = ( 𝑅 ↾t ( 𝐴 [,] 𝐵 ) ) )
143 140 24 141 142 syl3anc ⊢ ( 𝜑 → ( ( 𝑅 ↾t ( 𝐴 [,] 𝐶 ) ) ↾t ( 𝐴 [,] 𝐵 ) ) = ( 𝑅 ↾t ( 𝐴 [,] 𝐵 ) ) )
144 4 oveq1i ⊢ ( 𝑂 ↾t ( 𝐴 [,] 𝐵 ) ) = ( ( 𝑅 ↾t ( 𝐴 [,] 𝐶 ) ) ↾t ( 𝐴 [,] 𝐵 ) )
145 143 144 2 3eqtr4g ⊢ ( 𝜑 → ( 𝑂 ↾t ( 𝐴 [,] 𝐵 ) ) = 𝑀 )
146 33 oveq2d ⊢ ( 𝜑 → ( 𝐽 ↾t 𝑋 ) = ( 𝐽 ↾t ∪ 𝐽 ) )
147 35 restid ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( 𝐽 ↾t ∪ 𝐽 ) = 𝐽 )
148 8 147 syl ⊢ ( 𝜑 → ( 𝐽 ↾t ∪ 𝐽 ) = 𝐽 )
149 146 148 eqtrd ⊢ ( 𝜑 → ( 𝐽 ↾t 𝑋 ) = 𝐽 )
150 145 149 oveq12d ⊢ ( 𝜑 → ( ( 𝑂 ↾t ( 𝐴 [,] 𝐵 ) ) ×t ( 𝐽 ↾t 𝑋 ) ) = ( 𝑀 ×t 𝐽 ) )
151 139 150 eqtrd ⊢ ( 𝜑 → ( ( 𝑂 ×t 𝐽 ) ↾t ( ( 𝐴 [,] 𝐵 ) × 𝑋 ) ) = ( 𝑀 ×t 𝐽 ) )
152 151 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑂 ×t 𝐽 ) ↾t ( ( 𝐴 [,] 𝐵 ) × 𝑋 ) ) Cn 𝐾 ) = ( ( 𝑀 ×t 𝐽 ) Cn 𝐾 ) )
153 81 129 152 3eltr4d ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝐴 [,] 𝐶 ) , 𝑦 ∈ 𝑋 ↦ if ( 𝑥 ≤ 𝐵 , 𝐷 , 𝐸 ) ) ↾ ( ( 𝐴 [,] 𝐵 ) × 𝑋 ) ) ∈ ( ( ( 𝑂 ×t 𝐽 ) ↾t ( ( 𝐴 [,] 𝐵 ) × 𝑋 ) ) Cn 𝐾 ) )
154 resmpo ⊢ ( ( ( 𝐵 [,] 𝐶 ) ⊆ ( 𝐴 [,] 𝐶 ) ∧ 𝑋 ⊆ 𝑋 ) → ( ( 𝑥 ∈ ( 𝐴 [,] 𝐶 ) , 𝑦 ∈ 𝑋 ↦ if ( 𝑥 ≤ 𝐵 , 𝐷 , 𝐸 ) ) ↾ ( ( 𝐵 [,] 𝐶 ) × 𝑋 ) ) = ( 𝑥 ∈ ( 𝐵 [,] 𝐶 ) , 𝑦 ∈ 𝑋 ↦ if ( 𝑥 ≤ 𝐵 , 𝐷 , 𝐸 ) ) )
155 45 127 154 sylancl ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝐴 [,] 𝐶 ) , 𝑦 ∈ 𝑋 ↦ if ( 𝑥 ≤ 𝐵 , 𝐷 , 𝐸 ) ) ↾ ( ( 𝐵 [,] 𝐶 ) × 𝑋 ) ) = ( 𝑥 ∈ ( 𝐵 [,] 𝐶 ) , 𝑦 ∈ 𝑋 ↦ if ( 𝑥 ≤ 𝐵 , 𝐷 , 𝐸 ) ) )
156 ovexd ⊢ ( 𝜑 → ( 𝐵 [,] 𝐶 ) ∈ V )
157 txrest ⊢ ( ( ( 𝑂 ∈ Top ∧ 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ( ( 𝐵 [,] 𝐶 ) ∈ V ∧ 𝑋 ∈ ( Clsd ‘ 𝐽 ) ) ) → ( ( 𝑂 ×t 𝐽 ) ↾t ( ( 𝐵 [,] 𝐶 ) × 𝑋 ) ) = ( ( 𝑂 ↾t ( 𝐵 [,] 𝐶 ) ) ×t ( 𝐽 ↾t 𝑋 ) ) )
158 136 8 156 38 157 syl22anc ⊢ ( 𝜑 → ( ( 𝑂 ×t 𝐽 ) ↾t ( ( 𝐵 [,] 𝐶 ) × 𝑋 ) ) = ( ( 𝑂 ↾t ( 𝐵 [,] 𝐶 ) ) ×t ( 𝐽 ↾t 𝑋 ) ) )
159 restabs ⊢ ( ( 𝑅 ∈ Top ∧ ( 𝐵 [,] 𝐶 ) ⊆ ( 𝐴 [,] 𝐶 ) ∧ ( 𝐴 [,] 𝐶 ) ∈ V ) → ( ( 𝑅 ↾t ( 𝐴 [,] 𝐶 ) ) ↾t ( 𝐵 [,] 𝐶 ) ) = ( 𝑅 ↾t ( 𝐵 [,] 𝐶 ) ) )
160 140 45 141 159 syl3anc ⊢ ( 𝜑 → ( ( 𝑅 ↾t ( 𝐴 [,] 𝐶 ) ) ↾t ( 𝐵 [,] 𝐶 ) ) = ( 𝑅 ↾t ( 𝐵 [,] 𝐶 ) ) )
161 4 oveq1i ⊢ ( 𝑂 ↾t ( 𝐵 [,] 𝐶 ) ) = ( ( 𝑅 ↾t ( 𝐴 [,] 𝐶 ) ) ↾t ( 𝐵 [,] 𝐶 ) )
162 160 161 3 3eqtr4g ⊢ ( 𝜑 → ( 𝑂 ↾t ( 𝐵 [,] 𝐶 ) ) = 𝑁 )
163 162 149 oveq12d ⊢ ( 𝜑 → ( ( 𝑂 ↾t ( 𝐵 [,] 𝐶 ) ) ×t ( 𝐽 ↾t 𝑋 ) ) = ( 𝑁 ×t 𝐽 ) )
164 158 163 eqtrd ⊢ ( 𝜑 → ( ( 𝑂 ×t 𝐽 ) ↾t ( ( 𝐵 [,] 𝐶 ) × 𝑋 ) ) = ( 𝑁 ×t 𝐽 ) )
165 164 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑂 ×t 𝐽 ) ↾t ( ( 𝐵 [,] 𝐶 ) × 𝑋 ) ) Cn 𝐾 ) = ( ( 𝑁 ×t 𝐽 ) Cn 𝐾 ) )
166 113 155 165 3eltr4d ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 𝐴 [,] 𝐶 ) , 𝑦 ∈ 𝑋 ↦ if ( 𝑥 ≤ 𝐵 , 𝐷 , 𝐸 ) ) ↾ ( ( 𝐵 [,] 𝐶 ) × 𝑋 ) ) ∈ ( ( ( 𝑂 ×t 𝐽 ) ↾t ( ( 𝐵 [,] 𝐶 ) × 𝑋 ) ) Cn 𝐾 ) )
167 12 13 40 50 63 126 153 166 paste ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐶 ) , 𝑦 ∈ 𝑋 ↦ if ( 𝑥 ≤ 𝐵 , 𝐷 , 𝐸 ) ) ∈ ( ( 𝑂 ×t 𝐽 ) Cn 𝐾 ) )