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

Metamath Proof Explorer

Definition df-ssc

Description: Define the subset relation for subcategories. Despite the name, this is not really a "category-aware" definition, which is to say it makes no explicit references to homsets or composition; instead this is a subset-like relation on the functions that are used as subcategory specifications in df-subc , which makes it play an analogous role to the subset relation applied to the subgroups of a group. (Contributed by Mario Carneiro, 6-Jan-2017)

Ref Expression
Assertion df-ssc ⊢ ⊆ cat = h j | ∃ t j Fn t × t ∧ ∃ s ∈ 𝒫 t h ∈ ⨉ x ∈ s × s 𝒫 j ⁡ x

Detailed syntax breakdown

Step Hyp Ref Expression
0 cssc class ⊆ cat
1 vh setvar h
2 vj setvar j
3 vt setvar t
4 2 cv setvar j
5 3 cv setvar t
6 5 5 cxp class t × t
7 4 6 wfn wff j Fn t × t
8 vs setvar s
9 5 cpw class 𝒫 t
10 1 cv setvar h
11 vx setvar x
12 8 cv setvar s
13 12 12 cxp class s × s
14 11 cv setvar x
15 14 4 cfv class j ⁡ x
16 15 cpw class 𝒫 j ⁡ x
17 11 13 16 cixp class ⨉ x ∈ s × s 𝒫 j ⁡ x
18 10 17 wcel wff h ∈ ⨉ x ∈ s × s 𝒫 j ⁡ x
19 18 8 9 wrex wff ∃ s ∈ 𝒫 t h ∈ ⨉ x ∈ s × s 𝒫 j ⁡ x
20 7 19 wa wff j Fn t × t ∧ ∃ s ∈ 𝒫 t h ∈ ⨉ x ∈ s × s 𝒫 j ⁡ x
21 20 3 wex wff ∃ t j Fn t × t ∧ ∃ s ∈ 𝒫 t h ∈ ⨉ x ∈ s × s 𝒫 j ⁡ x
22 21 1 2 copab class h j | ∃ t j Fn t × t ∧ ∃ s ∈ 𝒫 t h ∈ ⨉ x ∈ s × s 𝒫 j ⁡ x
23 0 22 wceq wff ⊆ cat = h j | ∃ t j Fn t × t ∧ ∃ s ∈ 𝒫 t h ∈ ⨉ x ∈ s × s 𝒫 j ⁡ x