Theorem ssc2

Description: Infer subset relation on morphisms from the subcategory subset relation. (Contributed by Mario Carneiro, 6-Jan-2017)

	Ref	Expression
Hypotheses	ssc2.1	⊢ ( 𝜑 → 𝐻 Fn ( 𝑆 × 𝑆 ) )
	ssc2.2	⊢ ( 𝜑 → 𝐻 ⊆cat 𝐽 )
	ssc2.3	⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
	ssc2.4	⊢ ( 𝜑 → 𝑌 ∈ 𝑆 )
Assertion	ssc2	⊢ ( 𝜑 → ( 𝑋 𝐻 𝑌 ) ⊆ ( 𝑋 𝐽 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		ssc2.1	⊢ ( 𝜑 → 𝐻 Fn ( 𝑆 × 𝑆 ) )
2		ssc2.2	⊢ ( 𝜑 → 𝐻 ⊆cat 𝐽 )
3		ssc2.3	⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
4		ssc2.4	⊢ ( 𝜑 → 𝑌 ∈ 𝑆 )
5		eqidd	⊢ ( 𝜑 → dom dom 𝐽 = dom dom 𝐽 )
6	2 5	sscfn2	⊢ ( 𝜑 → 𝐽 Fn ( dom dom 𝐽 × dom dom 𝐽 ) )
7		sscrel	⊢ Rel ⊆cat
8	7	brrelex2i	⊢ ( 𝐻 ⊆cat 𝐽 → 𝐽 ∈ V )
9		dmexg	⊢ ( 𝐽 ∈ V → dom 𝐽 ∈ V )
10		dmexg	⊢ ( dom 𝐽 ∈ V → dom dom 𝐽 ∈ V )
11	2 8 9 10	4syl	⊢ ( 𝜑 → dom dom 𝐽 ∈ V )
12	1 6 11	isssc	⊢ ( 𝜑 → ( 𝐻 ⊆cat 𝐽 ↔ ( 𝑆 ⊆ dom dom 𝐽 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 𝐻 𝑦 ) ⊆ ( 𝑥 𝐽 𝑦 ) ) ) )
13	2 12	mpbid	⊢ ( 𝜑 → ( 𝑆 ⊆ dom dom 𝐽 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 𝐻 𝑦 ) ⊆ ( 𝑥 𝐽 𝑦 ) ) )
14	13	simprd	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 𝐻 𝑦 ) ⊆ ( 𝑥 𝐽 𝑦 ) )
15		oveq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 𝐻 𝑦 ) = ( 𝑋 𝐻 𝑦 ) )
16		oveq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 𝐽 𝑦 ) = ( 𝑋 𝐽 𝑦 ) )
17	15 16	sseq12d	⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 𝐻 𝑦 ) ⊆ ( 𝑥 𝐽 𝑦 ) ↔ ( 𝑋 𝐻 𝑦 ) ⊆ ( 𝑋 𝐽 𝑦 ) ) )
18		oveq2	⊢ ( 𝑦 = 𝑌 → ( 𝑋 𝐻 𝑦 ) = ( 𝑋 𝐻 𝑌 ) )
19		oveq2	⊢ ( 𝑦 = 𝑌 → ( 𝑋 𝐽 𝑦 ) = ( 𝑋 𝐽 𝑌 ) )
20	18 19	sseq12d	⊢ ( 𝑦 = 𝑌 → ( ( 𝑋 𝐻 𝑦 ) ⊆ ( 𝑋 𝐽 𝑦 ) ↔ ( 𝑋 𝐻 𝑌 ) ⊆ ( 𝑋 𝐽 𝑌 ) ) )
21	17 20	rspc2va	⊢ ( ( ( 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 𝐻 𝑦 ) ⊆ ( 𝑥 𝐽 𝑦 ) ) → ( 𝑋 𝐻 𝑌 ) ⊆ ( 𝑋 𝐽 𝑌 ) )
22	3 4 14 21	syl21anc	⊢ ( 𝜑 → ( 𝑋 𝐻 𝑌 ) ⊆ ( 𝑋 𝐽 𝑌 ) )