MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ssc Structured version   Visualization version   GIF version

Definition df-ssc 16391
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 16393, 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
StepHypRef Expression
1 cssc 16388 . 2 class cat
2 vj . . . . . . 7 setvar 𝑗
32cv 1479 . . . . . 6 class 𝑗
4 vt . . . . . . . 8 setvar 𝑡
54cv 1479 . . . . . . 7 class 𝑡
65, 5cxp 5072 . . . . . 6 class (𝑡 × 𝑡)
73, 6wfn 5842 . . . . 5 wff 𝑗 Fn (𝑡 × 𝑡)
8 vh . . . . . . . 8 setvar
98cv 1479 . . . . . . 7 class
10 vx . . . . . . . 8 setvar 𝑥
11 vs . . . . . . . . . 10 setvar 𝑠
1211cv 1479 . . . . . . . . 9 class 𝑠
1312, 12cxp 5072 . . . . . . . 8 class (𝑠 × 𝑠)
1410cv 1479 . . . . . . . . . 10 class 𝑥
1514, 3cfv 5847 . . . . . . . . 9 class (𝑗𝑥)
1615cpw 4130 . . . . . . . 8 class 𝒫 (𝑗𝑥)
1710, 13, 16cixp 7852 . . . . . . 7 class X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝑗𝑥)
189, 17wcel 1987 . . . . . 6 wff X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝑗𝑥)
195cpw 4130 . . . . . 6 class 𝒫 𝑡
2018, 11, 19wrex 2908 . . . . 5 wff 𝑠 ∈ 𝒫 𝑡X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝑗𝑥)
217, 20wa 384 . . . 4 wff (𝑗 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝑗𝑥))
2221, 4wex 1701 . . 3 wff 𝑡(𝑗 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝑗𝑥))
2322, 8, 2copab 4672 . 2 class {⟨, 𝑗⟩ ∣ ∃𝑡(𝑗 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝑗𝑥))}
241, 23wceq 1480 1 wff cat = {⟨, 𝑗⟩ ∣ ∃𝑡(𝑗 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡X𝑥 ∈ (𝑠 × 𝑠)𝒫 (𝑗𝑥))}
Colors of variables: wff setvar class
This definition is referenced by:  sscrel  16394  brssc  16395
  Copyright terms: Public domain W3C validator