Metamath Proof Explorer

Theorem nelsubc2

Description: An empty "hom-set" for non-empty base is not a subcategory. (Contributed by Zhi Wang, 5-Nov-2025)

Ref Expression
Hypotheses nelsubc.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
nelsubc.s ⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
nelsubc.0 ⊢ ( 𝜑 → 𝑆 ≠ ∅ )
nelsubc.j ⊢ ( 𝜑 → 𝐽 = ( ( 𝑆 × 𝑆 ) × { ∅ } ) )
nelsubc2.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
Assertion nelsubc2 ( 𝜑 → ¬ 𝐽 ∈ ( Subcat ‘ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 nelsubc.b ⊢ 𝐵 = ( Base ‘ 𝐶 )
2 nelsubc.s ⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
3 nelsubc.0 ⊢ ( 𝜑 → 𝑆 ≠ ∅ )
4 nelsubc.j ⊢ ( 𝜑 → 𝐽 = ( ( 𝑆 × 𝑆 ) × { ∅ } ) )
5 nelsubc2.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
6 eqid ⊢ ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐶 )
7 eqid ⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
8 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
9 1 2 3 4 6 7 8 nelsubc ⊢ ( 𝜑 → ( 𝐽 Fn ( 𝑆 × 𝑆 ) ∧ ( 𝐽 ⊆cat ( Homf ‘ 𝐶 ) ∧ ( ¬ ∀ 𝑥 ∈ 𝑆 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) ) ) )
10 9 simprrd ⊢ ( 𝜑 → ( ¬ ∀ 𝑥 ∈ 𝑆 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) )
11 10 simpld ⊢ ( 𝜑 → ¬ ∀ 𝑥 ∈ 𝑆 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) )
12 9 simpld ⊢ ( 𝜑 → 𝐽 Fn ( 𝑆 × 𝑆 ) )
13 6 7 8 5 12 issubc2 ⊢ ( 𝜑 → ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) ↔ ( 𝐽 ⊆cat ( Homf ‘ 𝐶 ) ∧ ∀ 𝑥 ∈ 𝑆 ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) ) ) )
14 13 simplbda ⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( Subcat ‘ 𝐶 ) ) → ∀ 𝑥 ∈ 𝑆 ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) )
15 r19.26 ⊢ ( ∀ 𝑥 ∈ 𝑆 ( ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) ↔ ( ∀ 𝑥 ∈ 𝑆 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) )
16 14 15 sylib ⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( Subcat ‘ 𝐶 ) ) → ( ∀ 𝑥 ∈ 𝑆 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) )
17 16 simpld ⊢ ( ( 𝜑 ∧ 𝐽 ∈ ( Subcat ‘ 𝐶 ) ) → ∀ 𝑥 ∈ 𝑆 ( ( Id ‘ 𝐶 ) ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) )
18 11 17 mtand ⊢ ( 𝜑 → ¬ 𝐽 ∈ ( Subcat ‘ 𝐶 ) )