Metamath Proof Explorer

Theorem par2diag

Description: Two constant functors into the concrete parallel-arrow category and a natural transformation whose component is the empty-set arrow. (Contributed by Zhi Wang, 14-Sep-2026)

Ref Expression
Hypotheses par2diag.c ⊢ C = SetCat ⁡ 1 𝑜
par2diag.e ⊢ E = Base ndx 2 𝑜 Hom ⁡ ndx m ∈ 2 𝑜 , n ∈ 2 𝑜 ⟼ if m = n 2 𝑜 if m = ∅ ∧ n = 1 𝑜 2 𝑜 ∅ comp ⁡ ndx p ∈ 2 𝑜 × 2 𝑜 , q ∈ 2 𝑜 ⟼ r ∈ 3 𝑜 , s ∈ 3 𝑜 ⟼ r ∩ s
par2diag.l ⊢ L = E Δ func C
par2diag.f ⊢ F = 1 st ⁡ L ⁡ ∅
par2diag.g ⊢ G = 1 st ⁡ L ⁡ 1 𝑜
par2diag.a ⊢ A = 1 𝑜 × ∅
Assertion par2diag ⊢ F ∈ C Func E ∧ G ∈ C Func E ∧ A ∈ F C Nat E G ∧ A ⁡ ∅ = ∅ ∧ 1 st ⁡ F ⁡ ∅ = ∅ ∧ 1 st ⁡ G ⁡ ∅ = 1 𝑜

Proof

