Step | Hyp | Ref
| Expression |
1 | | isinitoi.b |
. . 3
⊢ 𝐵 = (Base‘𝐶) |
2 | | isinitoi.h |
. . 3
⊢ 𝐻 = (Hom ‘𝐶) |
3 | | isinitoi.c |
. . 3
⊢ (𝜑 → 𝐶 ∈ Cat) |
4 | 1, 2, 3 | istermoi 16654 |
. 2
⊢ ((𝜑 ∧ 𝑂 ∈ (TermO‘𝐶)) → (𝑂 ∈ 𝐵 ∧ ∀𝑜 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝑜𝐻𝑂))) |
5 | | oveq1 6657 |
. . . . . . . 8
⊢ (𝑜 = 𝑂 → (𝑜𝐻𝑂) = (𝑂𝐻𝑂)) |
6 | 5 | eleq2d 2687 |
. . . . . . 7
⊢ (𝑜 = 𝑂 → (ℎ ∈ (𝑜𝐻𝑂) ↔ ℎ ∈ (𝑂𝐻𝑂))) |
7 | 6 | eubidv 2490 |
. . . . . 6
⊢ (𝑜 = 𝑂 → (∃!ℎ ℎ ∈ (𝑜𝐻𝑂) ↔ ∃!ℎ ℎ ∈ (𝑂𝐻𝑂))) |
8 | 7 | rspcv 3305 |
. . . . 5
⊢ (𝑂 ∈ 𝐵 → (∀𝑜 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝑜𝐻𝑂) → ∃!ℎ ℎ ∈ (𝑂𝐻𝑂))) |
9 | 8 | adantl 482 |
. . . 4
⊢ (((𝜑 ∧ 𝑂 ∈ (TermO‘𝐶)) ∧ 𝑂 ∈ 𝐵) → (∀𝑜 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝑜𝐻𝑂) → ∃!ℎ ℎ ∈ (𝑂𝐻𝑂))) |
10 | | eusn 4265 |
. . . . 5
⊢
(∃!ℎ ℎ ∈ (𝑂𝐻𝑂) ↔ ∃ℎ(𝑂𝐻𝑂) = {ℎ}) |
11 | | eqid 2622 |
. . . . . . . . 9
⊢
(Id‘𝐶) =
(Id‘𝐶) |
12 | 3 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑂 ∈ (TermO‘𝐶)) ∧ 𝑂 ∈ 𝐵) → 𝐶 ∈ Cat) |
13 | | simpr 477 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑂 ∈ (TermO‘𝐶)) ∧ 𝑂 ∈ 𝐵) → 𝑂 ∈ 𝐵) |
14 | 1, 2, 11, 12, 13 | catidcl 16343 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑂 ∈ (TermO‘𝐶)) ∧ 𝑂 ∈ 𝐵) → ((Id‘𝐶)‘𝑂) ∈ (𝑂𝐻𝑂)) |
15 | | fvex 6201 |
. . . . . . . . . . . . 13
⊢
((Id‘𝐶)‘𝑂) ∈ V |
16 | 15 | elsn 4192 |
. . . . . . . . . . . 12
⊢
(((Id‘𝐶)‘𝑂) ∈ {ℎ} ↔ ((Id‘𝐶)‘𝑂) = ℎ) |
17 | | eqcom 2629 |
. . . . . . . . . . . 12
⊢
(((Id‘𝐶)‘𝑂) = ℎ ↔ ℎ = ((Id‘𝐶)‘𝑂)) |
18 | | vex 3203 |
. . . . . . . . . . . . 13
⊢ ℎ ∈ V |
19 | | sneqbg 4374 |
. . . . . . . . . . . . . 14
⊢ (ℎ ∈ V → ({ℎ} = {((Id‘𝐶)‘𝑂)} ↔ ℎ = ((Id‘𝐶)‘𝑂))) |
20 | 19 | bicomd 213 |
. . . . . . . . . . . . 13
⊢ (ℎ ∈ V → (ℎ = ((Id‘𝐶)‘𝑂) ↔ {ℎ} = {((Id‘𝐶)‘𝑂)})) |
21 | 18, 20 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (ℎ = ((Id‘𝐶)‘𝑂) ↔ {ℎ} = {((Id‘𝐶)‘𝑂)}) |
22 | 16, 17, 21 | 3bitri 286 |
. . . . . . . . . . 11
⊢
(((Id‘𝐶)‘𝑂) ∈ {ℎ} ↔ {ℎ} = {((Id‘𝐶)‘𝑂)}) |
23 | 22 | biimpi 206 |
. . . . . . . . . 10
⊢
(((Id‘𝐶)‘𝑂) ∈ {ℎ} → {ℎ} = {((Id‘𝐶)‘𝑂)}) |
24 | 23 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑂𝐻𝑂) = {ℎ} → (((Id‘𝐶)‘𝑂) ∈ {ℎ} → {ℎ} = {((Id‘𝐶)‘𝑂)})) |
25 | | eleq2 2690 |
. . . . . . . . 9
⊢ ((𝑂𝐻𝑂) = {ℎ} → (((Id‘𝐶)‘𝑂) ∈ (𝑂𝐻𝑂) ↔ ((Id‘𝐶)‘𝑂) ∈ {ℎ})) |
26 | | eqeq1 2626 |
. . . . . . . . 9
⊢ ((𝑂𝐻𝑂) = {ℎ} → ((𝑂𝐻𝑂) = {((Id‘𝐶)‘𝑂)} ↔ {ℎ} = {((Id‘𝐶)‘𝑂)})) |
27 | 24, 25, 26 | 3imtr4d 283 |
. . . . . . . 8
⊢ ((𝑂𝐻𝑂) = {ℎ} → (((Id‘𝐶)‘𝑂) ∈ (𝑂𝐻𝑂) → (𝑂𝐻𝑂) = {((Id‘𝐶)‘𝑂)})) |
28 | 14, 27 | syl5 34 |
. . . . . . 7
⊢ ((𝑂𝐻𝑂) = {ℎ} → (((𝜑 ∧ 𝑂 ∈ (TermO‘𝐶)) ∧ 𝑂 ∈ 𝐵) → (𝑂𝐻𝑂) = {((Id‘𝐶)‘𝑂)})) |
29 | 28 | exlimiv 1858 |
. . . . . 6
⊢
(∃ℎ(𝑂𝐻𝑂) = {ℎ} → (((𝜑 ∧ 𝑂 ∈ (TermO‘𝐶)) ∧ 𝑂 ∈ 𝐵) → (𝑂𝐻𝑂) = {((Id‘𝐶)‘𝑂)})) |
30 | 29 | com12 32 |
. . . . 5
⊢ (((𝜑 ∧ 𝑂 ∈ (TermO‘𝐶)) ∧ 𝑂 ∈ 𝐵) → (∃ℎ(𝑂𝐻𝑂) = {ℎ} → (𝑂𝐻𝑂) = {((Id‘𝐶)‘𝑂)})) |
31 | 10, 30 | syl5bi 232 |
. . . 4
⊢ (((𝜑 ∧ 𝑂 ∈ (TermO‘𝐶)) ∧ 𝑂 ∈ 𝐵) → (∃!ℎ ℎ ∈ (𝑂𝐻𝑂) → (𝑂𝐻𝑂) = {((Id‘𝐶)‘𝑂)})) |
32 | 9, 31 | syld 47 |
. . 3
⊢ (((𝜑 ∧ 𝑂 ∈ (TermO‘𝐶)) ∧ 𝑂 ∈ 𝐵) → (∀𝑜 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝑜𝐻𝑂) → (𝑂𝐻𝑂) = {((Id‘𝐶)‘𝑂)})) |
33 | 32 | expimpd 629 |
. 2
⊢ ((𝜑 ∧ 𝑂 ∈ (TermO‘𝐶)) → ((𝑂 ∈ 𝐵 ∧ ∀𝑜 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝑜𝐻𝑂)) → (𝑂𝐻𝑂) = {((Id‘𝐶)‘𝑂)})) |
34 | 4, 33 | mpd 15 |
1
⊢ ((𝜑 ∧ 𝑂 ∈ (TermO‘𝐶)) → (𝑂𝐻𝑂) = {((Id‘𝐶)‘𝑂)}) |