fuconuniqlem

Description: Lemma for fuconuniq . (Contributed by Zhi Wang, 14-Sep-2026) (New usage is discouraged.)

	Ref	Expression
Hypotheses	fuconuniq2.c	⊢ 𝐶 = ( SetCat ‘ 1_o )
	fuconuniq2.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 ↦ ( 𝑟 ∩ 𝑠 ) ) ) ⟩ }
	fuconuniq2.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐸 )
	fuconuniq2.l	⊢ 𝐿 = ( ⟨ 𝐶 , 𝐶 ⟩ ∘_F 𝐸 )
	fuconuniq.a	⊢ 𝐴 = ( 𝑏 ∈ 3_o ↦ if ( 𝑏 = 2_o , 2_o , if ( 𝑏 = ∅ , 1_o , ∅ ) ) )
	fuconuniq.m	⊢ 𝑀 = ( 𝑢 ∈ 2_o , 𝑣 ∈ 2_o ↦ ( 𝑎 ∈ ( 𝑢 ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) ) 𝑣 ) ↦ ( 𝐴 ‘ 𝑎 ) ) )
	fuconuniq.s	⊢ 𝑆 = ⟨ ( I ↾ 2_o ) , 𝑀 ⟩
	fuconuniq.r	⊢ 𝑅 = ( 𝐸 FuncCat 𝐸 )
	fuconuniq.o	⊢ ⚬ = ( ⟨ 𝑅 , 𝑄 ⟩ curry_F ( ⟨ 𝐶 , 𝐸 ⟩ ∘_F 𝐸 ) )
	fuconuniq.k	⊢ 𝐾 = ( ( 1^st ‘ ⚬ ) ‘ 𝑆 )
	fuconuniqlem.t	⊢ 𝑇 = ( ( 𝐶 FuncCat 𝐸 ) ×_c ( 𝐶 FuncCat 𝐶 ) )
	fuconuniqlem.d	⊢ 𝐷 = ( 𝐸 Δ_func 𝐶 )
	fuconuniqlem.f	⊢ 𝐹 = ( ( 1^st ‘ 𝐷 ) ‘ ∅ )
	fuconuniqlem.g	⊢ 𝐺 = ( ( 1^st ‘ 𝐷 ) ‘ 1_o )
	fuconuniqlem.n	⊢ 𝑁 = ( 1_o × { ∅ } )
Assertion	fuconuniqlem	⊢ ( ( 1^st ‘ 𝐿 ) ( 𝑇 Func 𝑄 ) ( 2^nd ‘ ( 𝐾 ∘_func 𝐿 ) ) ∧ ( 2^nd ‘ ( 𝐾 ∘_func 𝐿 ) ) ≠ ( 2^nd ‘ 𝐿 ) )

Proof

