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

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 ⊢ ( 𝜑 → 𝐽 ∈ ( 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 ‘ 𝑋 ) ∈ ( 𝑋 𝐽 𝑋 ) )