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

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( 𝑋 𝐻 𝑌 ) ⊆ ( 𝑋 𝐽 𝑌 ) )