Definition df-ssc 16470

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 16472, 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.)

Assertion

Ref	Expression
df-ssc	⊢ ⊆cat = {⟨ℎ, 𝑗⟩ ∣ ∃𝑡(𝑗 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝑗‘𝑥))}

Distinct variable group:   ℎ,𝑗,𝑠,𝑡,𝑥

Detailed syntax breakdown of Definition df-ssc

Step	Hyp	Ref	Expression
1		cssc 16467	. 2 class ⊆cat
2		vj	. . . . . . 7 setvar 𝑗
3	2	cv 1482	. . . . . 6 class 𝑗
4		vt	. . . . . . . 8 setvar 𝑡
5	4	cv 1482	. . . . . . 7 class 𝑡
6	5, 5	cxp 5112	. . . . . 6 class (𝑡 × 𝑡)
7	3, 6	wfn 5883	. . . . 5 wff 𝑗 Fn (𝑡 × 𝑡)
8		vh	. . . . . . . 8 setvar ℎ
9	8	cv 1482	. . . . . . 7 class ℎ
10		vx	. . . . . . . 8 setvar 𝑥
11		vs	. . . . . . . . . 10 setvar 𝑠
12	11	cv 1482	. . . . . . . . 9 class 𝑠
13	12, 12	cxp 5112	. . . . . . . 8 class (𝑠 × 𝑠)
14	10	cv 1482	. . . . . . . . . 10 class 𝑥
15	14, 3	cfv 5888	. . . . . . . . 9 class (𝑗‘𝑥)
16	15	cpw 4158	. . . . . . . 8 class 𝒫 (𝑗‘𝑥)
17	10, 13, 16	cixp 7908	. . . . . . 7 class X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝑗‘𝑥)
18	9, 17	wcel 1990	. . . . . 6 wff ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝑗‘𝑥)
19	5	cpw 4158	. . . . . 6 class 𝒫 𝑡
20	18, 11, 19	wrex 2913	. . . . 5 wff ∃𝑠 ∈ 𝒫 𝑡ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝑗‘𝑥)
21	7, 20	wa 384	. . . 4 wff (𝑗 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝑗‘𝑥))
22	21, 4	wex 1704	. . 3 wff ∃𝑡(𝑗 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝑗‘𝑥))
23	22, 8, 2	copab 4712	. 2 class {⟨ℎ, 𝑗⟩ ∣ ∃𝑡(𝑗 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝑗‘𝑥))}
24	1, 23	wceq 1483	1 wff ⊆cat = {⟨ℎ, 𝑗⟩ ∣ ∃𝑡(𝑗 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝑗‘𝑥))}

This definition is referenced by:  sscrel  16473  brssc  16474