Step | Hyp | Ref
| Expression |
1 | | ttglem.2 |
. . . . . 6
⊢ 𝐸 = Slot 𝑁 |
2 | | ttglem.3 |
. . . . . 6
⊢ 𝑁 ∈ ℕ |
3 | 1, 2 | ndxid 16748 |
. . . . 5
⊢ 𝐸 = Slot (𝐸‘ndx) |
4 | 2 | nnrei 11839 |
. . . . . . 7
⊢ 𝑁 ∈ ℝ |
5 | | ttglem.4 |
. . . . . . 7
⊢ 𝑁 < ;16 |
6 | 4, 5 | ltneii 10945 |
. . . . . 6
⊢ 𝑁 ≠ ;16 |
7 | 1, 2 | ndxarg 16747 |
. . . . . . 7
⊢ (𝐸‘ndx) = 𝑁 |
8 | | itvndx 26531 |
. . . . . . 7
⊢
(Itv‘ndx) = ;16 |
9 | 7, 8 | neeq12i 3007 |
. . . . . 6
⊢ ((𝐸‘ndx) ≠ (Itv‘ndx)
↔ 𝑁 ≠ ;16) |
10 | 6, 9 | mpbir 234 |
. . . . 5
⊢ (𝐸‘ndx) ≠
(Itv‘ndx) |
11 | 3, 10 | setsnid 16759 |
. . . 4
⊢ (𝐸‘𝐻) = (𝐸‘(𝐻 sSet 〈(Itv‘ndx), (𝑥 ∈ (Base‘𝐻), 𝑦 ∈ (Base‘𝐻) ↦ {𝑧 ∈ (Base‘𝐻) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g‘𝐻)𝑥) = (𝑘( ·𝑠
‘𝐻)(𝑦(-g‘𝐻)𝑥))})〉)) |
12 | | 1nn0 12106 |
. . . . . . . . 9
⊢ 1 ∈
ℕ0 |
13 | | 6nn0 12111 |
. . . . . . . . 9
⊢ 6 ∈
ℕ0 |
14 | | 7nn 11922 |
. . . . . . . . 9
⊢ 7 ∈
ℕ |
15 | | 6lt7 12016 |
. . . . . . . . 9
⊢ 6 <
7 |
16 | 12, 13, 14, 15 | declt 12321 |
. . . . . . . 8
⊢ ;16 < ;17 |
17 | | 6nn 11919 |
. . . . . . . . . . 11
⊢ 6 ∈
ℕ |
18 | 12, 17 | decnncl 12313 |
. . . . . . . . . 10
⊢ ;16 ∈ ℕ |
19 | 18 | nnrei 11839 |
. . . . . . . . 9
⊢ ;16 ∈ ℝ |
20 | 12, 14 | decnncl 12313 |
. . . . . . . . . 10
⊢ ;17 ∈ ℕ |
21 | 20 | nnrei 11839 |
. . . . . . . . 9
⊢ ;17 ∈ ℝ |
22 | 4, 19, 21 | lttri 10958 |
. . . . . . . 8
⊢ ((𝑁 < ;16 ∧ ;16 < ;17) → 𝑁 < ;17) |
23 | 5, 16, 22 | mp2an 692 |
. . . . . . 7
⊢ 𝑁 < ;17 |
24 | 4, 23 | ltneii 10945 |
. . . . . 6
⊢ 𝑁 ≠ ;17 |
25 | | lngndx 26532 |
. . . . . . 7
⊢
(LineG‘ndx) = ;17 |
26 | 7, 25 | neeq12i 3007 |
. . . . . 6
⊢ ((𝐸‘ndx) ≠
(LineG‘ndx) ↔ 𝑁
≠ ;17) |
27 | 24, 26 | mpbir 234 |
. . . . 5
⊢ (𝐸‘ndx) ≠
(LineG‘ndx) |
28 | 3, 27 | setsnid 16759 |
. . . 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‘𝐺)𝑧))})〉)) |
29 | 11, 28 | eqtri 2765 |
. . 3
⊢ (𝐸‘𝐻) = (𝐸‘((𝐻 sSet 〈(Itv‘ndx), (𝑥 ∈ (Base‘𝐻), 𝑦 ∈ (Base‘𝐻) ↦ {𝑧 ∈ (Base‘𝐻) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g‘𝐻)𝑥) = (𝑘( ·𝑠
‘𝐻)(𝑦(-g‘𝐻)𝑥))})〉) sSet 〈(LineG‘ndx),
(𝑥 ∈ (Base‘𝐻), 𝑦 ∈ (Base‘𝐻) ↦ {𝑧 ∈ (Base‘𝐻) ∣ (𝑧 ∈ (𝑥(Itv‘𝐺)𝑦) ∨ 𝑥 ∈ (𝑧(Itv‘𝐺)𝑦) ∨ 𝑦 ∈ (𝑥(Itv‘𝐺)𝑧))})〉)) |
30 | | ttgval.n |
. . . . . 6
⊢ 𝐺 = (toTG‘𝐻) |
31 | | eqid 2737 |
. . . . . 6
⊢
(Base‘𝐻) =
(Base‘𝐻) |
32 | | eqid 2737 |
. . . . . 6
⊢
(-g‘𝐻) = (-g‘𝐻) |
33 | | eqid 2737 |
. . . . . 6
⊢ (
·𝑠 ‘𝐻) = ( ·𝑠
‘𝐻) |
34 | | eqid 2737 |
. . . . . 6
⊢
(Itv‘𝐺) =
(Itv‘𝐺) |
35 | 30, 31, 32, 33, 34 | ttgval 26966 |
. . . . 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‘𝐻)𝑥))}))) |
36 | 35 | simpld 498 |
. . . 4
⊢ (𝐻 ∈ V → 𝐺 = ((𝐻 sSet 〈(Itv‘ndx), (𝑥 ∈ (Base‘𝐻), 𝑦 ∈ (Base‘𝐻) ↦ {𝑧 ∈ (Base‘𝐻) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g‘𝐻)𝑥) = (𝑘( ·𝑠
‘𝐻)(𝑦(-g‘𝐻)𝑥))})〉) sSet 〈(LineG‘ndx),
(𝑥 ∈ (Base‘𝐻), 𝑦 ∈ (Base‘𝐻) ↦ {𝑧 ∈ (Base‘𝐻) ∣ (𝑧 ∈ (𝑥(Itv‘𝐺)𝑦) ∨ 𝑥 ∈ (𝑧(Itv‘𝐺)𝑦) ∨ 𝑦 ∈ (𝑥(Itv‘𝐺)𝑧))})〉)) |
37 | 36 | fveq2d 6721 |
. . 3
⊢ (𝐻 ∈ V → (𝐸‘𝐺) = (𝐸‘((𝐻 sSet 〈(Itv‘ndx), (𝑥 ∈ (Base‘𝐻), 𝑦 ∈ (Base‘𝐻) ↦ {𝑧 ∈ (Base‘𝐻) ∣ ∃𝑘 ∈ (0[,]1)(𝑧(-g‘𝐻)𝑥) = (𝑘( ·𝑠
‘𝐻)(𝑦(-g‘𝐻)𝑥))})〉) sSet 〈(LineG‘ndx),
(𝑥 ∈ (Base‘𝐻), 𝑦 ∈ (Base‘𝐻) ↦ {𝑧 ∈ (Base‘𝐻) ∣ (𝑧 ∈ (𝑥(Itv‘𝐺)𝑦) ∨ 𝑥 ∈ (𝑧(Itv‘𝐺)𝑦) ∨ 𝑦 ∈ (𝑥(Itv‘𝐺)𝑧))})〉))) |
38 | 29, 37 | eqtr4id 2797 |
. 2
⊢ (𝐻 ∈ V → (𝐸‘𝐻) = (𝐸‘𝐺)) |
39 | 1 | str0 16742 |
. . 3
⊢ ∅ =
(𝐸‘∅) |
40 | | fvprc 6709 |
. . 3
⊢ (¬
𝐻 ∈ V → (𝐸‘𝐻) = ∅) |
41 | | fvprc 6709 |
. . . . 5
⊢ (¬
𝐻 ∈ V →
(toTG‘𝐻) =
∅) |
42 | 30, 41 | syl5eq 2790 |
. . . 4
⊢ (¬
𝐻 ∈ V → 𝐺 = ∅) |
43 | 42 | fveq2d 6721 |
. . 3
⊢ (¬
𝐻 ∈ V → (𝐸‘𝐺) = (𝐸‘∅)) |
44 | 39, 40, 43 | 3eqtr4a 2804 |
. 2
⊢ (¬
𝐻 ∈ V → (𝐸‘𝐻) = (𝐸‘𝐺)) |
45 | 38, 44 | pm2.61i 185 |
1
⊢ (𝐸‘𝐻) = (𝐸‘𝐺) |