Metamath Proof Explorer

Theorem subcidcl

Description: The identity of the original category is contained in each subcategory. (Contributed by Mario Carneiro, 4-Jan-2017)

Ref Expression
Hypotheses subcidcl.j ⊢ φ → J ∈ Subcat ⁡ C
subcidcl.2 ⊢ φ → J Fn S × S
subcidcl.x ⊢ φ → X ∈ S
subcidcl.1 ⊢ 1 ˙ = Id ⁡ C
Assertion subcidcl ⊢ φ → 1 ˙ ⁡ X ∈ X J X

Proof

Step Hyp Ref Expression
1 subcidcl.j ⊢ φ → J ∈ Subcat ⁡ C
2 subcidcl.2 ⊢ φ → J Fn S × S
3 subcidcl.x ⊢ φ → X ∈ S
4 subcidcl.1 ⊢ 1 ˙ = Id ⁡ C
5 fveq2 ⊢ x = X → 1 ˙ ⁡ x = 1 ˙ ⁡ X
6 id ⊢ x = X → x = X
7 6 6 oveq12d ⊢ x = X → x J x = X J X
8 5 7 eleq12d ⊢ x = X → 1 ˙ ⁡ x ∈ x J x ↔ 1 ˙ ⁡ X ∈ X J X
9 eqid ⊢ Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ C
10 eqid ⊢ comp ⁡ C = comp ⁡ C
11 subcrcl ⊢ J ∈ Subcat ⁡ C → C ∈ Cat
12 1 11 syl ⊢ φ → C ∈ Cat
13 9 4 10 12 2 issubc2 ⊢ φ → J ∈ Subcat ⁡ C ↔ J ⊆ cat Hom 𝑓 ⁡ C ∧ ∀ x ∈ S 1 ˙ ⁡ x ∈ x J x ∧ ∀ y ∈ S ∀ z ∈ S ∀ f ∈ x J y ∀ g ∈ y J z g x y comp ⁡ C z f ∈ x J z
14 1 13 mpbid ⊢ φ → J ⊆ cat Hom 𝑓 ⁡ C ∧ ∀ x ∈ S 1 ˙ ⁡ x ∈ x J x ∧ ∀ y ∈ S ∀ z ∈ S ∀ f ∈ x J y ∀ g ∈ y J z g x y comp ⁡ C z f ∈ x J z
15 simpl ⊢ 1 ˙ ⁡ x ∈ x J x ∧ ∀ y ∈ S ∀ z ∈ S ∀ f ∈ x J y ∀ g ∈ y J z g x y comp ⁡ C z f ∈ x J z → 1 ˙ ⁡ x ∈ x J x
16 15 ralimi ⊢ ∀ x ∈ S 1 ˙ ⁡ x ∈ x J x ∧ ∀ y ∈ S ∀ z ∈ S ∀ f ∈ x J y ∀ g ∈ y J z g x y comp ⁡ C z f ∈ x J z → ∀ x ∈ S 1 ˙ ⁡ x ∈ x J x
17 14 16 simpl2im ⊢ φ → ∀ x ∈ S 1 ˙ ⁡ x ∈ x J x
18 8 17 3 rspcdva ⊢ φ → 1 ˙ ⁡ X ∈ X J X