Metamath Proof Explorer


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 ( 𝜑𝑆𝑇 )