funcsetc1o

Description: Value of the functor to the trivial category. The converse is also true because F would be the empty set if C were not a category; and the empty set cannot equal an ordered pair of two sets. (Contributed by Zhi Wang, 22-Oct-2025)

	Ref	Expression
Hypotheses	funcsetc1o.1	⊢ 1 = ( SetCat ‘ 1_o )
	funcsetc1o.f	⊢ 𝐹 = ( ( 1^st ‘ ( 1 Δ_func 𝐶 ) ) ‘ ∅ )
	funcsetc1o.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	funcsetc1o.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	funcsetc1o.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
Assertion	funcsetc1o	⊢ ( 𝜑 → 𝐹 = ⟨ ( 𝐵 × 1_o ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 𝐻 𝑦 ) × 1_o ) ) ⟩ )

Proof

Step	Hyp	Ref	Expression
1		funcsetc1o.1	⊢ 1 = ( SetCat ‘ 1_o )
2		funcsetc1o.f	⊢ 𝐹 = ( ( 1^st ‘ ( 1 Δ_func 𝐶 ) ) ‘ ∅ )
3		funcsetc1o.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
4		funcsetc1o.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
5		funcsetc1o.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
6		eqid	⊢ ( 1 Δ_func 𝐶 ) = ( 1 Δ_func 𝐶 )
7		setc1oterm	⊢ ( SetCat ‘ 1_o ) ∈ TermCat
8	1 7	eqeltri	⊢ 1 ∈ TermCat
9	8	a1i	⊢ ( 𝜑 → 1 ∈ TermCat )
10	9	termccd	⊢ ( 𝜑 → 1 ∈ Cat )
11	1	setc1obas	⊢ 1_o = ( Base ‘ 1 )
12		0lt1o	⊢ ∅ ∈ 1_o
13	12	a1i	⊢ ( 𝜑 → ∅ ∈ 1_o )
14		eqid	⊢ ( Id ‘ 1 ) = ( Id ‘ 1 )
15	6 10 3 11 13 2 4 5 14	diag1a	⊢ ( 𝜑 → 𝐹 = ⟨ ( 𝐵 × { ∅ } ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 𝐻 𝑦 ) × { ( ( Id ‘ 1 ) ‘ ∅ ) } ) ) ⟩ )
16		df1o2	⊢ 1_o = { ∅ }
17	16	xpeq2i	⊢ ( 𝐵 × 1_o ) = ( 𝐵 × { ∅ } )
18	1 14	setc1oid	⊢ ( ( Id ‘ 1 ) ‘ ∅ ) = ∅
19	18	sneqi	⊢ { ( ( Id ‘ 1 ) ‘ ∅ ) } = { ∅ }
20	16 19	eqtr4i	⊢ 1_o = { ( ( Id ‘ 1 ) ‘ ∅ ) }
21	20	xpeq2i	⊢ ( ( 𝑥 𝐻 𝑦 ) × 1_o ) = ( ( 𝑥 𝐻 𝑦 ) × { ( ( Id ‘ 1 ) ‘ ∅ ) } )
22	21	a1i	⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝑥 𝐻 𝑦 ) × 1_o ) = ( ( 𝑥 𝐻 𝑦 ) × { ( ( Id ‘ 1 ) ‘ ∅ ) } ) )
23	22	mpoeq3ia	⊢ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 𝐻 𝑦 ) × 1_o ) ) = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 𝐻 𝑦 ) × { ( ( Id ‘ 1 ) ‘ ∅ ) } ) )
24	17 23	opeq12i	⊢ ⟨ ( 𝐵 × 1_o ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 𝐻 𝑦 ) × 1_o ) ) ⟩ = ⟨ ( 𝐵 × { ∅ } ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 𝐻 𝑦 ) × { ( ( Id ‘ 1 ) ‘ ∅ ) } ) ) ⟩
25	15 24	eqtr4di	⊢ ( 𝜑 → 𝐹 = ⟨ ( 𝐵 × 1_o ) , ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( ( 𝑥 𝐻 𝑦 ) × 1_o ) ) ⟩ )

Metamath Proof Explorer

Theorem funcsetc1o

Proof