This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem issubc2

Description: Elementhood in the set of subcategories. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypotheses issubc.h ⊢ H = Hom 𝑓 ⁡ C
issubc.i ⊢ 1 ˙ = Id ⁡ C
issubc.o ⊢ · ˙ = comp ⁡ C
issubc.c ⊢ φ → C ∈ Cat
issubc2.a ⊢ φ → J Fn S × S
Assertion issubc2 ⊢ φ → J ∈ Subcat ⁡ C ↔ J ⊆ cat H ∧ ∀ x ∈ S 1 ˙ ⁡ x ∈ x J x ∧ ∀ y ∈ S ∀ z ∈ S ∀ f ∈ x J y ∀ g ∈ y J z g x y · ˙ z f ∈ x J z

Proof

Step Hyp Ref Expression
1 issubc.h ⊢ H = Hom 𝑓 ⁡ C
2 issubc.i ⊢ 1 ˙ = Id ⁡ C
3 issubc.o ⊢ · ˙ = comp ⁡ C
4 issubc.c ⊢ φ → C ∈ Cat
5 issubc2.a ⊢ φ → J Fn S × S
6 5 fndmd ⊢ φ → dom ⁡ J = S × S
7 6 dmeqd ⊢ φ → dom ⁡ dom ⁡ J = dom ⁡ S × S
8 dmxpid ⊢ dom ⁡ S × S = S
9 7 8 eqtr2di ⊢ φ → S = dom ⁡ dom ⁡ J
10 1 2 3 4 9 issubc ⊢ φ → J ∈ Subcat ⁡ C ↔ J ⊆ cat H ∧ ∀ x ∈ S 1 ˙ ⁡ x ∈ x J x ∧ ∀ y ∈ S ∀ z ∈ S ∀ f ∈ x J y ∀ g ∈ y J z g x y · ˙ z f ∈ x J z