Step	Hyp	Ref	Expression
1		fuconuniq2.c	⊢ 𝐶 = ( SetCat ‘ 1_o )
2		fuconuniq2.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		fuconuniq2.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐸 )
4		fuconuniq2.l	⊢ 𝐿 = ( ⟨ 𝐶 , 𝐶 ⟩ ∘_F 𝐸 )
5		fuconuniq.a	⊢ 𝐴 = ( 𝑏 ∈ 3_o ↦ if ( 𝑏 = 2_o , 2_o , if ( 𝑏 = ∅ , 1_o , ∅ ) ) )
6		fuconuniq.m	⊢ 𝑀 = ( 𝑢 ∈ 2_o , 𝑣 ∈ 2_o ↦ ( 𝑎 ∈ ( 𝑢 ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) ) 𝑣 ) ↦ ( 𝐴 ‘ 𝑎 ) ) )
7		fuconuniq.s	⊢ 𝑆 = ⟨ ( I ↾ 2_o ) , 𝑀 ⟩
8		fuconuniq.r	⊢ 𝑅 = ( 𝐸 FuncCat 𝐸 )
9		fuconuniq.o	⊢ ⚬ = ( ⟨ 𝑅 , 𝑄 ⟩ curry_F ( ⟨ 𝐶 , 𝐸 ⟩ ∘_F 𝐸 ) )
10		fuconuniq.k	⊢ 𝐾 = ( ( 1^st ‘ ⚬ ) ‘ 𝑆 )
11		fuconuniqlem.t	⊢ 𝑇 = ( ( 𝐶 FuncCat 𝐸 ) ×_c ( 𝐶 FuncCat 𝐶 ) )
12		fuconuniqlem.d	⊢ 𝐷 = ( 𝐸 Δ_func 𝐶 )
13		fuconuniqlem.f	⊢ 𝐹 = ( ( 1^st ‘ 𝐷 ) ‘ ∅ )
14		fuconuniqlem.g	⊢ 𝐺 = ( ( 1^st ‘ 𝐷 ) ‘ 1_o )
15		fuconuniqlem.n	⊢ 𝑁 = ( 1_o × { ∅ } )
16		setc1oterm	⊢ ( SetCat ‘ 1_o ) ∈ TermCat
17	1 16	eqeltri	⊢ 𝐶 ∈ TermCat
18	17	a1i	⊢ ( ⊤ → 𝐶 ∈ TermCat )
19	18	termccatd	⊢ ( ⊤ → 𝐶 ∈ Cat )
20	2	par2catid	⊢ ( 𝐸 ∈ Cat ∧ ( Id ‘ 𝐸 ) = ( 𝑦 ∈ 2_o ↦ 2_o ) )
21	20	simpli	⊢ 𝐸 ∈ Cat
22	21	a1i	⊢ ( ⊤ → 𝐸 ∈ Cat )
23	2 5 6	parswapfunc	⊢ ⟨ ( I ↾ 2_o ) , 𝑀 ⟩ ∈ ( 𝐸 Func 𝐸 )
24	7 23	eqeltri	⊢ 𝑆 ∈ ( 𝐸 Func 𝐸 )
25	24	a1i	⊢ ( ⊤ → 𝑆 ∈ ( 𝐸 Func 𝐸 ) )
26		mptresid	⊢ ( I ↾ 2_o ) = ( 𝑥 ∈ 2_o ↦ 𝑥 )
27		2oex	⊢ 2_o ∈ V
28	27	mptex	⊢ ( 𝑥 ∈ 2_o ↦ 𝑥 ) ∈ V
29	26 28	eqeltri	⊢ ( I ↾ 2_o ) ∈ V
30	27 27	mpoex	⊢ ( 𝑢 ∈ 2_o , 𝑣 ∈ 2_o ↦ ( 𝑎 ∈ ( 𝑢 ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) ) 𝑣 ) ↦ ( 𝐴 ‘ 𝑎 ) ) ) ∈ V
31	6 30	eqeltri	⊢ 𝑀 ∈ V
32	29 31	op1std	⊢ ( 𝑆 = ⟨ ( I ↾ 2_o ) , 𝑀 ⟩ → ( 1^st ‘ 𝑆 ) = ( I ↾ 2_o ) )
33	7 32	mp1i	⊢ ( ⊤ → ( 1^st ‘ 𝑆 ) = ( I ↾ 2_o ) )
34	18 3 8 9 10 25 33	termcpostfix	⊢ ( ⊤ → ( 𝐾 ∈ ( 𝑄 Func 𝑄 ) ∧ ( 1^st ‘ 𝐾 ) = ( I ↾ ( 𝐶 Func 𝐸 ) ) ) )
35	34	simpld	⊢ ( ⊤ → 𝐾 ∈ ( 𝑄 Func 𝑄 ) )
36	34	simprd	⊢ ( ⊤ → ( 1^st ‘ 𝐾 ) = ( I ↾ ( 𝐶 Func 𝐸 ) ) )
37	3 11 4 19 19 22 35 36	fucoaltfunc	⊢ ( ⊤ → ( 1^st ‘ 𝐿 ) ( 𝑇 Func 𝑄 ) ( 2^nd ‘ ( 𝐾 ∘_func 𝐿 ) ) )
38	1 2 12 13 14 15	par2diag	⊢ ( ( 𝐹 ∈ ( 𝐶 Func 𝐸 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐸 ) ) ∧ ( 𝑁 ∈ ( 𝐹 ( 𝐶 Nat 𝐸 ) 𝐺 ) ∧ ( 𝑁 ‘ ∅ ) = ∅ ) ∧ ( ( ( 1^st ‘ 𝐹 ) ‘ ∅ ) = ∅ ∧ ( ( 1^st ‘ 𝐺 ) ‘ ∅ ) = 1_o ) )
39	38	simp1i	⊢ ( 𝐹 ∈ ( 𝐶 Func 𝐸 ) ∧ 𝐺 ∈ ( 𝐶 Func 𝐸 ) )
40	39	simpli	⊢ 𝐹 ∈ ( 𝐶 Func 𝐸 )
41	40	a1i	⊢ ( ⊤ → 𝐹 ∈ ( 𝐶 Func 𝐸 ) )
42	39	simpri	⊢ 𝐺 ∈ ( 𝐶 Func 𝐸 )
43	42	a1i	⊢ ( ⊤ → 𝐺 ∈ ( 𝐶 Func 𝐸 ) )
44	38	simp2i	⊢ ( 𝑁 ∈ ( 𝐹 ( 𝐶 Nat 𝐸 ) 𝐺 ) ∧ ( 𝑁 ‘ ∅ ) = ∅ )
45	44	simpli	⊢ 𝑁 ∈ ( 𝐹 ( 𝐶 Nat 𝐸 ) 𝐺 )
46	45	a1i	⊢ ( ⊤ → 𝑁 ∈ ( 𝐹 ( 𝐶 Nat 𝐸 ) 𝐺 ) )
47		0lt1o	⊢ ∅ ∈ 1_o
48	1	setc1obas	⊢ 1_o = ( Base ‘ 𝐶 )
49	47 48	eleqtri	⊢ ∅ ∈ ( Base ‘ 𝐶 )
50	49	a1i	⊢ ( ⊤ → ∅ ∈ ( Base ‘ 𝐶 ) )
51	3 8 9 25 19 10 41 43 46 50	postcof2	⊢ ( ⊤ → ( ( ( 𝐹 ( 2^nd ‘ 𝐾 ) 𝐺 ) ‘ 𝑁 ) ‘ ∅ ) = ( ( ( ( 1^st ‘ 𝐹 ) ‘ ∅ ) ( 2^nd ‘ 𝑆 ) ( ( 1^st ‘ 𝐺 ) ‘ ∅ ) ) ‘ ( 𝑁 ‘ ∅ ) ) )
52	51	mptru	⊢ ( ( ( 𝐹 ( 2^nd ‘ 𝐾 ) 𝐺 ) ‘ 𝑁 ) ‘ ∅ ) = ( ( ( ( 1^st ‘ 𝐹 ) ‘ ∅ ) ( 2^nd ‘ 𝑆 ) ( ( 1^st ‘ 𝐺 ) ‘ ∅ ) ) ‘ ( 𝑁 ‘ ∅ ) )
53	38	simp3i	⊢ ( ( ( 1^st ‘ 𝐹 ) ‘ ∅ ) = ∅ ∧ ( ( 1^st ‘ 𝐺 ) ‘ ∅ ) = 1_o )
54	53	simpli	⊢ ( ( 1^st ‘ 𝐹 ) ‘ ∅ ) = ∅
55	53	simpri	⊢ ( ( 1^st ‘ 𝐺 ) ‘ ∅ ) = 1_o
56	29 31	op2ndd	⊢ ( 𝑆 = ⟨ ( I ↾ 2_o ) , 𝑀 ⟩ → ( 2^nd ‘ 𝑆 ) = 𝑀 )
57	7 56	ax-mp	⊢ ( 2^nd ‘ 𝑆 ) = 𝑀
58	54 55 57	oveq123i	⊢ ( ( ( 1^st ‘ 𝐹 ) ‘ ∅ ) ( 2^nd ‘ 𝑆 ) ( ( 1^st ‘ 𝐺 ) ‘ ∅ ) ) = ( ∅ 𝑀 1_o )
59	44	simpri	⊢ ( 𝑁 ‘ ∅ ) = ∅
60	58 59	fveq12i	⊢ ( ( ( ( 1^st ‘ 𝐹 ) ‘ ∅ ) ( 2^nd ‘ 𝑆 ) ( ( 1^st ‘ 𝐺 ) ‘ ∅ ) ) ‘ ( 𝑁 ‘ ∅ ) ) = ( ( ∅ 𝑀 1_o ) ‘ ∅ )
61	52 60	eqtri	⊢ ( ( ( 𝐹 ( 2^nd ‘ 𝐾 ) 𝐺 ) ‘ 𝑁 ) ‘ ∅ ) = ( ( ∅ 𝑀 1_o ) ‘ ∅ )
62		0ex	⊢ ∅ ∈ V
63	62	prid1	⊢ ∅ ∈ { ∅ , 1_o }
64		df2o3	⊢ 2_o = { ∅ , 1_o }
65	63 64	eleqtrri	⊢ ∅ ∈ 2_o
66	65	a1i	⊢ ( ⊤ → ∅ ∈ 2_o )
67		1oelpr	⊢ 1_o ∈ { ∅ , 1_o }
68	67 64	eleqtrri	⊢ 1_o ∈ 2_o
69	68	a1i	⊢ ( ⊤ → 1_o ∈ 2_o )
70		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 , ∅ ) ) )
71	70	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 , ∅ ) ) ) ∅ ) = ∅ ) )
72	71	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 , ∅ ) ) ) ∅ ) = ∅ )
73	72	simpli	⊢ ( ∅ ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) ) 1_o ) = 2_o
74	65 73	eleqtrri	⊢ ∅ ∈ ( ∅ ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) ) 1_o )
75	74	a1i	⊢ ( ⊤ → ∅ ∈ ( ∅ ( 𝑚 ∈ 2_o , 𝑛 ∈ 2_o ↦ if ( 𝑚 = 𝑛 , { 2_o } , if ( ( 𝑚 = ∅ ∧ 𝑛 = 1_o ) , 2_o , ∅ ) ) ) 1_o ) )
76	6 66 69 75	fvmpomptd	⊢ ( ⊤ → ( ( ∅ 𝑀 1_o ) ‘ ∅ ) = ( 𝐴 ‘ ∅ ) )
77	76	mptru	⊢ ( ( ∅ 𝑀 1_o ) ‘ ∅ ) = ( 𝐴 ‘ ∅ )
78	5	parswapprop	⊢ ( ( 𝐴 ‘ 2_o ) = 2_o ∧ ∀ 𝑡 ∈ 2_o ( 𝐴 ‘ 𝑡 ) ∈ 2_o ∧ ( 𝐴 ‘ ∅ ) = 1_o )
79	78	simp3i	⊢ ( 𝐴 ‘ ∅ ) = 1_o
80	61 77 79	3eqtri	⊢ ( ( ( 𝐹 ( 2^nd ‘ 𝐾 ) 𝐺 ) ‘ 𝑁 ) ‘ ∅ ) = 1_o
81		1n0	⊢ 1_o ≠ ∅
82	80 81	eqnetri	⊢ ( ( ( 𝐹 ( 2^nd ‘ 𝐾 ) 𝐺 ) ‘ 𝑁 ) ‘ ∅ ) ≠ ∅
83	82 59	neeqtrri	⊢ ( ( ( 𝐹 ( 2^nd ‘ 𝐾 ) 𝐺 ) ‘ 𝑁 ) ‘ ∅ ) ≠ ( 𝑁 ‘ ∅ )
84		fveq1	⊢ ( ( ( 𝐹 ( 2^nd ‘ 𝐾 ) 𝐺 ) ‘ 𝑁 ) = 𝑁 → ( ( ( 𝐹 ( 2^nd ‘ 𝐾 ) 𝐺 ) ‘ 𝑁 ) ‘ ∅ ) = ( 𝑁 ‘ ∅ ) )
85	84	necon3i	⊢ ( ( ( ( 𝐹 ( 2^nd ‘ 𝐾 ) 𝐺 ) ‘ 𝑁 ) ‘ ∅ ) ≠ ( 𝑁 ‘ ∅ ) → ( ( 𝐹 ( 2^nd ‘ 𝐾 ) 𝐺 ) ‘ 𝑁 ) ≠ 𝑁 )
86	83 85	mp1i	⊢ ( ⊤ → ( ( 𝐹 ( 2^nd ‘ 𝐾 ) 𝐺 ) ‘ 𝑁 ) ≠ 𝑁 )
87	3 4 19 22 35 41 43 46 86	fucoaltne	⊢ ( ⊤ → ( 2^nd ‘ ( 𝐾 ∘_func 𝐿 ) ) ≠ ( 2^nd ‘ 𝐿 ) )
88	37 87	jca	⊢ ( ⊤ → ( ( 1^st ‘ 𝐿 ) ( 𝑇 Func 𝑄 ) ( 2^nd ‘ ( 𝐾 ∘_func 𝐿 ) ) ∧ ( 2^nd ‘ ( 𝐾 ∘_func 𝐿 ) ) ≠ ( 2^nd ‘ 𝐿 ) ) )
89	88	mptru	⊢ ( ( 1^st ‘ 𝐿 ) ( 𝑇 Func 𝑄 ) ( 2^nd ‘ ( 𝐾 ∘_func 𝐿 ) ) ∧ ( 2^nd ‘ ( 𝐾 ∘_func 𝐿 ) ) ≠ ( 2^nd ‘ 𝐿 ) )

Metamath Proof Explorer

Theorem fuconuniqlem

Proof