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 = { ⟨ ℎ , 𝑗 ⟩ ∣ ∃ 𝑡 ( 𝑗 Fn ( 𝑡 × 𝑡 ) ∧ ∃ 𝑠 ∈ 𝒫 𝑡 ℎ ∈ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝑗 ‘ 𝑥 ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cssc	⊢ ⊆cat
1		vh	⊢ ℎ
2		vj	⊢ 𝑗
3		vt	⊢ 𝑡
4	2	cv	⊢ 𝑗
5	3	cv	⊢ 𝑡
6	5 5	cxp	⊢ ( 𝑡 × 𝑡 )
7	4 6	wfn	⊢ 𝑗 Fn ( 𝑡 × 𝑡 )
8		vs	⊢ 𝑠
9	5	cpw	⊢ 𝒫 𝑡
10	1	cv	⊢ ℎ
11		vx	⊢ 𝑥
12	8	cv	⊢ 𝑠
13	12 12	cxp	⊢ ( 𝑠 × 𝑠 )
14	11	cv	⊢ 𝑥
15	14 4	cfv	⊢ ( 𝑗 ‘ 𝑥 )
16	15	cpw	⊢ 𝒫 ( 𝑗 ‘ 𝑥 )
17	11 13 16	cixp	⊢ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝑗 ‘ 𝑥 )
18	10 17	wcel	⊢ ℎ ∈ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝑗 ‘ 𝑥 )
19	18 8 9	wrex	⊢ ∃ 𝑠 ∈ 𝒫 𝑡 ℎ ∈ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝑗 ‘ 𝑥 )
20	7 19	wa	⊢ ( 𝑗 Fn ( 𝑡 × 𝑡 ) ∧ ∃ 𝑠 ∈ 𝒫 𝑡 ℎ ∈ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝑗 ‘ 𝑥 ) )
21	20 3	wex	⊢ ∃ 𝑡 ( 𝑗 Fn ( 𝑡 × 𝑡 ) ∧ ∃ 𝑠 ∈ 𝒫 𝑡 ℎ ∈ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝑗 ‘ 𝑥 ) )
22	21 1 2	copab	⊢ { ⟨ ℎ , 𝑗 ⟩ ∣ ∃ 𝑡 ( 𝑗 Fn ( 𝑡 × 𝑡 ) ∧ ∃ 𝑠 ∈ 𝒫 𝑡 ℎ ∈ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝑗 ‘ 𝑥 ) ) }
23	0 22	wceq	⊢ ⊆cat = { ⟨ ℎ , 𝑗 ⟩ ∣ ∃ 𝑡 ( 𝑗 Fn ( 𝑡 × 𝑡 ) ∧ ∃ 𝑠 ∈ 𝒫 𝑡 ℎ ∈ X 𝑥 ∈ ( 𝑠 × 𝑠 ) 𝒫 ( 𝑗 ‘ 𝑥 ) ) }