Step |
Hyp |
Ref |
Expression |
1 |
|
0ssc |
⊢ ( 𝐶 ∈ Cat → ∅ ⊆cat ( Homf ‘ 𝐶 ) ) |
2 |
|
ral0 |
⊢ ∀ 𝑥 ∈ ∅ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 ∅ 𝑥 ) ∧ ∀ 𝑦 ∈ ∅ ∀ 𝑧 ∈ ∅ ∀ 𝑓 ∈ ( 𝑥 ∅ 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ∅ 𝑧 ) ( 𝑔 ( 〈 𝑥 , 𝑦 〉 ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ∅ 𝑧 ) ) |
3 |
2
|
a1i |
⊢ ( 𝐶 ∈ Cat → ∀ 𝑥 ∈ ∅ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 ∅ 𝑥 ) ∧ ∀ 𝑦 ∈ ∅ ∀ 𝑧 ∈ ∅ ∀ 𝑓 ∈ ( 𝑥 ∅ 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ∅ 𝑧 ) ( 𝑔 ( 〈 𝑥 , 𝑦 〉 ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ∅ 𝑧 ) ) ) |
4 |
|
eqid |
⊢ ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐶 ) |
5 |
|
eqid |
⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 ) |
6 |
|
eqid |
⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 ) |
7 |
|
id |
⊢ ( 𝐶 ∈ Cat → 𝐶 ∈ Cat ) |
8 |
|
f0 |
⊢ ∅ : ∅ ⟶ ∅ |
9 |
|
ffn |
⊢ ( ∅ : ∅ ⟶ ∅ → ∅ Fn ∅ ) |
10 |
8 9
|
ax-mp |
⊢ ∅ Fn ∅ |
11 |
|
0xp |
⊢ ( ∅ × ∅ ) = ∅ |
12 |
11
|
fneq2i |
⊢ ( ∅ Fn ( ∅ × ∅ ) ↔ ∅ Fn ∅ ) |
13 |
10 12
|
mpbir |
⊢ ∅ Fn ( ∅ × ∅ ) |
14 |
13
|
a1i |
⊢ ( 𝐶 ∈ Cat → ∅ Fn ( ∅ × ∅ ) ) |
15 |
4 5 6 7 14
|
issubc2 |
⊢ ( 𝐶 ∈ Cat → ( ∅ ∈ ( Subcat ‘ 𝐶 ) ↔ ( ∅ ⊆cat ( Homf ‘ 𝐶 ) ∧ ∀ 𝑥 ∈ ∅ ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 ∅ 𝑥 ) ∧ ∀ 𝑦 ∈ ∅ ∀ 𝑧 ∈ ∅ ∀ 𝑓 ∈ ( 𝑥 ∅ 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ∅ 𝑧 ) ( 𝑔 ( 〈 𝑥 , 𝑦 〉 ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 ∅ 𝑧 ) ) ) ) ) |
16 |
1 3 15
|
mpbir2and |
⊢ ( 𝐶 ∈ Cat → ∅ ∈ ( Subcat ‘ 𝐶 ) ) |