fucoaltnelem

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

	Ref	Expression
Hypotheses	fucoaltfunc.q	\|- Q = ( C FuncCat E )
	fucoaltval.l	\|- L = ( <. C , C >. o.F E )
	fucoaltval.c	\|- ( ph -> C e. Cat )
	fucoaltval.e	\|- ( ph -> E e. Cat )
	fucoaltval.k	\|- ( ph -> K e. ( Q Func Q ) )
	fucoaltval.f	\|- ( ph -> F e. ( C Func E ) )
	fucoaltval.g	\|- ( ph -> G e. ( C Func E ) )
	fucoaltval.a	\|- ( ph -> A e. ( F ( C Nat E ) G ) )
	fucoaltne.n	\|- ( ph -> ( ( F ( 2nd ` K ) G ) ` A ) =/= A )
	fucoaltnelem.t	\|- T = ( ( C FuncCat E ) Xc. ( C FuncCat C ) )
	fucoaltnelem.i	\|- I = ( idFunc ` C )
	fucoaltnelem.j	\|- J = ( Id ` ( C FuncCat C ) )
Assertion	fucoaltnelem	\|- ( ph -> ( 2nd ` ( K o.func L ) ) =/= ( 2nd ` L ) )

Proof

Step	Hyp	Ref	Expression
1		fucoaltfunc.q	\|- Q = ( C FuncCat E )
2		fucoaltval.l	\|- L = ( <. C , C >. o.F E )
3		fucoaltval.c	\|- ( ph -> C e. Cat )
4		fucoaltval.e	\|- ( ph -> E e. Cat )
5		fucoaltval.k	\|- ( ph -> K e. ( Q Func Q ) )
6		fucoaltval.f	\|- ( ph -> F e. ( C Func E ) )
7		fucoaltval.g	\|- ( ph -> G e. ( C Func E ) )
8		fucoaltval.a	\|- ( ph -> A e. ( F ( C Nat E ) G ) )
9		fucoaltne.n	\|- ( ph -> ( ( F ( 2nd ` K ) G ) ` A ) =/= A )
10		fucoaltnelem.t	\|- T = ( ( C FuncCat E ) Xc. ( C FuncCat C ) )
11		fucoaltnelem.i	\|- I = ( idFunc ` C )
12		fucoaltnelem.j	\|- J = ( Id ` ( C FuncCat C ) )
13		simpr	\|- ( ( ph /\ ( 2nd ` ( K o.func L ) ) = ( 2nd ` L ) ) -> ( 2nd ` ( K o.func L ) ) = ( 2nd ` L ) )
14	13	oveqd	\|- ( ( ph /\ ( 2nd ` ( K o.func L ) ) = ( 2nd ` L ) ) -> ( <. F , I >. ( 2nd ` ( K o.func L ) ) <. G , I >. ) = ( <. F , I >. ( 2nd ` L ) <. G , I >. ) )
15	14	oveqd	\|- ( ( ph /\ ( 2nd ` ( K o.func L ) ) = ( 2nd ` L ) ) -> ( A ( <. F , I >. ( 2nd ` ( K o.func L ) ) <. G , I >. ) ( J ` I ) ) = ( A ( <. F , I >. ( 2nd ` L ) <. G , I >. ) ( J ` I ) ) )
16	1 2 3 4 5 6 7 8 11 12	fucoaltval	\|- ( ph -> ( A ( <. F , I >. ( 2nd ` ( K o.func L ) ) <. G , I >. ) ( J ` I ) ) = ( ( F ( 2nd ` K ) G ) ` A ) )
17	16	adantr	\|- ( ( ph /\ ( 2nd ` ( K o.func L ) ) = ( 2nd ` L ) ) -> ( A ( <. F , I >. ( 2nd ` ( K o.func L ) ) <. G , I >. ) ( J ` I ) ) = ( ( F ( 2nd ` K ) G ) ` A ) )
18	2	eqcomi	\|- ( <. C , C >. o.F E ) = L
19	18	fveq2i	\|- ( 2nd ` ( <. C , C >. o.F E ) ) = ( 2nd ` L )
20	19	a1i	\|- ( ph -> ( 2nd ` ( <. C , C >. o.F E ) ) = ( 2nd ` L ) )
21		eqid	\|- ( C FuncCat C ) = ( C FuncCat C )
22	20 21 12 11 3 8	fucoridid	\|- ( ph -> ( A ( <. F , I >. ( 2nd ` L ) <. G , I >. ) ( J ` I ) ) = A )
23	22	adantr	\|- ( ( ph /\ ( 2nd ` ( K o.func L ) ) = ( 2nd ` L ) ) -> ( A ( <. F , I >. ( 2nd ` L ) <. G , I >. ) ( J ` I ) ) = A )
24	15 17 23	3eqtr3d	\|- ( ( ph /\ ( 2nd ` ( K o.func L ) ) = ( 2nd ` L ) ) -> ( ( F ( 2nd ` K ) G ) ` A ) = A )
25	9 24	mteqand	\|- ( ph -> ( 2nd ` ( K o.func L ) ) =/= ( 2nd ` L ) )

Metamath Proof Explorer

Theorem fucoaltnelem

Proof