Theorem fucoaltnelem

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

	Ref	Expression
Hypotheses	fucoaltfunc.q	$$⊢Q=C\mathrm{FuncCat}E$$
	fucoaltval.l	No typesetting found for |- L = ( <. C , C >. o.F E ) with typecode |-
	fucoaltval.c	$$⊢\phi \to C\in \mathrm{Cat}$$
	fucoaltval.e	$$⊢\phi \to E\in \mathrm{Cat}$$
	fucoaltval.k	$$⊢\phi \to K\in \left(Q\mathrm{Func}Q\right)$$
	fucoaltval.f	$$⊢\phi \to F\in \left(C\mathrm{Func}E\right)$$
	fucoaltval.g	$$⊢\phi \to G\in \left(C\mathrm{Func}E\right)$$
	fucoaltval.a	$$⊢\phi \to A\in \left(F\left(C\mathrm{Nat}E\right)G\right)$$
	fucoaltne.n	$$⊢\phi \to \left(F{2}^{nd}\left(K\right)G\right)\left(A\right)\ne A$$
	fucoaltnelem.t	$$⊢T=\left(C\mathrm{FuncCat}E\right){\times }_c\left(C\mathrm{FuncCat}C\right)$$
	fucoaltnelem.i	$$⊢I={id}_{\mathrm{func}}\left(C\right)$$
	fucoaltnelem.j	$$⊢J=\mathrm{Id}\left(C\mathrm{FuncCat}C\right)$$
Assertion	fucoaltnelem	$$⊢\phi \to 2^{nd}\left(K{\circ }_{\mathrm{func}}L\right)\ne 2^{nd}\left(L\right)$$

Proof

Step	Hyp	Ref	Expression
1		fucoaltfunc.q	$$⊢Q=C\mathrm{FuncCat}E$$
2		fucoaltval.l	Could not format L = ( <. C , C >. o.F E ) : No typesetting found for |- L = ( <. C , C >. o.F E ) with typecode |-
3		fucoaltval.c	$$⊢\phi \to C\in \mathrm{Cat}$$
4		fucoaltval.e	$$⊢\phi \to E\in \mathrm{Cat}$$
5		fucoaltval.k	$$⊢\phi \to K\in \left(Q\mathrm{Func}Q\right)$$
6		fucoaltval.f	$$⊢\phi \to F\in \left(C\mathrm{Func}E\right)$$
7		fucoaltval.g	$$⊢\phi \to G\in \left(C\mathrm{Func}E\right)$$
8		fucoaltval.a	$$⊢\phi \to A\in \left(F\left(C\mathrm{Nat}E\right)G\right)$$
9		fucoaltne.n	$$⊢\phi \to \left(F{2}^{nd}\left(K\right)G\right)\left(A\right)\ne A$$
10		fucoaltnelem.t	$$⊢T=\left(C\mathrm{FuncCat}E\right){\times }_c\left(C\mathrm{FuncCat}C\right)$$
11		fucoaltnelem.i	$$⊢I={id}_{\mathrm{func}}\left(C\right)$$
12		fucoaltnelem.j	$$⊢J=\mathrm{Id}\left(C\mathrm{FuncCat}C\right)$$
13		simpr	$$⊢\left(\phi \wedge 2^{nd}\left(K{\circ }_{\mathrm{func}}L\right)=2^{nd}\left(L\right)\right)\to 2^{nd}\left(K{\circ }_{\mathrm{func}}L\right)=2^{nd}\left(L\right)$$
14	13	oveqd	$$⊢\left(\phi \wedge 2^{nd}\left(K{\circ }_{\mathrm{func}}L\right)=2^{nd}\left(L\right)\right)\to ⟨F,I⟩2^{nd}\left(K{\circ }_{\mathrm{func}}L\right)⟨G,I⟩=⟨F,I⟩2^{nd}\left(L\right)⟨G,I⟩$$
15	14	oveqd	$$⊢\left(\phi \wedge 2^{nd}\left(K{\circ }_{\mathrm{func}}L\right)=2^{nd}\left(L\right)\right)\to A\left(⟨F,I⟩2^{nd}\left(K{\circ }_{\mathrm{func}}L\right)⟨G,I⟩\right)J\left(I\right)=A\left(⟨F,I⟩2^{nd}\left(L\right)⟨G,I⟩\right)J\left(I\right)$$
16	1 2 3 4 5 6 7 8 11 12	fucoaltval	$$⊢\phi \to A\left(⟨F,I⟩2^{nd}\left(K{\circ }_{\mathrm{func}}L\right)⟨G,I⟩\right)J\left(I\right)=\left(F{2}^{nd}\left(K\right)G\right)\left(A\right)$$
17	16	adantr	$$⊢\left(\phi \wedge 2^{nd}\left(K{\circ }_{\mathrm{func}}L\right)=2^{nd}\left(L\right)\right)\to A\left(⟨F,I⟩2^{nd}\left(K{\circ }_{\mathrm{func}}L\right)⟨G,I⟩\right)J\left(I\right)=\left(F{2}^{nd}\left(K\right)G\right)\left(A\right)$$
18	2	eqcomi	Could not format ( <. C , C >. o.F E ) = L : No typesetting found for |- ( <. C , C >. o.F E ) = L with typecode |-
19	18	fveq2i	Could not format ( 2nd ` ( <. C , C >. o.F E ) ) = ( 2nd ` L ) : No typesetting found for |- ( 2nd ` ( <. C , C >. o.F E ) ) = ( 2nd ` L ) with typecode |-
20	19	a1i	Could not format ( ph -> ( 2nd ` ( <. C , C >. o.F E ) ) = ( 2nd ` L ) ) : No typesetting found for |- ( ph -> ( 2nd ` ( <. C , C >. o.F E ) ) = ( 2nd ` L ) ) with typecode |-
21		eqid	$$⊢C\mathrm{FuncCat}C=C\mathrm{FuncCat}C$$
22	20 21 12 11 3 8	fucoridid	$$⊢\phi \to A\left(⟨F,I⟩2^{nd}\left(L\right)⟨G,I⟩\right)J\left(I\right)=A$$
23	22	adantr	$$⊢\left(\phi \wedge 2^{nd}\left(K{\circ }_{\mathrm{func}}L\right)=2^{nd}\left(L\right)\right)\to A\left(⟨F,I⟩2^{nd}\left(L\right)⟨G,I⟩\right)J\left(I\right)=A$$
24	15 17 23	3eqtr3d	$$⊢\left(\phi \wedge 2^{nd}\left(K{\circ }_{\mathrm{func}}L\right)=2^{nd}\left(L\right)\right)\to \left(F{2}^{nd}\left(K\right)G\right)\left(A\right)=A$$
25	9 24	mteqand	$$⊢\phi \to 2^{nd}\left(K{\circ }_{\mathrm{func}}L\right)\ne 2^{nd}\left(L\right)$$