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