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	⊢ 𝐶 = ( SetCat ‘ 1_o )
	par2diag.e	⊢ 𝐸 = { ⟨ ( Base ‘ ndx ) , 2_o ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑝 ∈ ( 2_o × 2_o ) , 𝑞 ∈ 2_o ↦ ( 𝑟 ∈ 3_o , 𝑠 ∈ 3_o ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ }
	par2diag.l	⊢ 𝐿 = ( 𝐸 Δ_func 𝐶 )
	par2diag.f	⊢ 𝐹 = ( ( 1^st ‘ 𝐿 ) ‘ ∅ )
	par2diag.g	⊢ 𝐺 = ( ( 1^st ‘ 𝐿 ) ‘ 1_o )
	par2diag.a	⊢ 𝐴 = ( 1_o × { ∅ } )
Assertion	par2diag	⊢ ( ( 𝐹 ∈ ( 𝐶 Func 𝐸 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐸 ) ) ∧ ( 𝐴 ∈ ( 𝐹 ( 𝐶 Nat 𝐸 ) 𝐺 ) ∧ ( 𝐴 ‘ ∅ ) = ∅ ) ∧ ( ( ( 1^st ‘ 𝐹 ) ‘ ∅ ) = ∅ ∧ ( ( 1^st ‘ 𝐺 ) ‘ ∅ ) = 1_o ) )

Proof

Step	Hyp	Ref	Expression
1		par2diag.c	⊢ 𝐶 = ( SetCat ‘ 1_o )
2		par2diag.e	⊢ 𝐸 = { ⟨ ( Base ‘ ndx ) , 2_o ⟩ , ⟨ ( Hom ‘ ndx ) , ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) ) ⟩ , ⟨ ( comp ‘ ndx ) , ( 𝑝 ∈ ( 2_o × 2_o ) , 𝑞 ∈ 2_o ↦ ( 𝑟 ∈ 3_o , 𝑠 ∈ 3_o ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ }
3		par2diag.l	⊢ 𝐿 = ( 𝐸 Δ_func 𝐶 )
4		par2diag.f	⊢ 𝐹 = ( ( 1^st ‘ 𝐿 ) ‘ ∅ )
5		par2diag.g	⊢ 𝐺 = ( ( 1^st ‘ 𝐿 ) ‘ 1_o )
6		par2diag.a	⊢ 𝐴 = ( 1_o × { ∅ } )
7	2	par2catid	⊢ ( 𝐸 ∈ Cat ∧ ( Id ‘ 𝐸 ) = ( 𝑦 ∈ 2_o ↦ 2_o ) )
8	7	simpli	⊢ 𝐸 ∈ Cat
9	8	a1i	⊢ ( ⊤ → 𝐸 ∈ Cat )
10		setc1oterm	⊢ ( SetCat ‘ 1_o ) ∈ TermCat
11	1 10	eqeltri	⊢ 𝐶 ∈ TermCat
12	11	a1i	⊢ ( ⊤ → 𝐶 ∈ TermCat )
13	12	termccatd	⊢ ( ⊤ → 𝐶 ∈ Cat )
14	2	par2str	⊢ ( 2_o = ( Base ‘ 𝐸 ) ∧ ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) ) = ( Hom ‘ 𝐸 ) ∧ ( 𝑝 ∈ ( 2_o × 2_o ) , 𝑞 ∈ 2_o ↦ ( 𝑟 ∈ 3_o , 𝑠 ∈ 3_o ↦ ( 𝑟 ∩ 𝑠 ) ) ) = ( comp ‘ 𝐸 ) )
15	14	simp1i	⊢ 2_o = ( Base ‘ 𝐸 )
16		0ex	⊢ ∅ ∈ V
17	16	prid1	⊢ ∅ ∈ { ∅ , 1_o }
18		df2o3	⊢ 2_o = { ∅ , 1_o }
19	17 18	eleqtrri	⊢ ∅ ∈ 2_o
20	19	a1i	⊢ ( ⊤ → ∅ ∈ 2_o )
21	3 9 13 15 20 4	diag1cl	⊢ ( ⊤ → 𝐹 ∈ ( 𝐶 Func 𝐸 ) )
22		1oelpr	⊢ 1_o ∈ { ∅ , 1_o }
23	22 18	eleqtrri	⊢ 1_o ∈ 2_o
24	23	a1i	⊢ ( ⊤ → 1_o ∈ 2_o )
25	3 9 13 15 24 5	diag1cl	⊢ ( ⊤ → 𝐺 ∈ ( 𝐶 Func 𝐸 ) )
26	21 25	jca	⊢ ( ⊤ → ( 𝐹 ∈ ( 𝐶 Func 𝐸 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐸 ) ) )
27	1	setc1obas	⊢ 1_o = ( Base ‘ 𝐶 )
28	14	simp2i	⊢ ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) ) = ( Hom ‘ 𝐸 )
29		eqid	⊢ ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) ) = ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) )
30	29	par2hom	⊢ ( ( ∅ ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) ) ∅ ) = { 2_o } ∧ ( 1_o ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) ) 1_o ) = { 2_o } ∧ ( ( ∅ ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) ) 1_o ) = 2_o ∧ ( 1_o ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) ) ∅ ) = ∅ ) )
31	30	simp3i	⊢ ( ( ∅ ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) ) 1_o ) = 2_o ∧ ( 1_o ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) ) ∅ ) = ∅ )
32	31	simpli	⊢ ( ∅ ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) ) 1_o ) = 2_o
33	19 32	eleqtrri	⊢ ∅ ∈ ( ∅ ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) ) 1_o )
34	33	a1i	⊢ ( ⊤ → ∅ ∈ ( ∅ ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) ) 1_o ) )
35		eqid	⊢ ( 𝐶 Nat 𝐸 ) = ( 𝐶 Nat 𝐸 )
36	3 15 27 28 9 13 20 24 34 35	diag2cl	⊢ ( ⊤ → ( 1_o × { ∅ } ) ∈ ( ( ( 1^st ‘ 𝐿 ) ‘ ∅ ) ( 𝐶 Nat 𝐸 ) ( ( 1^st ‘ 𝐿 ) ‘ 1_o ) ) )
37	4 5	oveq12i	⊢ ( 𝐹 ( 𝐶 Nat 𝐸 ) 𝐺 ) = ( ( ( 1^st ‘ 𝐿 ) ‘ ∅ ) ( 𝐶 Nat 𝐸 ) ( ( 1^st ‘ 𝐿 ) ‘ 1_o ) )
38	36 6 37	3eltr4g	⊢ ( ⊤ → 𝐴 ∈ ( 𝐹 ( 𝐶 Nat 𝐸 ) 𝐺 ) )
39	6	fveq1i	⊢ ( 𝐴 ‘ ∅ ) = ( ( 1_o × { ∅ } ) ‘ ∅ )
40		0lt1o	⊢ ∅ ∈ 1_o
41	16	fvconst2	⊢ ( ∅ ∈ 1_o → ( ( 1_o × { ∅ } ) ‘ ∅ ) = ∅ )
42	40 41	ax-mp	⊢ ( ( 1_o × { ∅ } ) ‘ ∅ ) = ∅
43	39 42	eqtri	⊢ ( 𝐴 ‘ ∅ ) = ∅
44	38 43	jctir	⊢ ( ⊤ → ( 𝐴 ∈ ( 𝐹 ( 𝐶 Nat 𝐸 ) 𝐺 ) ∧ ( 𝐴 ‘ ∅ ) = ∅ ) )
45	40	a1i	⊢ ( ⊤ → ∅ ∈ 1_o )
46	3 9 13 15 20 4 27 45	diag11	⊢ ( ⊤ → ( ( 1^st ‘ 𝐹 ) ‘ ∅ ) = ∅ )
47	3 9 13 15 24 5 27 45	diag11	⊢ ( ⊤ → ( ( 1^st ‘ 𝐺 ) ‘ ∅ ) = 1_o )
48	46 47	jca	⊢ ( ⊤ → ( ( ( 1^st ‘ 𝐹 ) ‘ ∅ ) = ∅ ∧ ( ( 1^st ‘ 𝐺 ) ‘ ∅ ) = 1_o ) )
49	26 44 48	3jca	⊢ ( ⊤ → ( ( 𝐹 ∈ ( 𝐶 Func 𝐸 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐸 ) ) ∧ ( 𝐴 ∈ ( 𝐹 ( 𝐶 Nat 𝐸 ) 𝐺 ) ∧ ( 𝐴 ‘ ∅ ) = ∅ ) ∧ ( ( ( 1^st ‘ 𝐹 ) ‘ ∅ ) = ∅ ∧ ( ( 1^st ‘ 𝐺 ) ‘ ∅ ) = 1_o ) ) )
50	49	mptru	⊢ ( ( 𝐹 ∈ ( 𝐶 Func 𝐸 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐸 ) ) ∧ ( 𝐴 ∈ ( 𝐹 ( 𝐶 Nat 𝐸 ) 𝐺 ) ∧ ( 𝐴 ‘ ∅ ) = ∅ ) ∧ ( ( ( 1^st ‘ 𝐹 ) ‘ ∅ ) = ∅ ∧ ( ( 1^st ‘ 𝐺 ) ‘ ∅ ) = 1_o ) )

Metamath Proof Explorer

Theorem par2diag

Proof