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