Step Hyp Ref Expression
1 par2diag.c ⊢ C = SetCat ⁡ 1 𝑜
2 par2diag.e ⊢ E = Base ndx 2 𝑜 Hom ⁡ ndx m ∈ 2 𝑜 , n ∈ 2 𝑜 ⟼ if m = n 2 𝑜 if m = ∅ ∧ n = 1 𝑜 2 𝑜 ∅ comp ⁡ ndx p ∈ 2 𝑜 × 2 𝑜 , q ∈ 2 𝑜 ⟼ r ∈ 3 𝑜 , s ∈ 3 𝑜 ⟼ r ∩ s
3 par2diag.l ⊢ L = E Δ func C
4 par2diag.f ⊢ F = 1 st ⁡ L ⁡ ∅
5 par2diag.g ⊢ G = 1 st ⁡ L ⁡ 1 𝑜
6 par2diag.a ⊢ A = 1 𝑜 × ∅
7 2 par2catid ⊢ E ∈ Cat ∧ Id ⁡ E = y ∈ 2 𝑜 ⟼ 2 𝑜
8 7 simpli ⊢ E ∈ Cat
9 8 a1i ⊢ ⊤ → E ∈ Cat
10 setc1oterm Could not format ( SetCat ` 1o ) e. TermCat : No typesetting found for |- ( SetCat ` 1o ) e. TermCat with typecode |-
11 1 10 eqeltri Could not format C e. TermCat : No typesetting found for |- C e. TermCat with typecode |-
12 11 a1i Could not format ( T. -> C e. TermCat ) : No typesetting found for |- ( T. -> C e. TermCat ) with typecode |-
13 12 termccatd ⊢ ⊤ → C ∈ Cat
14 2 par2str ⊢ 2 𝑜 = Base E ∧ m ∈ 2 𝑜 , n ∈ 2 𝑜 ⟼ if m = n 2 𝑜 if m = ∅ ∧ n = 1 𝑜 2 𝑜 ∅ = Hom ⁡ E ∧ p ∈ 2 𝑜 × 2 𝑜 , q ∈ 2 𝑜 ⟼ r ∈ 3 𝑜 , s ∈ 3 𝑜 ⟼ r ∩ s = comp ⁡ E
15 14 simp1i ⊢ 2 𝑜 = Base E
16 0ex ⊢ ∅ ∈ V
17 16 prid1 ⊢ ∅ ∈ ∅ 1 𝑜
18 df2o3 ⊢ 2 𝑜 = ∅ 1 𝑜
19 17 18 eleqtrri ⊢ ∅ ∈ 2 𝑜
20 19 a1i ⊢ ⊤ → ∅ ∈ 2 𝑜
21 3 9 13 15 20 4 diag1cl ⊢ ⊤ → F ∈ C Func E
22 1oelpr ⊢ 1 𝑜 ∈ ∅ 1 𝑜
23 22 18 eleqtrri ⊢ 1 𝑜 ∈ 2 𝑜
24 23 a1i ⊢ ⊤ → 1 𝑜 ∈ 2 𝑜
25 3 9 13 15 24 5 diag1cl ⊢ ⊤ → G ∈ C Func E
26 21 25 jca ⊢ ⊤ → F ∈ C Func E ∧ G ∈ C Func E
27 1 setc1obas ⊢ 1 𝑜 = Base C
28 14 simp2i ⊢ m ∈ 2 𝑜 , n ∈ 2 𝑜 ⟼ if m = n 2 𝑜 if m = ∅ ∧ n = 1 𝑜 2 𝑜 ∅ = Hom ⁡ E
29 eqid ⊢ m ∈ 2 𝑜 , n ∈ 2 𝑜 ⟼ if m = n 2 𝑜 if m = ∅ ∧ n = 1 𝑜 2 𝑜 ∅ = m ∈ 2 𝑜 , n ∈ 2 𝑜 ⟼ if m = n 2 𝑜 if m = ∅ ∧ n = 1 𝑜 2 𝑜 ∅
30 29 par2hom ⊢ ∅ m ∈ 2 𝑜 , n ∈ 2 𝑜 ⟼ if m = n 2 𝑜 if m = ∅ ∧ n = 1 𝑜 2 𝑜 ∅ ∅ = 2 𝑜 ∧ 1 𝑜 m ∈ 2 𝑜 , n ∈ 2 𝑜 ⟼ if m = n 2 𝑜 if m = ∅ ∧ n = 1 𝑜 2 𝑜 ∅ 1 𝑜 = 2 𝑜 ∧ ∅ m ∈ 2 𝑜 , n ∈ 2 𝑜 ⟼ if m = n 2 𝑜 if m = ∅ ∧ n = 1 𝑜 2 𝑜 ∅ 1 𝑜 = 2 𝑜 ∧ 1 𝑜 m ∈ 2 𝑜 , n ∈ 2 𝑜 ⟼ if m = n 2 𝑜 if m = ∅ ∧ n = 1 𝑜 2 𝑜 ∅ ∅ = ∅
31 30 simp3i ⊢ ∅ m ∈ 2 𝑜 , n ∈ 2 𝑜 ⟼ if m = n 2 𝑜 if m = ∅ ∧ n = 1 𝑜 2 𝑜 ∅ 1 𝑜 = 2 𝑜 ∧ 1 𝑜 m ∈ 2 𝑜 , n ∈ 2 𝑜 ⟼ if m = n 2 𝑜 if m = ∅ ∧ n = 1 𝑜 2 𝑜 ∅ ∅ = ∅
32 31 simpli ⊢ ∅ m ∈ 2 𝑜 , n ∈ 2 𝑜 ⟼ if m = n 2 𝑜 if m = ∅ ∧ n = 1 𝑜 2 𝑜 ∅ 1 𝑜 = 2 𝑜
33 19 32 eleqtrri ⊢ ∅ ∈ ∅ m ∈ 2 𝑜 , n ∈ 2 𝑜 ⟼ if m = n 2 𝑜 if m = ∅ ∧ n = 1 𝑜 2 𝑜 ∅ 1 𝑜
34 33 a1i ⊢ ⊤ → ∅ ∈ ∅ m ∈ 2 𝑜 , n ∈ 2 𝑜 ⟼ if m = n 2 𝑜 if m = ∅ ∧ n = 1 𝑜 2 𝑜 ∅ 1 𝑜
35 eqid ⊢ C Nat E = C Nat E
36 3 15 27 28 9 13 20 24 34 35 diag2cl ⊢ ⊤ → 1 𝑜 × ∅ ∈ 1 st ⁡ L ⁡ ∅ C Nat E 1 st ⁡ L ⁡ 1 𝑜
37 4 5 oveq12i ⊢ F C Nat E G = 1 st ⁡ L ⁡ ∅ C Nat E 1 st ⁡ L ⁡ 1 𝑜
38 36 6 37 3eltr4g ⊢ ⊤ → A ∈ F C Nat E G
39 6 fveq1i ⊢ A ⁡ ∅ = 1 𝑜 × ∅ ⁡ ∅
40 0lt1o ⊢ ∅ ∈ 1 𝑜
41 16 fvconst2 ⊢ ∅ ∈ 1 𝑜 → 1 𝑜 × ∅ ⁡ ∅ = ∅
42 40 41 ax-mp ⊢ 1 𝑜 × ∅ ⁡ ∅ = ∅
43 39 42 eqtri ⊢ A ⁡ ∅ = ∅
44 38 43 jctir ⊢ ⊤ → A ∈ F C Nat E G ∧ A ⁡ ∅ = ∅
45 40 a1i ⊢ ⊤ → ∅ ∈ 1 𝑜
46 3 9 13 15 20 4 27 45 diag11 ⊢ ⊤ → 1 st ⁡ F ⁡ ∅ = ∅
47 3 9 13 15 24 5 27 45 diag11 ⊢ ⊤ → 1 st ⁡ G ⁡ ∅ = 1 𝑜
48 46 47 jca ⊢ ⊤ → 1 st ⁡ F ⁡ ∅ = ∅ ∧ 1 st ⁡ G ⁡ ∅ = 1 𝑜
49 26 44 48 3jca ⊢ ⊤ → F ∈ C Func E ∧ G ∈ C Func E ∧ A ∈ F C Nat E G ∧ A ⁡ ∅ = ∅ ∧ 1 st ⁡ F ⁡ ∅ = ∅ ∧ 1 st ⁡ G ⁡ ∅ = 1 𝑜
50 49 mptru ⊢ F ∈ C Func E ∧ G ∈ C Func E ∧ A ∈ F C Nat E G ∧ A ⁡ ∅ = ∅ ∧ 1 st ⁡ F ⁡ ∅ = ∅ ∧ 1 st ⁡ G ⁡ ∅ = 1 𝑜