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	⊢ ( 𝜑 → 𝐽 ∈ ( Subcat ‘ 𝐶 ) )
	subcidcl.2	⊢ ( 𝜑 → 𝐽 Fn ( 𝑆 × 𝑆 ) )
	subcidcl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
	subcidcl.1	⊢ 1 = ( Id ‘ 𝐶 )
Assertion	subcidcl	⊢ ( 𝜑 → ( 1 ‘ 𝑋 ) ∈ ( 𝑋 𝐽 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		subcidcl.j	⊢ ( 𝜑 → 𝐽 ∈ ( Subcat ‘ 𝐶 ) )
2		subcidcl.2	⊢ ( 𝜑 → 𝐽 Fn ( 𝑆 × 𝑆 ) )
3		subcidcl.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
4		subcidcl.1	⊢ 1 = ( Id ‘ 𝐶 )
5		fveq2	⊢ ( 𝑥 = 𝑋 → ( 1 ‘ 𝑥 ) = ( 1 ‘ 𝑋 ) )
6		id	⊢ ( 𝑥 = 𝑋 → 𝑥 = 𝑋 )
7	6 6	oveq12d	⊢ ( 𝑥 = 𝑋 → ( 𝑥 𝐽 𝑥 ) = ( 𝑋 𝐽 𝑋 ) )
8	5 7	eleq12d	⊢ ( 𝑥 = 𝑋 → ( ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ↔ ( 1 ‘ 𝑋 ) ∈ ( 𝑋 𝐽 𝑋 ) ) )
9		eqid	⊢ ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐶 )
10		eqid	⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
11		subcrcl	⊢ ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) → 𝐶 ∈ Cat )
12	1 11	syl	⊢ ( 𝜑 → 𝐶 ∈ Cat )
13	9 4 10 12 2	issubc2	⊢ ( 𝜑 → ( 𝐽 ∈ ( Subcat ‘ 𝐶 ) ↔ ( 𝐽 ⊆cat ( Homf ‘ 𝐶 ) ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) ) ) )
14	1 13	mpbid	⊢ ( 𝜑 → ( 𝐽 ⊆cat ( Homf ‘ 𝐶 ) ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) ) )
15		simpl	⊢ ( ( ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) → ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) )
16	15	ralimi	⊢ ( ∀ 𝑥 ∈ 𝑆 ( ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 𝐽 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ 𝐶 ) 𝑧 ) 𝑓 ) ∈ ( 𝑥 𝐽 𝑧 ) ) → ∀ 𝑥 ∈ 𝑆 ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) )
17	14 16	simpl2im	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 ( 1 ‘ 𝑥 ) ∈ ( 𝑥 𝐽 𝑥 ) )
18	8 17 3	rspcdva	⊢ ( 𝜑 → ( 1 ‘ 𝑋 ) ∈ ( 𝑋 𝐽 𝑋 ) )