Step |
Hyp |
Ref |
Expression |
1 |
|
ebtwntg.1 |
⊢ ( 𝜑 → 𝑁 ∈ ℕ ) |
2 |
|
ebtwntg.2 |
⊢ 𝑃 = ( Base ‘ ( EEG ‘ 𝑁 ) ) |
3 |
|
ebtwntg.3 |
⊢ 𝐼 = ( Itv ‘ ( EEG ‘ 𝑁 ) ) |
4 |
|
ebtwntg.x |
⊢ ( 𝜑 → 𝑋 ∈ 𝑃 ) |
5 |
|
ebtwntg.y |
⊢ ( 𝜑 → 𝑌 ∈ 𝑃 ) |
6 |
|
ebtwntg.z |
⊢ ( 𝜑 → 𝑍 ∈ 𝑃 ) |
7 |
|
itvid |
⊢ Itv = Slot ( Itv ‘ ndx ) |
8 |
|
fvexd |
⊢ ( 𝜑 → ( EEG ‘ 𝑁 ) ∈ V ) |
9 |
|
eengstr |
⊢ ( 𝑁 ∈ ℕ → ( EEG ‘ 𝑁 ) Struct 〈 1 , ; 1 7 〉 ) |
10 |
1 9
|
syl |
⊢ ( 𝜑 → ( EEG ‘ 𝑁 ) Struct 〈 1 , ; 1 7 〉 ) |
11 |
|
structn0fun |
⊢ ( ( EEG ‘ 𝑁 ) Struct 〈 1 , ; 1 7 〉 → Fun ( ( EEG ‘ 𝑁 ) ∖ { ∅ } ) ) |
12 |
10 11
|
syl |
⊢ ( 𝜑 → Fun ( ( EEG ‘ 𝑁 ) ∖ { ∅ } ) ) |
13 |
|
structcnvcnv |
⊢ ( ( EEG ‘ 𝑁 ) Struct 〈 1 , ; 1 7 〉 → ◡ ◡ ( EEG ‘ 𝑁 ) = ( ( EEG ‘ 𝑁 ) ∖ { ∅ } ) ) |
14 |
10 13
|
syl |
⊢ ( 𝜑 → ◡ ◡ ( EEG ‘ 𝑁 ) = ( ( EEG ‘ 𝑁 ) ∖ { ∅ } ) ) |
15 |
14
|
funeqd |
⊢ ( 𝜑 → ( Fun ◡ ◡ ( EEG ‘ 𝑁 ) ↔ Fun ( ( EEG ‘ 𝑁 ) ∖ { ∅ } ) ) ) |
16 |
12 15
|
mpbird |
⊢ ( 𝜑 → Fun ◡ ◡ ( EEG ‘ 𝑁 ) ) |
17 |
|
opex |
⊢ 〈 ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn 〈 𝑥 , 𝑦 〉 } ) 〉 ∈ V |
18 |
17
|
prid1 |
⊢ 〈 ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn 〈 𝑥 , 𝑦 〉 } ) 〉 ∈ { 〈 ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn 〈 𝑥 , 𝑦 〉 } ) 〉 , 〈 ( LineG ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑧 Btwn 〈 𝑥 , 𝑦 〉 ∨ 𝑥 Btwn 〈 𝑧 , 𝑦 〉 ∨ 𝑦 Btwn 〈 𝑥 , 𝑧 〉 ) } ) 〉 } |
19 |
|
elun2 |
⊢ ( 〈 ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn 〈 𝑥 , 𝑦 〉 } ) 〉 ∈ { 〈 ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn 〈 𝑥 , 𝑦 〉 } ) 〉 , 〈 ( LineG ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑧 Btwn 〈 𝑥 , 𝑦 〉 ∨ 𝑥 Btwn 〈 𝑧 , 𝑦 〉 ∨ 𝑦 Btwn 〈 𝑥 , 𝑧 〉 ) } ) 〉 } → 〈 ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn 〈 𝑥 , 𝑦 〉 } ) 〉 ∈ ( { 〈 ( Base ‘ ndx ) , ( 𝔼 ‘ 𝑁 ) 〉 , 〈 ( dist ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ↑ 2 ) ) 〉 } ∪ { 〈 ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn 〈 𝑥 , 𝑦 〉 } ) 〉 , 〈 ( LineG ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑧 Btwn 〈 𝑥 , 𝑦 〉 ∨ 𝑥 Btwn 〈 𝑧 , 𝑦 〉 ∨ 𝑦 Btwn 〈 𝑥 , 𝑧 〉 ) } ) 〉 } ) ) |
20 |
18 19
|
ax-mp |
⊢ 〈 ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn 〈 𝑥 , 𝑦 〉 } ) 〉 ∈ ( { 〈 ( Base ‘ ndx ) , ( 𝔼 ‘ 𝑁 ) 〉 , 〈 ( dist ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ↑ 2 ) ) 〉 } ∪ { 〈 ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn 〈 𝑥 , 𝑦 〉 } ) 〉 , 〈 ( LineG ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑧 Btwn 〈 𝑥 , 𝑦 〉 ∨ 𝑥 Btwn 〈 𝑧 , 𝑦 〉 ∨ 𝑦 Btwn 〈 𝑥 , 𝑧 〉 ) } ) 〉 } ) |
21 |
|
eengv |
⊢ ( 𝑁 ∈ ℕ → ( EEG ‘ 𝑁 ) = ( { 〈 ( Base ‘ ndx ) , ( 𝔼 ‘ 𝑁 ) 〉 , 〈 ( dist ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ↑ 2 ) ) 〉 } ∪ { 〈 ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn 〈 𝑥 , 𝑦 〉 } ) 〉 , 〈 ( LineG ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑧 Btwn 〈 𝑥 , 𝑦 〉 ∨ 𝑥 Btwn 〈 𝑧 , 𝑦 〉 ∨ 𝑦 Btwn 〈 𝑥 , 𝑧 〉 ) } ) 〉 } ) ) |
22 |
1 21
|
syl |
⊢ ( 𝜑 → ( EEG ‘ 𝑁 ) = ( { 〈 ( Base ‘ ndx ) , ( 𝔼 ‘ 𝑁 ) 〉 , 〈 ( dist ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ Σ 𝑖 ∈ ( 1 ... 𝑁 ) ( ( ( 𝑥 ‘ 𝑖 ) − ( 𝑦 ‘ 𝑖 ) ) ↑ 2 ) ) 〉 } ∪ { 〈 ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn 〈 𝑥 , 𝑦 〉 } ) 〉 , 〈 ( LineG ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( ( 𝔼 ‘ 𝑁 ) ∖ { 𝑥 } ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ ( 𝑧 Btwn 〈 𝑥 , 𝑦 〉 ∨ 𝑥 Btwn 〈 𝑧 , 𝑦 〉 ∨ 𝑦 Btwn 〈 𝑥 , 𝑧 〉 ) } ) 〉 } ) ) |
23 |
20 22
|
eleqtrrid |
⊢ ( 𝜑 → 〈 ( Itv ‘ ndx ) , ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn 〈 𝑥 , 𝑦 〉 } ) 〉 ∈ ( EEG ‘ 𝑁 ) ) |
24 |
|
fvex |
⊢ ( 𝔼 ‘ 𝑁 ) ∈ V |
25 |
24 24
|
mpoex |
⊢ ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn 〈 𝑥 , 𝑦 〉 } ) ∈ V |
26 |
25
|
a1i |
⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn 〈 𝑥 , 𝑦 〉 } ) ∈ V ) |
27 |
7 8 16 23 26
|
strfv2d |
⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn 〈 𝑥 , 𝑦 〉 } ) = ( Itv ‘ ( EEG ‘ 𝑁 ) ) ) |
28 |
3 27
|
eqtr4id |
⊢ ( 𝜑 → 𝐼 = ( 𝑥 ∈ ( 𝔼 ‘ 𝑁 ) , 𝑦 ∈ ( 𝔼 ‘ 𝑁 ) ↦ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn 〈 𝑥 , 𝑦 〉 } ) ) |
29 |
|
simprl |
⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → 𝑥 = 𝑋 ) |
30 |
|
simprr |
⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → 𝑦 = 𝑌 ) |
31 |
29 30
|
opeq12d |
⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → 〈 𝑥 , 𝑦 〉 = 〈 𝑋 , 𝑌 〉 ) |
32 |
31
|
breq2d |
⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → ( 𝑧 Btwn 〈 𝑥 , 𝑦 〉 ↔ 𝑧 Btwn 〈 𝑋 , 𝑌 〉 ) ) |
33 |
32
|
rabbidv |
⊢ ( ( 𝜑 ∧ ( 𝑥 = 𝑋 ∧ 𝑦 = 𝑌 ) ) → { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn 〈 𝑥 , 𝑦 〉 } = { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn 〈 𝑋 , 𝑌 〉 } ) |
34 |
4 2
|
eleqtrdi |
⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) |
35 |
|
eengbas |
⊢ ( 𝑁 ∈ ℕ → ( 𝔼 ‘ 𝑁 ) = ( Base ‘ ( EEG ‘ 𝑁 ) ) ) |
36 |
1 35
|
syl |
⊢ ( 𝜑 → ( 𝔼 ‘ 𝑁 ) = ( Base ‘ ( EEG ‘ 𝑁 ) ) ) |
37 |
34 36
|
eleqtrrd |
⊢ ( 𝜑 → 𝑋 ∈ ( 𝔼 ‘ 𝑁 ) ) |
38 |
5 2
|
eleqtrdi |
⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) |
39 |
38 36
|
eleqtrrd |
⊢ ( 𝜑 → 𝑌 ∈ ( 𝔼 ‘ 𝑁 ) ) |
40 |
24
|
rabex |
⊢ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn 〈 𝑋 , 𝑌 〉 } ∈ V |
41 |
40
|
a1i |
⊢ ( 𝜑 → { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn 〈 𝑋 , 𝑌 〉 } ∈ V ) |
42 |
28 33 37 39 41
|
ovmpod |
⊢ ( 𝜑 → ( 𝑋 𝐼 𝑌 ) = { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn 〈 𝑋 , 𝑌 〉 } ) |
43 |
42
|
eleq2d |
⊢ ( 𝜑 → ( 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ↔ 𝑍 ∈ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn 〈 𝑋 , 𝑌 〉 } ) ) |
44 |
6 2
|
eleqtrdi |
⊢ ( 𝜑 → 𝑍 ∈ ( Base ‘ ( EEG ‘ 𝑁 ) ) ) |
45 |
44 36
|
eleqtrrd |
⊢ ( 𝜑 → 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) ) |
46 |
|
breq1 |
⊢ ( 𝑧 = 𝑍 → ( 𝑧 Btwn 〈 𝑋 , 𝑌 〉 ↔ 𝑍 Btwn 〈 𝑋 , 𝑌 〉 ) ) |
47 |
46
|
elrab3 |
⊢ ( 𝑍 ∈ ( 𝔼 ‘ 𝑁 ) → ( 𝑍 ∈ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn 〈 𝑋 , 𝑌 〉 } ↔ 𝑍 Btwn 〈 𝑋 , 𝑌 〉 ) ) |
48 |
45 47
|
syl |
⊢ ( 𝜑 → ( 𝑍 ∈ { 𝑧 ∈ ( 𝔼 ‘ 𝑁 ) ∣ 𝑧 Btwn 〈 𝑋 , 𝑌 〉 } ↔ 𝑍 Btwn 〈 𝑋 , 𝑌 〉 ) ) |
49 |
43 48
|
bitr2d |
⊢ ( 𝜑 → ( 𝑍 Btwn 〈 𝑋 , 𝑌 〉 ↔ 𝑍 ∈ ( 𝑋 𝐼 𝑌 ) ) ) |