Step | Hyp | Ref
| Expression |
1 | | ttgval.n |
. . . . . 6
⊢ 𝐺 = (toTG‘𝐻) |
2 | | eqid 2795 |
. . . . . 6
⊢
(Base‘𝐻) =
(Base‘𝐻) |
3 | | eqid 2795 |
. . . . . 6
⊢
(-g‘𝐻) = (-g‘𝐻) |
4 | | eqid 2795 |
. . . . . 6
⊢ (
·𝑠 ‘𝐻) = ( ·𝑠
‘𝐻) |
5 | | eqid 2795 |
. . . . . 6
⊢
(Itv‘𝐺) =
(Itv‘𝐺) |
6 | 1, 2, 3, 4, 5 | ttgval 26344 |
. . . . 5
⊢ (𝐻 ∈ V → (𝐺 = ((𝐻 sSet 〈(Itv‘ndx), (𝑥 ∈ (Base‘𝐻), 𝑦 ∈ (Base‘𝐻) ↦ {𝑧 ∈ (Base‘𝐻) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g‘𝐻)𝑥) = (𝑘( ·𝑠
‘𝐻)(𝑦(-g‘𝐻)𝑥))})〉) sSet 〈(LineG‘ndx),
(𝑥 ∈ (Base‘𝐻), 𝑦 ∈ (Base‘𝐻) ↦ {𝑧 ∈ (Base‘𝐻) ∣ (𝑧 ∈ (𝑥(Itv‘𝐺)𝑦) ∨ 𝑥 ∈ (𝑧(Itv‘𝐺)𝑦) ∨ 𝑦 ∈ (𝑥(Itv‘𝐺)𝑧))})〉) ∧ (Itv‘𝐺) = (𝑥 ∈ (Base‘𝐻), 𝑦 ∈ (Base‘𝐻) ↦ {𝑧 ∈ (Base‘𝐻) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g‘𝐻)𝑥) = (𝑘( ·𝑠
‘𝐻)(𝑦(-g‘𝐻)𝑥))}))) |
7 | 6 | simpld 495 |
. . . 4
⊢ (𝐻 ∈ V → 𝐺 = ((𝐻 sSet 〈(Itv‘ndx), (𝑥 ∈ (Base‘𝐻), 𝑦 ∈ (Base‘𝐻) ↦ {𝑧 ∈ (Base‘𝐻) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g‘𝐻)𝑥) = (𝑘( ·𝑠
‘𝐻)(𝑦(-g‘𝐻)𝑥))})〉) sSet 〈(LineG‘ndx),
(𝑥 ∈ (Base‘𝐻), 𝑦 ∈ (Base‘𝐻) ↦ {𝑧 ∈ (Base‘𝐻) ∣ (𝑧 ∈ (𝑥(Itv‘𝐺)𝑦) ∨ 𝑥 ∈ (𝑧(Itv‘𝐺)𝑦) ∨ 𝑦 ∈ (𝑥(Itv‘𝐺)𝑧))})〉)) |
8 | 7 | fveq2d 6542 |
. . 3
⊢ (𝐻 ∈ V → (𝐸‘𝐺) = (𝐸‘((𝐻 sSet 〈(Itv‘ndx), (𝑥 ∈ (Base‘𝐻), 𝑦 ∈ (Base‘𝐻) ↦ {𝑧 ∈ (Base‘𝐻) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g‘𝐻)𝑥) = (𝑘( ·𝑠
‘𝐻)(𝑦(-g‘𝐻)𝑥))})〉) sSet 〈(LineG‘ndx),
(𝑥 ∈ (Base‘𝐻), 𝑦 ∈ (Base‘𝐻) ↦ {𝑧 ∈ (Base‘𝐻) ∣ (𝑧 ∈ (𝑥(Itv‘𝐺)𝑦) ∨ 𝑥 ∈ (𝑧(Itv‘𝐺)𝑦) ∨ 𝑦 ∈ (𝑥(Itv‘𝐺)𝑧))})〉))) |
9 | | ttglem.2 |
. . . . . 6
⊢ 𝐸 = Slot 𝑁 |
10 | | ttglem.3 |
. . . . . 6
⊢ 𝑁 ∈ ℕ |
11 | 9, 10 | ndxid 16338 |
. . . . 5
⊢ 𝐸 = Slot (𝐸‘ndx) |
12 | 10 | nnrei 11495 |
. . . . . . 7
⊢ 𝑁 ∈ ℝ |
13 | | ttglem.4 |
. . . . . . 7
⊢ 𝑁 < ;16 |
14 | 12, 13 | ltneii 10600 |
. . . . . 6
⊢ 𝑁 ≠ ;16 |
15 | 9, 10 | ndxarg 16337 |
. . . . . . 7
⊢ (𝐸‘ndx) = 𝑁 |
16 | | itvndx 25908 |
. . . . . . 7
⊢
(Itv‘ndx) = ;16 |
17 | 15, 16 | neeq12i 3050 |
. . . . . 6
⊢ ((𝐸‘ndx) ≠ (Itv‘ndx)
↔ 𝑁 ≠ ;16) |
18 | 14, 17 | mpbir 232 |
. . . . 5
⊢ (𝐸‘ndx) ≠
(Itv‘ndx) |
19 | 11, 18 | setsnid 16368 |
. . . 4
⊢ (𝐸‘𝐻) = (𝐸‘(𝐻 sSet 〈(Itv‘ndx), (𝑥 ∈ (Base‘𝐻), 𝑦 ∈ (Base‘𝐻) ↦ {𝑧 ∈ (Base‘𝐻) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g‘𝐻)𝑥) = (𝑘( ·𝑠
‘𝐻)(𝑦(-g‘𝐻)𝑥))})〉)) |
20 | | 1nn0 11761 |
. . . . . . . . 9
⊢ 1 ∈
ℕ0 |
21 | | 6nn0 11766 |
. . . . . . . . 9
⊢ 6 ∈
ℕ0 |
22 | | 7nn 11577 |
. . . . . . . . 9
⊢ 7 ∈
ℕ |
23 | | 6lt7 11671 |
. . . . . . . . 9
⊢ 6 <
7 |
24 | 20, 21, 22, 23 | declt 11975 |
. . . . . . . 8
⊢ ;16 < ;17 |
25 | | 6nn 11574 |
. . . . . . . . . . 11
⊢ 6 ∈
ℕ |
26 | 20, 25 | decnncl 11967 |
. . . . . . . . . 10
⊢ ;16 ∈ ℕ |
27 | 26 | nnrei 11495 |
. . . . . . . . 9
⊢ ;16 ∈ ℝ |
28 | 20, 22 | decnncl 11967 |
. . . . . . . . . 10
⊢ ;17 ∈ ℕ |
29 | 28 | nnrei 11495 |
. . . . . . . . 9
⊢ ;17 ∈ ℝ |
30 | 12, 27, 29 | lttri 10613 |
. . . . . . . 8
⊢ ((𝑁 < ;16 ∧ ;16 < ;17) → 𝑁 < ;17) |
31 | 13, 24, 30 | mp2an 688 |
. . . . . . 7
⊢ 𝑁 < ;17 |
32 | 12, 31 | ltneii 10600 |
. . . . . 6
⊢ 𝑁 ≠ ;17 |
33 | | lngndx 25909 |
. . . . . . 7
⊢
(LineG‘ndx) = ;17 |
34 | 15, 33 | neeq12i 3050 |
. . . . . 6
⊢ ((𝐸‘ndx) ≠
(LineG‘ndx) ↔ 𝑁
≠ ;17) |
35 | 32, 34 | mpbir 232 |
. . . . 5
⊢ (𝐸‘ndx) ≠
(LineG‘ndx) |
36 | 11, 35 | setsnid 16368 |
. . . 4
⊢ (𝐸‘(𝐻 sSet 〈(Itv‘ndx), (𝑥 ∈ (Base‘𝐻), 𝑦 ∈ (Base‘𝐻) ↦ {𝑧 ∈ (Base‘𝐻) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g‘𝐻)𝑥) = (𝑘( ·𝑠
‘𝐻)(𝑦(-g‘𝐻)𝑥))})〉)) = (𝐸‘((𝐻 sSet 〈(Itv‘ndx), (𝑥 ∈ (Base‘𝐻), 𝑦 ∈ (Base‘𝐻) ↦ {𝑧 ∈ (Base‘𝐻) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g‘𝐻)𝑥) = (𝑘( ·𝑠
‘𝐻)(𝑦(-g‘𝐻)𝑥))})〉) sSet 〈(LineG‘ndx),
(𝑥 ∈ (Base‘𝐻), 𝑦 ∈ (Base‘𝐻) ↦ {𝑧 ∈ (Base‘𝐻) ∣ (𝑧 ∈ (𝑥(Itv‘𝐺)𝑦) ∨ 𝑥 ∈ (𝑧(Itv‘𝐺)𝑦) ∨ 𝑦 ∈ (𝑥(Itv‘𝐺)𝑧))})〉)) |
37 | 19, 36 | eqtri 2819 |
. . 3
⊢ (𝐸‘𝐻) = (𝐸‘((𝐻 sSet 〈(Itv‘ndx), (𝑥 ∈ (Base‘𝐻), 𝑦 ∈ (Base‘𝐻) ↦ {𝑧 ∈ (Base‘𝐻) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g‘𝐻)𝑥) = (𝑘( ·𝑠
‘𝐻)(𝑦(-g‘𝐻)𝑥))})〉) sSet 〈(LineG‘ndx),
(𝑥 ∈ (Base‘𝐻), 𝑦 ∈ (Base‘𝐻) ↦ {𝑧 ∈ (Base‘𝐻) ∣ (𝑧 ∈ (𝑥(Itv‘𝐺)𝑦) ∨ 𝑥 ∈ (𝑧(Itv‘𝐺)𝑦) ∨ 𝑦 ∈ (𝑥(Itv‘𝐺)𝑧))})〉)) |
38 | 8, 37 | syl6reqr 2850 |
. 2
⊢ (𝐻 ∈ V → (𝐸‘𝐻) = (𝐸‘𝐺)) |
39 | 9 | str0 16364 |
. . 3
⊢ ∅ =
(𝐸‘∅) |
40 | | fvprc 6531 |
. . 3
⊢ (¬
𝐻 ∈ V → (𝐸‘𝐻) = ∅) |
41 | | fvprc 6531 |
. . . . 5
⊢ (¬
𝐻 ∈ V →
(toTG‘𝐻) =
∅) |
42 | 1, 41 | syl5eq 2843 |
. . . 4
⊢ (¬
𝐻 ∈ V → 𝐺 = ∅) |
43 | 42 | fveq2d 6542 |
. . 3
⊢ (¬
𝐻 ∈ V → (𝐸‘𝐺) = (𝐸‘∅)) |
44 | 39, 40, 43 | 3eqtr4a 2857 |
. 2
⊢ (¬
𝐻 ∈ V → (𝐸‘𝐻) = (𝐸‘𝐺)) |
45 | 38, 44 | pm2.61i 183 |
1
⊢ (𝐸‘𝐻) = (𝐸‘𝐺) |