| Step | Hyp | Ref
| Expression |
| 1 | | ax-hilex 31018 |
. . . 4
⊢ ℋ
∈ V |
| 2 | | fex2 7958 |
. . . 4
⊢ ((𝑇: ℋ⟶ ℋ ∧
ℋ ∈ V ∧ ℋ ∈ V) → 𝑇 ∈ V) |
| 3 | 1, 1, 2 | mp3an23 1455 |
. . 3
⊢ (𝑇: ℋ⟶ ℋ →
𝑇 ∈
V) |
| 4 | | feq1 6716 |
. . . . . . . . 9
⊢ (𝑡 = 𝑇 → (𝑡: ℋ⟶ ℋ ↔ 𝑇: ℋ⟶
ℋ)) |
| 5 | | fveq1 6905 |
. . . . . . . . . . . 12
⊢ (𝑡 = 𝑇 → (𝑡‘𝑦) = (𝑇‘𝑦)) |
| 6 | 5 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ (𝑡 = 𝑇 → (𝑥 ·ih (𝑡‘𝑦)) = (𝑥 ·ih (𝑇‘𝑦))) |
| 7 | 6 | eqeq1d 2739 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑇 → ((𝑥 ·ih (𝑡‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦) ↔ (𝑥 ·ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦))) |
| 8 | 7 | 2ralbidv 3221 |
. . . . . . . . 9
⊢ (𝑡 = 𝑇 → (∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑡‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦) ↔ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥
·ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦))) |
| 9 | 4, 8 | 3anbi13d 1440 |
. . . . . . . 8
⊢ (𝑡 = 𝑇 → ((𝑡: ℋ⟶ ℋ ∧ 𝑢: ℋ⟶ ℋ ∧
∀𝑥 ∈ ℋ
∀𝑦 ∈ ℋ
(𝑥
·ih (𝑡‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦)) ↔ (𝑇: ℋ⟶ ℋ ∧ 𝑢: ℋ⟶ ℋ ∧
∀𝑥 ∈ ℋ
∀𝑦 ∈ ℋ
(𝑥
·ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦)))) |
| 10 | | 3anass 1095 |
. . . . . . . 8
⊢ ((𝑇: ℋ⟶ ℋ ∧
𝑢: ℋ⟶ ℋ
∧ ∀𝑥 ∈
ℋ ∀𝑦 ∈
ℋ (𝑥
·ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦)) ↔ (𝑇: ℋ⟶ ℋ ∧ (𝑢: ℋ⟶ ℋ ∧
∀𝑥 ∈ ℋ
∀𝑦 ∈ ℋ
(𝑥
·ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦)))) |
| 11 | 9, 10 | bitrdi 287 |
. . . . . . 7
⊢ (𝑡 = 𝑇 → ((𝑡: ℋ⟶ ℋ ∧ 𝑢: ℋ⟶ ℋ ∧
∀𝑥 ∈ ℋ
∀𝑦 ∈ ℋ
(𝑥
·ih (𝑡‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦)) ↔ (𝑇: ℋ⟶ ℋ ∧ (𝑢: ℋ⟶ ℋ ∧
∀𝑥 ∈ ℋ
∀𝑦 ∈ ℋ
(𝑥
·ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦))))) |
| 12 | 11 | exbidv 1921 |
. . . . . 6
⊢ (𝑡 = 𝑇 → (∃𝑢(𝑡: ℋ⟶ ℋ ∧ 𝑢: ℋ⟶ ℋ ∧
∀𝑥 ∈ ℋ
∀𝑦 ∈ ℋ
(𝑥
·ih (𝑡‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦)) ↔ ∃𝑢(𝑇: ℋ⟶ ℋ ∧ (𝑢: ℋ⟶ ℋ ∧
∀𝑥 ∈ ℋ
∀𝑦 ∈ ℋ
(𝑥
·ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦))))) |
| 13 | | 19.42v 1953 |
. . . . . 6
⊢
(∃𝑢(𝑇: ℋ⟶ ℋ ∧
(𝑢: ℋ⟶ ℋ
∧ ∀𝑥 ∈
ℋ ∀𝑦 ∈
ℋ (𝑥
·ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦))) ↔ (𝑇: ℋ⟶ ℋ ∧ ∃𝑢(𝑢: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥
·ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦)))) |
| 14 | 12, 13 | bitrdi 287 |
. . . . 5
⊢ (𝑡 = 𝑇 → (∃𝑢(𝑡: ℋ⟶ ℋ ∧ 𝑢: ℋ⟶ ℋ ∧
∀𝑥 ∈ ℋ
∀𝑦 ∈ ℋ
(𝑥
·ih (𝑡‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦)) ↔ (𝑇: ℋ⟶ ℋ ∧ ∃𝑢(𝑢: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥
·ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦))))) |
| 15 | | dfadj2 31904 |
. . . . . . 7
⊢
adjℎ = {〈𝑡, 𝑢〉 ∣ (𝑡: ℋ⟶ ℋ ∧ 𝑢: ℋ⟶ ℋ ∧
∀𝑥 ∈ ℋ
∀𝑦 ∈ ℋ
(𝑥
·ih (𝑡‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦))} |
| 16 | 15 | dmeqi 5915 |
. . . . . 6
⊢ dom
adjℎ = dom {〈𝑡, 𝑢〉 ∣ (𝑡: ℋ⟶ ℋ ∧ 𝑢: ℋ⟶ ℋ ∧
∀𝑥 ∈ ℋ
∀𝑦 ∈ ℋ
(𝑥
·ih (𝑡‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦))} |
| 17 | | dmopab 5926 |
. . . . . 6
⊢ dom
{〈𝑡, 𝑢〉 ∣ (𝑡: ℋ⟶ ℋ ∧
𝑢: ℋ⟶ ℋ
∧ ∀𝑥 ∈
ℋ ∀𝑦 ∈
ℋ (𝑥
·ih (𝑡‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦))} = {𝑡 ∣ ∃𝑢(𝑡: ℋ⟶ ℋ ∧ 𝑢: ℋ⟶ ℋ ∧
∀𝑥 ∈ ℋ
∀𝑦 ∈ ℋ
(𝑥
·ih (𝑡‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦))} |
| 18 | 16, 17 | eqtri 2765 |
. . . . 5
⊢ dom
adjℎ = {𝑡
∣ ∃𝑢(𝑡: ℋ⟶ ℋ ∧
𝑢: ℋ⟶ ℋ
∧ ∀𝑥 ∈
ℋ ∀𝑦 ∈
ℋ (𝑥
·ih (𝑡‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦))} |
| 19 | 14, 18 | elab2g 3680 |
. . . 4
⊢ (𝑇 ∈ V → (𝑇 ∈ dom
adjℎ ↔ (𝑇: ℋ⟶ ℋ ∧ ∃𝑢(𝑢: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥
·ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦))))) |
| 20 | 19 | baibd 539 |
. . 3
⊢ ((𝑇 ∈ V ∧ 𝑇: ℋ⟶ ℋ)
→ (𝑇 ∈ dom
adjℎ ↔ ∃𝑢(𝑢: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥
·ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦)))) |
| 21 | 3, 20 | mpancom 688 |
. 2
⊢ (𝑇: ℋ⟶ ℋ →
(𝑇 ∈ dom
adjℎ ↔ ∃𝑢(𝑢: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥
·ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦)))) |
| 22 | | df-reu 3381 |
. . 3
⊢
(∃!𝑢 ∈ (
ℋ ↑m ℋ)∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦) ↔ ∃!𝑢(𝑢 ∈ ( ℋ ↑m ℋ)
∧ ∀𝑥 ∈
ℋ ∀𝑦 ∈
ℋ (𝑥
·ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦))) |
| 23 | 1, 1 | elmap 8911 |
. . . . 5
⊢ (𝑢 ∈ ( ℋ
↑m ℋ) ↔ 𝑢: ℋ⟶ ℋ) |
| 24 | 23 | anbi1i 624 |
. . . 4
⊢ ((𝑢 ∈ ( ℋ
↑m ℋ) ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦)) ↔ (𝑢: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥
·ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦))) |
| 25 | 24 | eubii 2585 |
. . 3
⊢
(∃!𝑢(𝑢 ∈ ( ℋ
↑m ℋ) ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦)) ↔ ∃!𝑢(𝑢: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥
·ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦))) |
| 26 | | adjmo 31851 |
. . . 4
⊢
∃*𝑢(𝑢: ℋ⟶ ℋ ∧
∀𝑥 ∈ ℋ
∀𝑦 ∈ ℋ
(𝑥
·ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦)) |
| 27 | | df-eu 2569 |
. . . 4
⊢
(∃!𝑢(𝑢: ℋ⟶ ℋ ∧
∀𝑥 ∈ ℋ
∀𝑦 ∈ ℋ
(𝑥
·ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦)) ↔ (∃𝑢(𝑢: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥
·ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦)) ∧ ∃*𝑢(𝑢: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥
·ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦)))) |
| 28 | 26, 27 | mpbiran2 710 |
. . 3
⊢
(∃!𝑢(𝑢: ℋ⟶ ℋ ∧
∀𝑥 ∈ ℋ
∀𝑦 ∈ ℋ
(𝑥
·ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦)) ↔ ∃𝑢(𝑢: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥
·ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦))) |
| 29 | 22, 25, 28 | 3bitri 297 |
. 2
⊢
(∃!𝑢 ∈ (
ℋ ↑m ℋ)∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥 ·ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦) ↔ ∃𝑢(𝑢: ℋ⟶ ℋ ∧ ∀𝑥 ∈ ℋ ∀𝑦 ∈ ℋ (𝑥
·ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦))) |
| 30 | 21, 29 | bitr4di 289 |
1
⊢ (𝑇: ℋ⟶ ℋ →
(𝑇 ∈ dom
adjℎ ↔ ∃!𝑢 ∈ ( ℋ ↑m
ℋ)∀𝑥 ∈
ℋ ∀𝑦 ∈
ℋ (𝑥
·ih (𝑇‘𝑦)) = ((𝑢‘𝑥) ·ih 𝑦))) |