| Step | Hyp | Ref
| Expression |
| 1 | | grpidval.o |
. 2
⊢ 0 =
(0g‘𝐺) |
| 2 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → (Base‘𝑔) = (Base‘𝐺)) |
| 3 | | grpidval.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝐺) |
| 4 | 2, 3 | eqtr4di 2795 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (Base‘𝑔) = 𝐵) |
| 5 | 4 | eleq2d 2827 |
. . . . . 6
⊢ (𝑔 = 𝐺 → (𝑒 ∈ (Base‘𝑔) ↔ 𝑒 ∈ 𝐵)) |
| 6 | | fveq2 6906 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝐺 → (+g‘𝑔) = (+g‘𝐺)) |
| 7 | | grpidval.p |
. . . . . . . . . . 11
⊢ + =
(+g‘𝐺) |
| 8 | 6, 7 | eqtr4di 2795 |
. . . . . . . . . 10
⊢ (𝑔 = 𝐺 → (+g‘𝑔) = + ) |
| 9 | 8 | oveqd 7448 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → (𝑒(+g‘𝑔)𝑥) = (𝑒 + 𝑥)) |
| 10 | 9 | eqeq1d 2739 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → ((𝑒(+g‘𝑔)𝑥) = 𝑥 ↔ (𝑒 + 𝑥) = 𝑥)) |
| 11 | 8 | oveqd 7448 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → (𝑥(+g‘𝑔)𝑒) = (𝑥 + 𝑒)) |
| 12 | 11 | eqeq1d 2739 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → ((𝑥(+g‘𝑔)𝑒) = 𝑥 ↔ (𝑥 + 𝑒) = 𝑥)) |
| 13 | 10, 12 | anbi12d 632 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → (((𝑒(+g‘𝑔)𝑥) = 𝑥 ∧ (𝑥(+g‘𝑔)𝑒) = 𝑥) ↔ ((𝑒 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑒) = 𝑥))) |
| 14 | 4, 13 | raleqbidv 3346 |
. . . . . 6
⊢ (𝑔 = 𝐺 → (∀𝑥 ∈ (Base‘𝑔)((𝑒(+g‘𝑔)𝑥) = 𝑥 ∧ (𝑥(+g‘𝑔)𝑒) = 𝑥) ↔ ∀𝑥 ∈ 𝐵 ((𝑒 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑒) = 𝑥))) |
| 15 | 5, 14 | anbi12d 632 |
. . . . 5
⊢ (𝑔 = 𝐺 → ((𝑒 ∈ (Base‘𝑔) ∧ ∀𝑥 ∈ (Base‘𝑔)((𝑒(+g‘𝑔)𝑥) = 𝑥 ∧ (𝑥(+g‘𝑔)𝑒) = 𝑥)) ↔ (𝑒 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ((𝑒 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑒) = 𝑥)))) |
| 16 | 15 | iotabidv 6545 |
. . . 4
⊢ (𝑔 = 𝐺 → (℩𝑒(𝑒 ∈ (Base‘𝑔) ∧ ∀𝑥 ∈ (Base‘𝑔)((𝑒(+g‘𝑔)𝑥) = 𝑥 ∧ (𝑥(+g‘𝑔)𝑒) = 𝑥))) = (℩𝑒(𝑒 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ((𝑒 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑒) = 𝑥)))) |
| 17 | | df-0g 17486 |
. . . 4
⊢
0g = (𝑔
∈ V ↦ (℩𝑒(𝑒 ∈ (Base‘𝑔) ∧ ∀𝑥 ∈ (Base‘𝑔)((𝑒(+g‘𝑔)𝑥) = 𝑥 ∧ (𝑥(+g‘𝑔)𝑒) = 𝑥)))) |
| 18 | | iotaex 6534 |
. . . 4
⊢
(℩𝑒(𝑒 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ((𝑒 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑒) = 𝑥))) ∈ V |
| 19 | 16, 17, 18 | fvmpt 7016 |
. . 3
⊢ (𝐺 ∈ V →
(0g‘𝐺) =
(℩𝑒(𝑒 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ((𝑒 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑒) = 𝑥)))) |
| 20 | | fvprc 6898 |
. . . 4
⊢ (¬
𝐺 ∈ V →
(0g‘𝐺) =
∅) |
| 21 | | euex 2577 |
. . . . . 6
⊢
(∃!𝑒(𝑒 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ((𝑒 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑒) = 𝑥)) → ∃𝑒(𝑒 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ((𝑒 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑒) = 𝑥))) |
| 22 | | n0i 4340 |
. . . . . . . . 9
⊢ (𝑒 ∈ 𝐵 → ¬ 𝐵 = ∅) |
| 23 | | fvprc 6898 |
. . . . . . . . . 10
⊢ (¬
𝐺 ∈ V →
(Base‘𝐺) =
∅) |
| 24 | 3, 23 | eqtrid 2789 |
. . . . . . . . 9
⊢ (¬
𝐺 ∈ V → 𝐵 = ∅) |
| 25 | 22, 24 | nsyl2 141 |
. . . . . . . 8
⊢ (𝑒 ∈ 𝐵 → 𝐺 ∈ V) |
| 26 | 25 | adantr 480 |
. . . . . . 7
⊢ ((𝑒 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ((𝑒 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑒) = 𝑥)) → 𝐺 ∈ V) |
| 27 | 26 | exlimiv 1930 |
. . . . . 6
⊢
(∃𝑒(𝑒 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ((𝑒 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑒) = 𝑥)) → 𝐺 ∈ V) |
| 28 | 21, 27 | syl 17 |
. . . . 5
⊢
(∃!𝑒(𝑒 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ((𝑒 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑒) = 𝑥)) → 𝐺 ∈ V) |
| 29 | | iotanul 6539 |
. . . . 5
⊢ (¬
∃!𝑒(𝑒 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ((𝑒 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑒) = 𝑥)) → (℩𝑒(𝑒 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ((𝑒 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑒) = 𝑥))) = ∅) |
| 30 | 28, 29 | nsyl5 159 |
. . . 4
⊢ (¬
𝐺 ∈ V →
(℩𝑒(𝑒 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ((𝑒 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑒) = 𝑥))) = ∅) |
| 31 | 20, 30 | eqtr4d 2780 |
. . 3
⊢ (¬
𝐺 ∈ V →
(0g‘𝐺) =
(℩𝑒(𝑒 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ((𝑒 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑒) = 𝑥)))) |
| 32 | 19, 31 | pm2.61i 182 |
. 2
⊢
(0g‘𝐺) = (℩𝑒(𝑒 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ((𝑒 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑒) = 𝑥))) |
| 33 | 1, 32 | eqtri 2765 |
1
⊢ 0 =
(℩𝑒(𝑒 ∈ 𝐵 ∧ ∀𝑥 ∈ 𝐵 ((𝑒 + 𝑥) = 𝑥 ∧ (𝑥 + 𝑒) = 𝑥))) |