Definition df-ssc 17439

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 17441, 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 17436	. 2 class ⊆cat
2		vj	. . . . . . 7 setvar 𝑗
3	2	cv 1538	. . . . . 6 class 𝑗
4		vt	. . . . . . . 8 setvar 𝑡
5	4	cv 1538	. . . . . . 7 class 𝑡
6	5, 5	cxp 5578	. . . . . 6 class (𝑡 × 𝑡)
7	3, 6	wfn 6413	. . . . 5 wff 𝑗 Fn (𝑡 × 𝑡)
8		vh	. . . . . . . 8 setvar ℎ
9	8	cv 1538	. . . . . . 7 class ℎ
10		vx	. . . . . . . 8 setvar 𝑥
11		vs	. . . . . . . . . 10 setvar 𝑠
12	11	cv 1538	. . . . . . . . 9 class 𝑠
13	12, 12	cxp 5578	. . . . . . . 8 class (𝑠 × 𝑠)
14	10	cv 1538	. . . . . . . . . 10 class 𝑥
15	14, 3	cfv 6418	. . . . . . . . 9 class (𝑗‘𝑥)
16	15	cpw 4530	. . . . . . . 8 class 𝒫 (𝑗‘𝑥)
17	10, 13, 16	cixp 8643	. . . . . . 7 class X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝑗‘𝑥)
18	9, 17	wcel 2108	. . . . . 6 wff ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝑗‘𝑥)
19	5	cpw 4530	. . . . . 6 class 𝒫 𝑡
20	18, 11, 19	wrex 3064	. . . . 5 wff ∃𝑠 ∈ 𝒫 𝑡ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝑗‘𝑥)
21	7, 20	wa 395	. . . 4 wff (𝑗 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝑗‘𝑥))
22	21, 4	wex 1783	. . 3 wff ∃𝑡(𝑗 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝑗‘𝑥))
23	22, 8, 2	copab 5132	. 2 class {⟨ℎ, 𝑗⟩ ∣ ∃𝑡(𝑗 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝑗‘𝑥))}
24	1, 23	wceq 1539	1 wff ⊆cat = {⟨ℎ, 𝑗⟩ ∣ ∃𝑡(𝑗 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡ℎ ∈ X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝑗‘𝑥))}

This definition is referenced by:  sscrel  17442  brssc  17443