Proof of Theorem initc
| Step | Hyp | Ref
| Expression |
|---|
| 1 | | simpll 766 |
. . . . . 6
⊢ (((𝐶 ∈ V ∧ ∅ =
(Base‘𝐶)) ∧ 𝑑 ∈ Cat) → 𝐶 ∈ V) |
| 2 | | simplr 768 |
. . . . . 6
⊢ (((𝐶 ∈ V ∧ ∅ =
(Base‘𝐶)) ∧ 𝑑 ∈ Cat) → ∅ =
(Base‘𝐶)) |
| 3 | | simpr 484 |
. . . . . 6
⊢ (((𝐶 ∈ V ∧ ∅ =
(Base‘𝐶)) ∧ 𝑑 ∈ Cat) → 𝑑 ∈ Cat) |
| 4 | 1, 2, 3 | 0funcg 49002 |
. . . . 5
⊢ (((𝐶 ∈ V ∧ ∅ =
(Base‘𝐶)) ∧ 𝑑 ∈ Cat) → (𝐶 Func 𝑑) = {⟨∅,
∅⟩}) |
| 5 | | opex 5432 |
. . . . . 6
⊢
⟨∅, ∅⟩ ∈ V |
| 6 | | sneq 4607 |
. . . . . . 7
⊢ (𝑓 = ⟨∅, ∅⟩
→ {𝑓} =
{⟨∅, ∅⟩}) |
| 7 | 6 | eqeq2d 2741 |
. . . . . 6
⊢ (𝑓 = ⟨∅, ∅⟩
→ ((𝐶 Func 𝑑) = {𝑓} ↔ (𝐶 Func 𝑑) = {⟨∅,
∅⟩})) |
| 8 | 5, 7 | spcev 3581 |
. . . . 5
⊢ ((𝐶 Func 𝑑) = {⟨∅, ∅⟩} →
∃𝑓(𝐶 Func 𝑑) = {𝑓}) |
| 9 | 4, 8 | syl 17 |
. . . 4
⊢ (((𝐶 ∈ V ∧ ∅ =
(Base‘𝐶)) ∧ 𝑑 ∈ Cat) → ∃𝑓(𝐶 Func 𝑑) = {𝑓}) |
| 10 | | eusn 4702 |
. . . 4
⊢
(∃!𝑓 𝑓 ∈ (𝐶 Func 𝑑) ↔ ∃𝑓(𝐶 Func 𝑑) = {𝑓}) |
| 11 | 9, 10 | sylibr 234 |
. . 3
⊢ (((𝐶 ∈ V ∧ ∅ =
(Base‘𝐶)) ∧ 𝑑 ∈ Cat) →
∃!𝑓 𝑓 ∈ (𝐶 Func 𝑑)) |
| 12 | 11 | ralrimiva 3127 |
. 2
⊢ ((𝐶 ∈ V ∧ ∅ =
(Base‘𝐶)) →
∀𝑑 ∈ Cat
∃!𝑓 𝑓 ∈ (𝐶 Func 𝑑)) |
| 13 | | 0cat 17656 |
. . . 4
⊢ ∅
∈ Cat |
| 14 | | oveq2 7402 |
. . . . . . 7
⊢ (𝑑 = ∅ → (𝐶 Func 𝑑) = (𝐶 Func ∅)) |
| 15 | 14 | eleq2d 2815 |
. . . . . 6
⊢ (𝑑 = ∅ → (𝑓 ∈ (𝐶 Func 𝑑) ↔ 𝑓 ∈ (𝐶 Func ∅))) |
| 16 | 15 | eubidv 2580 |
. . . . 5
⊢ (𝑑 = ∅ → (∃!𝑓 𝑓 ∈ (𝐶 Func 𝑑) ↔ ∃!𝑓 𝑓 ∈ (𝐶 Func ∅))) |
| 17 | 16 | rspcv 3593 |
. . . 4
⊢ (∅
∈ Cat → (∀𝑑 ∈ Cat ∃!𝑓 𝑓 ∈ (𝐶 Func 𝑑) → ∃!𝑓 𝑓 ∈ (𝐶 Func ∅))) |
| 18 | 13, 17 | ax-mp 5 |
. . 3
⊢
(∀𝑑 ∈
Cat ∃!𝑓 𝑓 ∈ (𝐶 Func 𝑑) → ∃!𝑓 𝑓 ∈ (𝐶 Func ∅)) |
| 19 | | euex 2571 |
. . 3
⊢
(∃!𝑓 𝑓 ∈ (𝐶 Func ∅) → ∃𝑓 𝑓 ∈ (𝐶 Func ∅)) |
| 20 | | funcrcl 17831 |
. . . . . . 7
⊢ (𝑓 ∈ (𝐶 Func ∅) → (𝐶 ∈ Cat ∧ ∅ ∈
Cat)) |
| 21 | 20 | simpld 494 |
. . . . . 6
⊢ (𝑓 ∈ (𝐶 Func ∅) → 𝐶 ∈ Cat) |
| 22 | 21 | elexd 3479 |
. . . . 5
⊢ (𝑓 ∈ (𝐶 Func ∅) → 𝐶 ∈ V) |
| 23 | | eqid 2730 |
. . . . . . 7
⊢
(Base‘𝐶) =
(Base‘𝐶) |
| 24 | | base0 17190 |
. . . . . . 7
⊢ ∅ =
(Base‘∅) |
| 25 | | eqidd 2731 |
. . . . . . 7
⊢ (𝑓 ∈ (𝐶 Func ∅) → ∅ =
∅) |
| 26 | | id 22 |
. . . . . . 7
⊢ (𝑓 ∈ (𝐶 Func ∅) → 𝑓 ∈ (𝐶 Func ∅)) |
| 27 | 23, 24, 25, 26 | func0g2 49007 |
. . . . . 6
⊢ (𝑓 ∈ (𝐶 Func ∅) → (Base‘𝐶) = ∅) |
| 28 | 27 | eqcomd 2736 |
. . . . 5
⊢ (𝑓 ∈ (𝐶 Func ∅) → ∅ =
(Base‘𝐶)) |
| 29 | 22, 28 | jca 511 |
. . . 4
⊢ (𝑓 ∈ (𝐶 Func ∅) → (𝐶 ∈ V ∧ ∅ = (Base‘𝐶))) |
| 30 | 29 | exlimiv 1930 |
. . 3
⊢
(∃𝑓 𝑓 ∈ (𝐶 Func ∅) → (𝐶 ∈ V ∧ ∅ = (Base‘𝐶))) |
| 31 | 18, 19, 30 | 3syl 18 |
. 2
⊢
(∀𝑑 ∈
Cat ∃!𝑓 𝑓 ∈ (𝐶 Func 𝑑) → (𝐶 ∈ V ∧ ∅ = (Base‘𝐶))) |
| 32 | 12, 31 | impbii 209 |
1
⊢ ((𝐶 ∈ V ∧ ∅ =
(Base‘𝐶)) ↔
∀𝑑 ∈ Cat
∃!𝑓 𝑓 ∈ (𝐶 Func 𝑑)) |
