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 ⊢ φ → H Fn S × S
isssc.2 ⊢ φ → J Fn T × T
ssc1.3 ⊢ φ → H ⊆ cat J
Assertion ssc1 ⊢ φ → S ⊆ T

Proof

Step Hyp Ref Expression
1 isssc.1 ⊢ φ → H Fn S × S
2 isssc.2 ⊢ φ → J Fn T × T
3 ssc1.3 ⊢ φ → H ⊆ cat J
4 sscrel ⊢ Rel ⁡ ⊆ cat
5 4 brrelex2i ⊢ H ⊆ cat J → J ∈ V
6 3 5 syl ⊢ φ → J ∈ V
7 2 ssclem ⊢ φ → J ∈ V ↔ T ∈ V
8 6 7 mpbid ⊢ φ → T ∈ V
9 1 2 8 isssc ⊢ φ → H ⊆ cat J ↔ S ⊆ T ∧ ∀ x ∈ S ∀ y ∈ S x H y ⊆ x J y
10 3 9 mpbid ⊢ φ → S ⊆ T ∧ ∀ x ∈ S ∀ y ∈ S x H y ⊆ x J y
11 10 simpld ⊢ φ → S ⊆ T