Step | Hyp | Ref
| Expression |
1 | | isinitoi.b |
. . 3
⊢ 𝐵 = (Base‘𝐶) |
2 | | isinitoi.h |
. . 3
⊢ 𝐻 = (Hom ‘𝐶) |
3 | | isinitoi.c |
. . 3
⊢ (𝜑 → 𝐶 ∈ Cat) |
4 | 1, 2, 3 | isinitoi 17529 |
. 2
⊢ ((𝜑 ∧ 𝑂 ∈ (InitO‘𝐶)) → (𝑂 ∈ 𝐵 ∧ ∀𝑜 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝑂𝐻𝑜))) |
5 | | oveq2 7239 |
. . . . . . . 8
⊢ (𝑜 = 𝑂 → (𝑂𝐻𝑜) = (𝑂𝐻𝑂)) |
6 | 5 | eleq2d 2824 |
. . . . . . 7
⊢ (𝑜 = 𝑂 → (ℎ ∈ (𝑂𝐻𝑜) ↔ ℎ ∈ (𝑂𝐻𝑂))) |
7 | 6 | eubidv 2586 |
. . . . . 6
⊢ (𝑜 = 𝑂 → (∃!ℎ ℎ ∈ (𝑂𝐻𝑜) ↔ ∃!ℎ ℎ ∈ (𝑂𝐻𝑂))) |
8 | 7 | rspcv 3544 |
. . . . 5
⊢ (𝑂 ∈ 𝐵 → (∀𝑜 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝑂𝐻𝑜) → ∃!ℎ ℎ ∈ (𝑂𝐻𝑂))) |
9 | 8 | adantl 485 |
. . . 4
⊢ (((𝜑 ∧ 𝑂 ∈ (InitO‘𝐶)) ∧ 𝑂 ∈ 𝐵) → (∀𝑜 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝑂𝐻𝑜) → ∃!ℎ ℎ ∈ (𝑂𝐻𝑂))) |
10 | | eusn 4660 |
. . . . 5
⊢
(∃!ℎ ℎ ∈ (𝑂𝐻𝑂) ↔ ∃ℎ(𝑂𝐻𝑂) = {ℎ}) |
11 | | eqid 2738 |
. . . . . . . . 9
⊢
(Id‘𝐶) =
(Id‘𝐶) |
12 | 3 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑂 ∈ (InitO‘𝐶)) ∧ 𝑂 ∈ 𝐵) → 𝐶 ∈ Cat) |
13 | | simpr 488 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑂 ∈ (InitO‘𝐶)) ∧ 𝑂 ∈ 𝐵) → 𝑂 ∈ 𝐵) |
14 | 1, 2, 11, 12, 13 | catidcl 17209 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑂 ∈ (InitO‘𝐶)) ∧ 𝑂 ∈ 𝐵) → ((Id‘𝐶)‘𝑂) ∈ (𝑂𝐻𝑂)) |
15 | | fvex 6748 |
. . . . . . . . . . . . 13
⊢
((Id‘𝐶)‘𝑂) ∈ V |
16 | 15 | elsn 4570 |
. . . . . . . . . . . 12
⊢
(((Id‘𝐶)‘𝑂) ∈ {ℎ} ↔ ((Id‘𝐶)‘𝑂) = ℎ) |
17 | | eqcom 2745 |
. . . . . . . . . . . 12
⊢
(((Id‘𝐶)‘𝑂) = ℎ ↔ ℎ = ((Id‘𝐶)‘𝑂)) |
18 | | sneqbg 4768 |
. . . . . . . . . . . . . 14
⊢ (ℎ ∈ V → ({ℎ} = {((Id‘𝐶)‘𝑂)} ↔ ℎ = ((Id‘𝐶)‘𝑂))) |
19 | 18 | bicomd 226 |
. . . . . . . . . . . . 13
⊢ (ℎ ∈ V → (ℎ = ((Id‘𝐶)‘𝑂) ↔ {ℎ} = {((Id‘𝐶)‘𝑂)})) |
20 | 19 | elv 3426 |
. . . . . . . . . . . 12
⊢ (ℎ = ((Id‘𝐶)‘𝑂) ↔ {ℎ} = {((Id‘𝐶)‘𝑂)}) |
21 | 16, 17, 20 | 3bitri 300 |
. . . . . . . . . . 11
⊢
(((Id‘𝐶)‘𝑂) ∈ {ℎ} ↔ {ℎ} = {((Id‘𝐶)‘𝑂)}) |
22 | 21 | biimpi 219 |
. . . . . . . . . 10
⊢
(((Id‘𝐶)‘𝑂) ∈ {ℎ} → {ℎ} = {((Id‘𝐶)‘𝑂)}) |
23 | 22 | a1i 11 |
. . . . . . . . 9
⊢ ((𝑂𝐻𝑂) = {ℎ} → (((Id‘𝐶)‘𝑂) ∈ {ℎ} → {ℎ} = {((Id‘𝐶)‘𝑂)})) |
24 | | eleq2 2827 |
. . . . . . . . 9
⊢ ((𝑂𝐻𝑂) = {ℎ} → (((Id‘𝐶)‘𝑂) ∈ (𝑂𝐻𝑂) ↔ ((Id‘𝐶)‘𝑂) ∈ {ℎ})) |
25 | | eqeq1 2742 |
. . . . . . . . 9
⊢ ((𝑂𝐻𝑂) = {ℎ} → ((𝑂𝐻𝑂) = {((Id‘𝐶)‘𝑂)} ↔ {ℎ} = {((Id‘𝐶)‘𝑂)})) |
26 | 23, 24, 25 | 3imtr4d 297 |
. . . . . . . 8
⊢ ((𝑂𝐻𝑂) = {ℎ} → (((Id‘𝐶)‘𝑂) ∈ (𝑂𝐻𝑂) → (𝑂𝐻𝑂) = {((Id‘𝐶)‘𝑂)})) |
27 | 14, 26 | syl5 34 |
. . . . . . 7
⊢ ((𝑂𝐻𝑂) = {ℎ} → (((𝜑 ∧ 𝑂 ∈ (InitO‘𝐶)) ∧ 𝑂 ∈ 𝐵) → (𝑂𝐻𝑂) = {((Id‘𝐶)‘𝑂)})) |
28 | 27 | exlimiv 1938 |
. . . . . 6
⊢
(∃ℎ(𝑂𝐻𝑂) = {ℎ} → (((𝜑 ∧ 𝑂 ∈ (InitO‘𝐶)) ∧ 𝑂 ∈ 𝐵) → (𝑂𝐻𝑂) = {((Id‘𝐶)‘𝑂)})) |
29 | 28 | com12 32 |
. . . . 5
⊢ (((𝜑 ∧ 𝑂 ∈ (InitO‘𝐶)) ∧ 𝑂 ∈ 𝐵) → (∃ℎ(𝑂𝐻𝑂) = {ℎ} → (𝑂𝐻𝑂) = {((Id‘𝐶)‘𝑂)})) |
30 | 10, 29 | syl5bi 245 |
. . . 4
⊢ (((𝜑 ∧ 𝑂 ∈ (InitO‘𝐶)) ∧ 𝑂 ∈ 𝐵) → (∃!ℎ ℎ ∈ (𝑂𝐻𝑂) → (𝑂𝐻𝑂) = {((Id‘𝐶)‘𝑂)})) |
31 | 9, 30 | syld 47 |
. . 3
⊢ (((𝜑 ∧ 𝑂 ∈ (InitO‘𝐶)) ∧ 𝑂 ∈ 𝐵) → (∀𝑜 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝑂𝐻𝑜) → (𝑂𝐻𝑂) = {((Id‘𝐶)‘𝑂)})) |
32 | 31 | expimpd 457 |
. 2
⊢ ((𝜑 ∧ 𝑂 ∈ (InitO‘𝐶)) → ((𝑂 ∈ 𝐵 ∧ ∀𝑜 ∈ 𝐵 ∃!ℎ ℎ ∈ (𝑂𝐻𝑜)) → (𝑂𝐻𝑂) = {((Id‘𝐶)‘𝑂)})) |
33 | 4, 32 | mpd 15 |
1
⊢ ((𝜑 ∧ 𝑂 ∈ (InitO‘𝐶)) → (𝑂𝐻𝑂) = {((Id‘𝐶)‘𝑂)}) |