Step | Hyp | Ref
| Expression |
1 | | isinitoi.b |
. . 3
⊢ 𝐵 = (Base‘𝐶) |
2 | | isinitoi.h |
. . 3
⊢ 𝐻 = (Hom ‘𝐶) |
3 | | isinitoi.c |
. . 3
⊢ (𝜑 → 𝐶 ∈ Cat) |
4 | 1, 2, 3 | istermoi 17726 |
. 2
⊢ ((𝜑 ∧ 𝑂 ∈ (TermO‘𝐶)) → (𝑂 ∈ 𝐵 ∧ ∀𝑜 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝑜𝐻𝑂))) |
5 | | oveq1 7279 |
. . . . . . . 8
⊢ (𝑜 = 𝑂 → (𝑜𝐻𝑂) = (𝑂𝐻𝑂)) |
6 | 5 | eleq2d 2826 |
. . . . . . 7
⊢ (𝑜 = 𝑂 → (ℎ ∈ (𝑜𝐻𝑂) ↔ ℎ ∈ (𝑂𝐻𝑂))) |
7 | 6 | eubidv 2588 |
. . . . . 6
⊢ (𝑜 = 𝑂 → (∃!ℎ ℎ ∈ (𝑜𝐻𝑂) ↔ ∃!ℎ ℎ ∈ (𝑂𝐻𝑂))) |
8 | 7 | rspcv 3556 |
. . . . 5
⊢ (𝑂 ∈ 𝐵 → (∀𝑜 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝑜𝐻𝑂) → ∃!ℎ ℎ ∈ (𝑂𝐻𝑂))) |
9 | 8 | adantl 482 |
. . . 4
⊢ (((𝜑 ∧ 𝑂 ∈ (TermO‘𝐶)) ∧ 𝑂 ∈ 𝐵) → (∀𝑜 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝑜𝐻𝑂) → ∃!ℎ ℎ ∈ (𝑂𝐻𝑂))) |
10 | | eusn 4672 |
. . . . 5
⊢
(∃!ℎ ℎ ∈ (𝑂𝐻𝑂) ↔ ∃ℎ(𝑂𝐻𝑂) = {ℎ}) |
11 | | eqid 2740 |
. . . . . . . . 9
⊢
(Id‘𝐶) =
(Id‘𝐶) |
12 | 3 | ad2antrr 723 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑂 ∈ (TermO‘𝐶)) ∧ 𝑂 ∈ 𝐵) → 𝐶 ∈ Cat) |
13 | | simpr 485 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑂 ∈ (TermO‘𝐶)) ∧ 𝑂 ∈ 𝐵) → 𝑂 ∈ 𝐵) |
14 | 1, 2, 11, 12, 13 | catidcl 17402 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑂 ∈ (TermO‘𝐶)) ∧ 𝑂 ∈ 𝐵) → ((Id‘𝐶)‘𝑂) ∈ (𝑂𝐻𝑂)) |
15 | | fvex 6784 |
. . . . . . . . . . . . 13
⊢
((Id‘𝐶)‘𝑂) ∈ V |
16 | 15 | elsn 4582 |
. . . . . . . . . . . 12
⊢
(((Id‘𝐶)‘𝑂) ∈ {ℎ} ↔ ((Id‘𝐶)‘𝑂) = ℎ) |
17 | | eqcom 2747 |
. . . . . . . . . . . 12
⊢
(((Id‘𝐶)‘𝑂) = ℎ ↔ ℎ = ((Id‘𝐶)‘𝑂)) |
18 | | sneqbg 4780 |
. . . . . . . . . . . . . 14
⊢ (ℎ ∈ V → ({ℎ} = {((Id‘𝐶)‘𝑂)} ↔ ℎ = ((Id‘𝐶)‘𝑂))) |
19 | 18 | bicomd 222 |
. . . . . . . . . . . . 13
⊢ (ℎ ∈ V → (ℎ = ((Id‘𝐶)‘𝑂) ↔ {ℎ} = {((Id‘𝐶)‘𝑂)})) |
20 | 19 | elv 3437 |
. . . . . . . . . . . 12
⊢ (ℎ = ((Id‘𝐶)‘𝑂) ↔ {ℎ} = {((Id‘𝐶)‘𝑂)}) |
21 | 16, 17, 20 | 3bitri 297 |
. . . . . . . . . . 11
⊢
(((Id‘𝐶)‘𝑂) ∈ {ℎ} ↔ {ℎ} = {((Id‘𝐶)‘𝑂)}) |
22 | 21 | biimpi 215 |
. . . . . . . . . 10
⊢
(((Id‘𝐶)‘𝑂) ∈ {ℎ} → {ℎ} = {((Id‘𝐶)‘𝑂)}) |
23 | 22 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑂𝐻𝑂) = {ℎ} → (((Id‘𝐶)‘𝑂) ∈ {ℎ} → {ℎ} = {((Id‘𝐶)‘𝑂)})) |
24 | | eleq2 2829 |
. . . . . . . . 9
⊢ ((𝑂𝐻𝑂) = {ℎ} → (((Id‘𝐶)‘𝑂) ∈ (𝑂𝐻𝑂) ↔ ((Id‘𝐶)‘𝑂) ∈ {ℎ})) |
25 | | eqeq1 2744 |
. . . . . . . . 9
⊢ ((𝑂𝐻𝑂) = {ℎ} → ((𝑂𝐻𝑂) = {((Id‘𝐶)‘𝑂)} ↔ {ℎ} = {((Id‘𝐶)‘𝑂)})) |
26 | 23, 24, 25 | 3imtr4d 294 |
. . . . . . . 8
⊢ ((𝑂𝐻𝑂) = {ℎ} → (((Id‘𝐶)‘𝑂) ∈ (𝑂𝐻𝑂) → (𝑂𝐻𝑂) = {((Id‘𝐶)‘𝑂)})) |
27 | 14, 26 | syl5 34 |
. . . . . . 7
⊢ ((𝑂𝐻𝑂) = {ℎ} → (((𝜑 ∧ 𝑂 ∈ (TermO‘𝐶)) ∧ 𝑂 ∈ 𝐵) → (𝑂𝐻𝑂) = {((Id‘𝐶)‘𝑂)})) |
28 | 27 | exlimiv 1937 |
. . . . . 6
⊢
(∃ℎ(𝑂𝐻𝑂) = {ℎ} → (((𝜑 ∧ 𝑂 ∈ (TermO‘𝐶)) ∧ 𝑂 ∈ 𝐵) → (𝑂𝐻𝑂) = {((Id‘𝐶)‘𝑂)})) |
29 | 28 | com12 32 |
. . . . 5
⊢ (((𝜑 ∧ 𝑂 ∈ (TermO‘𝐶)) ∧ 𝑂 ∈ 𝐵) → (∃ℎ(𝑂𝐻𝑂) = {ℎ} → (𝑂𝐻𝑂) = {((Id‘𝐶)‘𝑂)})) |
30 | 10, 29 | syl5bi 241 |
. . . 4
⊢ (((𝜑 ∧ 𝑂 ∈ (TermO‘𝐶)) ∧ 𝑂 ∈ 𝐵) → (∃!ℎ ℎ ∈ (𝑂𝐻𝑂) → (𝑂𝐻𝑂) = {((Id‘𝐶)‘𝑂)})) |
31 | 9, 30 | syld 47 |
. . 3
⊢ (((𝜑 ∧ 𝑂 ∈ (TermO‘𝐶)) ∧ 𝑂 ∈ 𝐵) → (∀𝑜 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝑜𝐻𝑂) → (𝑂𝐻𝑂) = {((Id‘𝐶)‘𝑂)})) |
32 | 31 | expimpd 454 |
. 2
⊢ ((𝜑 ∧ 𝑂 ∈ (TermO‘𝐶)) → ((𝑂 ∈ 𝐵 ∧ ∀𝑜 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝑜𝐻𝑂)) → (𝑂𝐻𝑂) = {((Id‘𝐶)‘𝑂)})) |
33 | 4, 32 | mpd 15 |
1
⊢ ((𝜑 ∧ 𝑂 ∈ (TermO‘𝐶)) → (𝑂𝐻𝑂) = {((Id‘𝐶)‘𝑂)}) |