isinito2lem

Description: The predicate "is an initial object" of a category, using universal property. (Contributed by Zhi Wang, 23-Oct-2025)

	Ref	Expression
Hypotheses	isinito2.1	⊢ 1 = ( SetCat ‘ 1_o )
	isinito2.f	⊢ 𝐹 = ( ( 1^st ‘ ( 1 Δ_func 𝐶 ) ) ‘ ∅ )
	isinito2lem.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	isinito2lem.i	⊢ ( 𝜑 → 𝐼 ∈ ( Base ‘ 𝐶 ) )
Assertion	isinito2lem	⊢ ( 𝜑 → ( 𝐼 ∈ ( InitO ‘ 𝐶 ) ↔ 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		isinito2.1	⊢ 1 = ( SetCat ‘ 1_o )
2		isinito2.f	⊢ 𝐹 = ( ( 1^st ‘ ( 1 Δ_func 𝐶 ) ) ‘ ∅ )
3		isinito2lem.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
4		isinito2lem.i	⊢ ( 𝜑 → 𝐼 ∈ ( Base ‘ 𝐶 ) )
5		reutru	⊢ ( ∃! 𝑓 𝑓 ∈ ( 𝐼 ( Hom ‘ 𝐶 ) 𝑥 ) ↔ ∃! 𝑓 ∈ ( 𝐼 ( Hom ‘ 𝐶 ) 𝑥 ) ⊤ )
6		0ex	⊢ ∅ ∈ V
7		eqeq1	⊢ ( 𝑦 = ∅ → ( 𝑦 = ( ( ( 𝐼 ( 2^nd ‘ 𝐹 ) 𝑥 ) ‘ 𝑓 ) ( ⟨ ∅ , ( ( 1^st ‘ 𝐹 ) ‘ 𝐼 ) ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , { ⟨ ∅ , ∅ , ∅ ⟩ } ⟩ } ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ∅ ) ↔ ∅ = ( ( ( 𝐼 ( 2^nd ‘ 𝐹 ) 𝑥 ) ‘ 𝑓 ) ( ⟨ ∅ , ( ( 1^st ‘ 𝐹 ) ‘ 𝐼 ) ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , { ⟨ ∅ , ∅ , ∅ ⟩ } ⟩ } ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ∅ ) ) )
8	7	reubidv	⊢ ( 𝑦 = ∅ → ( ∃! 𝑓 ∈ ( 𝐼 ( Hom ‘ 𝐶 ) 𝑥 ) 𝑦 = ( ( ( 𝐼 ( 2^nd ‘ 𝐹 ) 𝑥 ) ‘ 𝑓 ) ( ⟨ ∅ , ( ( 1^st ‘ 𝐹 ) ‘ 𝐼 ) ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , { ⟨ ∅ , ∅ , ∅ ⟩ } ⟩ } ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ∅ ) ↔ ∃! 𝑓 ∈ ( 𝐼 ( Hom ‘ 𝐶 ) 𝑥 ) ∅ = ( ( ( 𝐼 ( 2^nd ‘ 𝐹 ) 𝑥 ) ‘ 𝑓 ) ( ⟨ ∅ , ( ( 1^st ‘ 𝐹 ) ‘ 𝐼 ) ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , { ⟨ ∅ , ∅ , ∅ ⟩ } ⟩ } ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ∅ ) ) )
9	6 8	ralsn	⊢ ( ∀ 𝑦 ∈ { ∅ } ∃! 𝑓 ∈ ( 𝐼 ( Hom ‘ 𝐶 ) 𝑥 ) 𝑦 = ( ( ( 𝐼 ( 2^nd ‘ 𝐹 ) 𝑥 ) ‘ 𝑓 ) ( ⟨ ∅ , ( ( 1^st ‘ 𝐹 ) ‘ 𝐼 ) ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , { ⟨ ∅ , ∅ , ∅ ⟩ } ⟩ } ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ∅ ) ↔ ∃! 𝑓 ∈ ( 𝐼 ( Hom ‘ 𝐶 ) 𝑥 ) ∅ = ( ( ( 𝐼 ( 2^nd ‘ 𝐹 ) 𝑥 ) ‘ 𝑓 ) ( ⟨ ∅ , ( ( 1^st ‘ 𝐹 ) ‘ 𝐼 ) ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , { ⟨ ∅ , ∅ , ∅ ⟩ } ⟩ } ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ∅ ) )
10		eqid	⊢ ( 1 Δ_func 𝐶 ) = ( 1 Δ_func 𝐶 )
11		setc1oterm	⊢ ( SetCat ‘ 1_o ) ∈ TermCat
12	1 11	eqeltri	⊢ 1 ∈ TermCat
13	12	a1i	⊢ ( 𝜑 → 1 ∈ TermCat )
14	13	termccd	⊢ ( 𝜑 → 1 ∈ Cat )
15	1	setc1obas	⊢ 1_o = ( Base ‘ 1 )
16		0lt1o	⊢ ∅ ∈ 1_o
17	16	a1i	⊢ ( 𝜑 → ∅ ∈ 1_o )
18		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
19	10 14 3 15 17 2 18 4	diag11	⊢ ( 𝜑 → ( ( 1^st ‘ 𝐹 ) ‘ 𝐼 ) = ∅ )
20	19	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝐼 ) = ∅ )
21	20	opeq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ⟨ ∅ , ( ( 1^st ‘ 𝐹 ) ‘ 𝐼 ) ⟩ = ⟨ ∅ , ∅ ⟩ )
22	14	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 1 ∈ Cat )
23	3	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐶 ∈ Cat )
24	16	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ∅ ∈ 1_o )
25		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
26	10 22 23 15 24 2 18 25	diag11	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) = ∅ )
27	21 26	oveq12d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ⟨ ∅ , ( ( 1^st ‘ 𝐹 ) ‘ 𝐼 ) ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , { ⟨ ∅ , ∅ , ∅ ⟩ } ⟩ } ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) = ( ⟨ ∅ , ∅ ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , { ⟨ ∅ , ∅ , ∅ ⟩ } ⟩ } ∅ ) )
28		snex	⊢ { ⟨ ∅ , ∅ , ∅ ⟩ } ∈ V
29	28	ovsn2	⊢ ( ⟨ ∅ , ∅ ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , { ⟨ ∅ , ∅ , ∅ ⟩ } ⟩ } ∅ ) = { ⟨ ∅ , ∅ , ∅ ⟩ }
30	27 29	eqtrdi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ⟨ ∅ , ( ( 1^st ‘ 𝐹 ) ‘ 𝐼 ) ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , { ⟨ ∅ , ∅ , ∅ ⟩ } ⟩ } ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) = { ⟨ ∅ , ∅ , ∅ ⟩ } )
31	30	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑓 ∈ ( 𝐼 ( Hom ‘ 𝐶 ) 𝑥 ) ) → ( ⟨ ∅ , ( ( 1^st ‘ 𝐹 ) ‘ 𝐼 ) ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , { ⟨ ∅ , ∅ , ∅ ⟩ } ⟩ } ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) = { ⟨ ∅ , ∅ , ∅ ⟩ } )
32	12	a1i	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑓 ∈ ( 𝐼 ( Hom ‘ 𝐶 ) 𝑥 ) ) → 1 ∈ TermCat )
33	32	termccd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑓 ∈ ( 𝐼 ( Hom ‘ 𝐶 ) 𝑥 ) ) → 1 ∈ Cat )
34	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑓 ∈ ( 𝐼 ( Hom ‘ 𝐶 ) 𝑥 ) ) → 𝐶 ∈ Cat )
35	16	a1i	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑓 ∈ ( 𝐼 ( Hom ‘ 𝐶 ) 𝑥 ) ) → ∅ ∈ 1_o )
36	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑓 ∈ ( 𝐼 ( Hom ‘ 𝐶 ) 𝑥 ) ) → 𝐼 ∈ ( Base ‘ 𝐶 ) )
37		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
38		eqid	⊢ ( Id ‘ 1 ) = ( Id ‘ 1 )
39		simplr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑓 ∈ ( 𝐼 ( Hom ‘ 𝐶 ) 𝑥 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
40		simpr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑓 ∈ ( 𝐼 ( Hom ‘ 𝐶 ) 𝑥 ) ) → 𝑓 ∈ ( 𝐼 ( Hom ‘ 𝐶 ) 𝑥 ) )
41	10 33 34 15 35 2 18 36 37 38 39 40	diag12	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑓 ∈ ( 𝐼 ( Hom ‘ 𝐶 ) 𝑥 ) ) → ( ( 𝐼 ( 2^nd ‘ 𝐹 ) 𝑥 ) ‘ 𝑓 ) = ( ( Id ‘ 1 ) ‘ ∅ ) )
42	1 38	setc1oid	⊢ ( ( Id ‘ 1 ) ‘ ∅ ) = ∅
43	41 42	eqtrdi	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑓 ∈ ( 𝐼 ( Hom ‘ 𝐶 ) 𝑥 ) ) → ( ( 𝐼 ( 2^nd ‘ 𝐹 ) 𝑥 ) ‘ 𝑓 ) = ∅ )
44		eqidd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑓 ∈ ( 𝐼 ( Hom ‘ 𝐶 ) 𝑥 ) ) → ∅ = ∅ )
45	31 43 44	oveq123d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑓 ∈ ( 𝐼 ( Hom ‘ 𝐶 ) 𝑥 ) ) → ( ( ( 𝐼 ( 2^nd ‘ 𝐹 ) 𝑥 ) ‘ 𝑓 ) ( ⟨ ∅ , ( ( 1^st ‘ 𝐹 ) ‘ 𝐼 ) ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , { ⟨ ∅ , ∅ , ∅ ⟩ } ⟩ } ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ∅ ) = ( ∅ { ⟨ ∅ , ∅ , ∅ ⟩ } ∅ ) )
46	6	ovsn2	⊢ ( ∅ { ⟨ ∅ , ∅ , ∅ ⟩ } ∅ ) = ∅
47	45 46	eqtr2di	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑓 ∈ ( 𝐼 ( Hom ‘ 𝐶 ) 𝑥 ) ) → ∅ = ( ( ( 𝐼 ( 2^nd ‘ 𝐹 ) 𝑥 ) ‘ 𝑓 ) ( ⟨ ∅ , ( ( 1^st ‘ 𝐹 ) ‘ 𝐼 ) ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , { ⟨ ∅ , ∅ , ∅ ⟩ } ⟩ } ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ∅ ) )
48		tbtru	⊢ ( ∅ = ( ( ( 𝐼 ( 2^nd ‘ 𝐹 ) 𝑥 ) ‘ 𝑓 ) ( ⟨ ∅ , ( ( 1^st ‘ 𝐹 ) ‘ 𝐼 ) ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , { ⟨ ∅ , ∅ , ∅ ⟩ } ⟩ } ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ∅ ) ↔ ( ∅ = ( ( ( 𝐼 ( 2^nd ‘ 𝐹 ) 𝑥 ) ‘ 𝑓 ) ( ⟨ ∅ , ( ( 1^st ‘ 𝐹 ) ‘ 𝐼 ) ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , { ⟨ ∅ , ∅ , ∅ ⟩ } ⟩ } ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ∅ ) ↔ ⊤ ) )
49	47 48	sylib	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑓 ∈ ( 𝐼 ( Hom ‘ 𝐶 ) 𝑥 ) ) → ( ∅ = ( ( ( 𝐼 ( 2^nd ‘ 𝐹 ) 𝑥 ) ‘ 𝑓 ) ( ⟨ ∅ , ( ( 1^st ‘ 𝐹 ) ‘ 𝐼 ) ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , { ⟨ ∅ , ∅ , ∅ ⟩ } ⟩ } ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ∅ ) ↔ ⊤ ) )
50	49	reubidva	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ∃! 𝑓 ∈ ( 𝐼 ( Hom ‘ 𝐶 ) 𝑥 ) ∅ = ( ( ( 𝐼 ( 2^nd ‘ 𝐹 ) 𝑥 ) ‘ 𝑓 ) ( ⟨ ∅ , ( ( 1^st ‘ 𝐹 ) ‘ 𝐼 ) ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , { ⟨ ∅ , ∅ , ∅ ⟩ } ⟩ } ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ∅ ) ↔ ∃! 𝑓 ∈ ( 𝐼 ( Hom ‘ 𝐶 ) 𝑥 ) ⊤ ) )
51	9 50	bitr2id	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ∃! 𝑓 ∈ ( 𝐼 ( Hom ‘ 𝐶 ) 𝑥 ) ⊤ ↔ ∀ 𝑦 ∈ { ∅ } ∃! 𝑓 ∈ ( 𝐼 ( Hom ‘ 𝐶 ) 𝑥 ) 𝑦 = ( ( ( 𝐼 ( 2^nd ‘ 𝐹 ) 𝑥 ) ‘ 𝑓 ) ( ⟨ ∅ , ( ( 1^st ‘ 𝐹 ) ‘ 𝐼 ) ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , { ⟨ ∅ , ∅ , ∅ ⟩ } ⟩ } ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ∅ ) ) )
52	26	oveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ∅ { ⟨ ∅ , ∅ , 1_o ⟩ } ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) = ( ∅ { ⟨ ∅ , ∅ , 1_o ⟩ } ∅ ) )
53		1oex	⊢ 1_o ∈ V
54	53	ovsn2	⊢ ( ∅ { ⟨ ∅ , ∅ , 1_o ⟩ } ∅ ) = 1_o
55		df1o2	⊢ 1_o = { ∅ }
56	54 55	eqtri	⊢ ( ∅ { ⟨ ∅ , ∅ , 1_o ⟩ } ∅ ) = { ∅ }
57	52 56	eqtrdi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ∅ { ⟨ ∅ , ∅ , 1_o ⟩ } ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) = { ∅ } )
58	57	raleqdv	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ∀ 𝑦 ∈ ( ∅ { ⟨ ∅ , ∅ , 1_o ⟩ } ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ∃! 𝑓 ∈ ( 𝐼 ( Hom ‘ 𝐶 ) 𝑥 ) 𝑦 = ( ( ( 𝐼 ( 2^nd ‘ 𝐹 ) 𝑥 ) ‘ 𝑓 ) ( ⟨ ∅ , ( ( 1^st ‘ 𝐹 ) ‘ 𝐼 ) ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , { ⟨ ∅ , ∅ , ∅ ⟩ } ⟩ } ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ∅ ) ↔ ∀ 𝑦 ∈ { ∅ } ∃! 𝑓 ∈ ( 𝐼 ( Hom ‘ 𝐶 ) 𝑥 ) 𝑦 = ( ( ( 𝐼 ( 2^nd ‘ 𝐹 ) 𝑥 ) ‘ 𝑓 ) ( ⟨ ∅ , ( ( 1^st ‘ 𝐹 ) ‘ 𝐼 ) ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , { ⟨ ∅ , ∅ , ∅ ⟩ } ⟩ } ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ∅ ) ) )
59	51 58	bitr4d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ∃! 𝑓 ∈ ( 𝐼 ( Hom ‘ 𝐶 ) 𝑥 ) ⊤ ↔ ∀ 𝑦 ∈ ( ∅ { ⟨ ∅ , ∅ , 1_o ⟩ } ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ∃! 𝑓 ∈ ( 𝐼 ( Hom ‘ 𝐶 ) 𝑥 ) 𝑦 = ( ( ( 𝐼 ( 2^nd ‘ 𝐹 ) 𝑥 ) ‘ 𝑓 ) ( ⟨ ∅ , ( ( 1^st ‘ 𝐹 ) ‘ 𝐼 ) ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , { ⟨ ∅ , ∅ , ∅ ⟩ } ⟩ } ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ∅ ) ) )
60	5 59	bitrid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ∃! 𝑓 𝑓 ∈ ( 𝐼 ( Hom ‘ 𝐶 ) 𝑥 ) ↔ ∀ 𝑦 ∈ ( ∅ { ⟨ ∅ , ∅ , 1_o ⟩ } ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ∃! 𝑓 ∈ ( 𝐼 ( Hom ‘ 𝐶 ) 𝑥 ) 𝑦 = ( ( ( 𝐼 ( 2^nd ‘ 𝐹 ) 𝑥 ) ‘ 𝑓 ) ( ⟨ ∅ , ( ( 1^st ‘ 𝐹 ) ‘ 𝐼 ) ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , { ⟨ ∅ , ∅ , ∅ ⟩ } ⟩ } ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ∅ ) ) )
61	60	ralbidva	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∃! 𝑓 𝑓 ∈ ( 𝐼 ( Hom ‘ 𝐶 ) 𝑥 ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( ∅ { ⟨ ∅ , ∅ , 1_o ⟩ } ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ∃! 𝑓 ∈ ( 𝐼 ( Hom ‘ 𝐶 ) 𝑥 ) 𝑦 = ( ( ( 𝐼 ( 2^nd ‘ 𝐹 ) 𝑥 ) ‘ 𝑓 ) ( ⟨ ∅ , ( ( 1^st ‘ 𝐹 ) ‘ 𝐼 ) ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , { ⟨ ∅ , ∅ , ∅ ⟩ } ⟩ } ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ∅ ) ) )
62	18 37 3 4	isinito	⊢ ( 𝜑 → ( 𝐼 ∈ ( InitO ‘ 𝐶 ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∃! 𝑓 𝑓 ∈ ( 𝐼 ( Hom ‘ 𝐶 ) 𝑥 ) ) )
63	1	setc1ohomfval	⊢ { ⟨ ∅ , ∅ , 1_o ⟩ } = ( Hom ‘ 1 )
64	1	setc1ocofval	⊢ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , { ⟨ ∅ , ∅ , ∅ ⟩ } ⟩ } = ( comp ‘ 1 )
65	1 2 3	funcsetc1ocl	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 1 ) )
66	65	func1st2nd	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 1 ) ( 2^nd ‘ 𝐹 ) )
67	19	oveq2d	⊢ ( 𝜑 → ( ∅ { ⟨ ∅ , ∅ , 1_o ⟩ } ( ( 1^st ‘ 𝐹 ) ‘ 𝐼 ) ) = ( ∅ { ⟨ ∅ , ∅ , 1_o ⟩ } ∅ ) )
68	67 54	eqtrdi	⊢ ( 𝜑 → ( ∅ { ⟨ ∅ , ∅ , 1_o ⟩ } ( ( 1^st ‘ 𝐹 ) ‘ 𝐼 ) ) = 1_o )
69	16 68	eleqtrrid	⊢ ( 𝜑 → ∅ ∈ ( ∅ { ⟨ ∅ , ∅ , 1_o ⟩ } ( ( 1^st ‘ 𝐹 ) ‘ 𝐼 ) ) )
70	18 15 37 63 64 17 66 4 69	isup	⊢ ( 𝜑 → ( 𝐼 ( ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ ( 𝐶 UP 1 ) ∅ ) ∅ ↔ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( ∅ { ⟨ ∅ , ∅ , 1_o ⟩ } ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ∃! 𝑓 ∈ ( 𝐼 ( Hom ‘ 𝐶 ) 𝑥 ) 𝑦 = ( ( ( 𝐼 ( 2^nd ‘ 𝐹 ) 𝑥 ) ‘ 𝑓 ) ( ⟨ ∅ , ( ( 1^st ‘ 𝐹 ) ‘ 𝐼 ) ⟩ { ⟨ ⟨ ∅ , ∅ ⟩ , ∅ , { ⟨ ∅ , ∅ , ∅ ⟩ } ⟩ } ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ∅ ) ) )
71	61 62 70	3bitr4d	⊢ ( 𝜑 → ( 𝐼 ∈ ( InitO ‘ 𝐶 ) ↔ 𝐼 ( ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ ( 𝐶 UP 1 ) ∅ ) ∅ ) )
72	65	up1st2ndb	⊢ ( 𝜑 → ( 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) ∅ ↔ 𝐼 ( ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ ( 𝐶 UP 1 ) ∅ ) ∅ ) )
73	71 72	bitr4d	⊢ ( 𝜑 → ( 𝐼 ∈ ( InitO ‘ 𝐶 ) ↔ 𝐼 ( 𝐹 ( 𝐶 UP 1 ) ∅ ) ∅ ) )

Metamath Proof Explorer

Theorem isinito2lem

Proof