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