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

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