Metamath Proof Explorer

Theorem ssctr

Description: The subcategory subset relation is transitive. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Assertion ssctr ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐶 ) → 𝐴 ⊆cat 𝐶 )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐶 ) → 𝐴 ⊆cat 𝐵 )
2 eqidd ⊢ ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐶 ) → dom dom 𝐴 = dom dom 𝐴 )
3 1 2 sscfn1 ⊢ ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐶 ) → 𝐴 Fn ( dom dom 𝐴 × dom dom 𝐴 ) )
4 eqidd ⊢ ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐶 ) → dom dom 𝐵 = dom dom 𝐵 )
5 1 4 sscfn2 ⊢ ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐶 ) → 𝐵 Fn ( dom dom 𝐵 × dom dom 𝐵 ) )
6 3 5 1 ssc1 ⊢ ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐶 ) → dom dom 𝐴 ⊆ dom dom 𝐵 )
7 simpr ⊢ ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐶 ) → 𝐵 ⊆cat 𝐶 )
8 eqidd ⊢ ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐶 ) → dom dom 𝐶 = dom dom 𝐶 )
9 7 8 sscfn2 ⊢ ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐶 ) → 𝐶 Fn ( dom dom 𝐶 × dom dom 𝐶 ) )
10 5 9 7 ssc1 ⊢ ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐶 ) → dom dom 𝐵 ⊆ dom dom 𝐶 )
11 6 10 sstrd ⊢ ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐶 ) → dom dom 𝐴 ⊆ dom dom 𝐶 )
12 3 adantr ⊢ ( ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐶 ) ∧ ( 𝑥 ∈ dom dom 𝐴 ∧ 𝑦 ∈ dom dom 𝐴 ) ) → 𝐴 Fn ( dom dom 𝐴 × dom dom 𝐴 ) )
13 1 adantr ⊢ ( ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐶 ) ∧ ( 𝑥 ∈ dom dom 𝐴 ∧ 𝑦 ∈ dom dom 𝐴 ) ) → 𝐴 ⊆cat 𝐵 )
14 simprl ⊢ ( ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐶 ) ∧ ( 𝑥 ∈ dom dom 𝐴 ∧ 𝑦 ∈ dom dom 𝐴 ) ) → 𝑥 ∈ dom dom 𝐴 )
15 simprr ⊢ ( ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐶 ) ∧ ( 𝑥 ∈ dom dom 𝐴 ∧ 𝑦 ∈ dom dom 𝐴 ) ) → 𝑦 ∈ dom dom 𝐴 )
16 12 13 14 15 ssc2 ⊢ ( ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐶 ) ∧ ( 𝑥 ∈ dom dom 𝐴 ∧ 𝑦 ∈ dom dom 𝐴 ) ) → ( 𝑥 𝐴 𝑦 ) ⊆ ( 𝑥 𝐵 𝑦 ) )
17 5 adantr ⊢ ( ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐶 ) ∧ ( 𝑥 ∈ dom dom 𝐴 ∧ 𝑦 ∈ dom dom 𝐴 ) ) → 𝐵 Fn ( dom dom 𝐵 × dom dom 𝐵 ) )
18 7 adantr ⊢ ( ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐶 ) ∧ ( 𝑥 ∈ dom dom 𝐴 ∧ 𝑦 ∈ dom dom 𝐴 ) ) → 𝐵 ⊆cat 𝐶 )
19 6 adantr ⊢ ( ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐶 ) ∧ ( 𝑥 ∈ dom dom 𝐴 ∧ 𝑦 ∈ dom dom 𝐴 ) ) → dom dom 𝐴 ⊆ dom dom 𝐵 )
20 19 14 sseldd ⊢ ( ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐶 ) ∧ ( 𝑥 ∈ dom dom 𝐴 ∧ 𝑦 ∈ dom dom 𝐴 ) ) → 𝑥 ∈ dom dom 𝐵 )
21 19 15 sseldd ⊢ ( ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐶 ) ∧ ( 𝑥 ∈ dom dom 𝐴 ∧ 𝑦 ∈ dom dom 𝐴 ) ) → 𝑦 ∈ dom dom 𝐵 )
22 17 18 20 21 ssc2 ⊢ ( ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐶 ) ∧ ( 𝑥 ∈ dom dom 𝐴 ∧ 𝑦 ∈ dom dom 𝐴 ) ) → ( 𝑥 𝐵 𝑦 ) ⊆ ( 𝑥 𝐶 𝑦 ) )
23 16 22 sstrd ⊢ ( ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐶 ) ∧ ( 𝑥 ∈ dom dom 𝐴 ∧ 𝑦 ∈ dom dom 𝐴 ) ) → ( 𝑥 𝐴 𝑦 ) ⊆ ( 𝑥 𝐶 𝑦 ) )
24 23 ralrimivva ⊢ ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐶 ) → ∀ 𝑥 ∈ dom dom 𝐴 ∀ 𝑦 ∈ dom dom 𝐴 ( 𝑥 𝐴 𝑦 ) ⊆ ( 𝑥 𝐶 𝑦 ) )
25 sscrel ⊢ Rel ⊆cat
26 25 brrelex2i ⊢ ( 𝐵 ⊆cat 𝐶 → 𝐶 ∈ V )
27 26 adantl ⊢ ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐶 ) → 𝐶 ∈ V )
28 dmexg ⊢ ( 𝐶 ∈ V → dom 𝐶 ∈ V )
29 dmexg ⊢ ( dom 𝐶 ∈ V → dom dom 𝐶 ∈ V )
30 27 28 29 3syl ⊢ ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐶 ) → dom dom 𝐶 ∈ V )
31 3 9 30 isssc ⊢ ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐶 ) → ( 𝐴 ⊆cat 𝐶 ↔ ( dom dom 𝐴 ⊆ dom dom 𝐶 ∧ ∀ 𝑥 ∈ dom dom 𝐴 ∀ 𝑦 ∈ dom dom 𝐴 ( 𝑥 𝐴 𝑦 ) ⊆ ( 𝑥 𝐶 𝑦 ) ) ) )
32 11 24 31 mpbir2and ⊢ ( ( 𝐴 ⊆cat 𝐵 ∧ 𝐵 ⊆cat 𝐶 ) → 𝐴 ⊆cat 𝐶 )