Theorem ssc1

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

	Ref	Expression
Hypotheses	isssc.1	⊢ ( 𝜑 → 𝐻 Fn ( 𝑆 × 𝑆 ) )
	isssc.2	⊢ ( 𝜑 → 𝐽 Fn ( 𝑇 × 𝑇 ) )
	ssc1.3	⊢ ( 𝜑 → 𝐻 ⊆cat 𝐽 )
Assertion	ssc1	⊢ ( 𝜑 → 𝑆 ⊆ 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		isssc.1	⊢ ( 𝜑 → 𝐻 Fn ( 𝑆 × 𝑆 ) )
2		isssc.2	⊢ ( 𝜑 → 𝐽 Fn ( 𝑇 × 𝑇 ) )
3		ssc1.3	⊢ ( 𝜑 → 𝐻 ⊆cat 𝐽 )
4		sscrel	⊢ Rel ⊆cat
5	4	brrelex2i	⊢ ( 𝐻 ⊆cat 𝐽 → 𝐽 ∈ V )
6	3 5	syl	⊢ ( 𝜑 → 𝐽 ∈ V )
7	2	ssclem	⊢ ( 𝜑 → ( 𝐽 ∈ V ↔ 𝑇 ∈ V ) )
8	6 7	mpbid	⊢ ( 𝜑 → 𝑇 ∈ V )
9	1 2 8	isssc	⊢ ( 𝜑 → ( 𝐻 ⊆cat 𝐽 ↔ ( 𝑆 ⊆ 𝑇 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 𝐻 𝑦 ) ⊆ ( 𝑥 𝐽 𝑦 ) ) ) )
10	3 9	mpbid	⊢ ( 𝜑 → ( 𝑆 ⊆ 𝑇 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 𝐻 𝑦 ) ⊆ ( 𝑥 𝐽 𝑦 ) ) )
11	10	simpld	⊢ ( 𝜑 → 𝑆 ⊆ 𝑇 )