fucoaltnelem

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

	Ref	Expression
Hypotheses	fucoaltfunc.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐸 )
	fucoaltval.l	⊢ 𝐿 = ( ⟨ 𝐶 , 𝐶 ⟩ ∘_F 𝐸 )
	fucoaltval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	fucoaltval.e	⊢ ( 𝜑 → 𝐸 ∈ Cat )
	fucoaltval.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑄 Func 𝑄 ) )
	fucoaltval.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐸 ) )
	fucoaltval.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝐸 ) )
	fucoaltval.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐹 ( 𝐶 Nat 𝐸 ) 𝐺 ) )
	fucoaltne.n	⊢ ( 𝜑 → ( ( 𝐹 ( 2^nd ‘ 𝐾 ) 𝐺 ) ‘ 𝐴 ) ≠ 𝐴 )
	fucoaltnelem.t	⊢ 𝑇 = ( ( 𝐶 FuncCat 𝐸 ) ×_c ( 𝐶 FuncCat 𝐶 ) )
	fucoaltnelem.i	⊢ 𝐼 = ( id_func ‘ 𝐶 )
	fucoaltnelem.j	⊢ 𝐽 = ( Id ‘ ( 𝐶 FuncCat 𝐶 ) )
Assertion	fucoaltnelem	⊢ ( 𝜑 → ( 2^nd ‘ ( 𝐾 ∘_func 𝐿 ) ) ≠ ( 2^nd ‘ 𝐿 ) )

Proof

Step	Hyp	Ref	Expression
1		fucoaltfunc.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐸 )
2		fucoaltval.l	⊢ 𝐿 = ( ⟨ 𝐶 , 𝐶 ⟩ ∘_F 𝐸 )
3		fucoaltval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
4		fucoaltval.e	⊢ ( 𝜑 → 𝐸 ∈ Cat )
5		fucoaltval.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑄 Func 𝑄 ) )
6		fucoaltval.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐸 ) )
7		fucoaltval.g	⊢ ( 𝜑 → 𝐺 ∈ ( 𝐶 Func 𝐸 ) )
8		fucoaltval.a	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐹 ( 𝐶 Nat 𝐸 ) 𝐺 ) )
9		fucoaltne.n	⊢ ( 𝜑 → ( ( 𝐹 ( 2^nd ‘ 𝐾 ) 𝐺 ) ‘ 𝐴 ) ≠ 𝐴 )
10		fucoaltnelem.t	⊢ 𝑇 = ( ( 𝐶 FuncCat 𝐸 ) ×_c ( 𝐶 FuncCat 𝐶 ) )
11		fucoaltnelem.i	⊢ 𝐼 = ( id_func ‘ 𝐶 )
12		fucoaltnelem.j	⊢ 𝐽 = ( Id ‘ ( 𝐶 FuncCat 𝐶 ) )
13		simpr	⊢ ( ( 𝜑 ∧ ( 2^nd ‘ ( 𝐾 ∘_func 𝐿 ) ) = ( 2^nd ‘ 𝐿 ) ) → ( 2^nd ‘ ( 𝐾 ∘_func 𝐿 ) ) = ( 2^nd ‘ 𝐿 ) )
14	13	oveqd	⊢ ( ( 𝜑 ∧ ( 2^nd ‘ ( 𝐾 ∘_func 𝐿 ) ) = ( 2^nd ‘ 𝐿 ) ) → ( ⟨ 𝐹 , 𝐼 ⟩ ( 2^nd ‘ ( 𝐾 ∘_func 𝐿 ) ) ⟨ 𝐺 , 𝐼 ⟩ ) = ( ⟨ 𝐹 , 𝐼 ⟩ ( 2^nd ‘ 𝐿 ) ⟨ 𝐺 , 𝐼 ⟩ ) )
15	14	oveqd	⊢ ( ( 𝜑 ∧ ( 2^nd ‘ ( 𝐾 ∘_func 𝐿 ) ) = ( 2^nd ‘ 𝐿 ) ) → ( 𝐴 ( ⟨ 𝐹 , 𝐼 ⟩ ( 2^nd ‘ ( 𝐾 ∘_func 𝐿 ) ) ⟨ 𝐺 , 𝐼 ⟩ ) ( 𝐽 ‘ 𝐼 ) ) = ( 𝐴 ( ⟨ 𝐹 , 𝐼 ⟩ ( 2^nd ‘ 𝐿 ) ⟨ 𝐺 , 𝐼 ⟩ ) ( 𝐽 ‘ 𝐼 ) ) )
16	1 2 3 4 5 6 7 8 11 12	fucoaltval	⊢ ( 𝜑 → ( 𝐴 ( ⟨ 𝐹 , 𝐼 ⟩ ( 2^nd ‘ ( 𝐾 ∘_func 𝐿 ) ) ⟨ 𝐺 , 𝐼 ⟩ ) ( 𝐽 ‘ 𝐼 ) ) = ( ( 𝐹 ( 2^nd ‘ 𝐾 ) 𝐺 ) ‘ 𝐴 ) )
17	16	adantr	⊢ ( ( 𝜑 ∧ ( 2^nd ‘ ( 𝐾 ∘_func 𝐿 ) ) = ( 2^nd ‘ 𝐿 ) ) → ( 𝐴 ( ⟨ 𝐹 , 𝐼 ⟩ ( 2^nd ‘ ( 𝐾 ∘_func 𝐿 ) ) ⟨ 𝐺 , 𝐼 ⟩ ) ( 𝐽 ‘ 𝐼 ) ) = ( ( 𝐹 ( 2^nd ‘ 𝐾 ) 𝐺 ) ‘ 𝐴 ) )
18	2	eqcomi	⊢ ( ⟨ 𝐶 , 𝐶 ⟩ ∘_F 𝐸 ) = 𝐿
19	18	fveq2i	⊢ ( 2^nd ‘ ( ⟨ 𝐶 , 𝐶 ⟩ ∘_F 𝐸 ) ) = ( 2^nd ‘ 𝐿 )
20	19	a1i	⊢ ( 𝜑 → ( 2^nd ‘ ( ⟨ 𝐶 , 𝐶 ⟩ ∘_F 𝐸 ) ) = ( 2^nd ‘ 𝐿 ) )
21		eqid	⊢ ( 𝐶 FuncCat 𝐶 ) = ( 𝐶 FuncCat 𝐶 )
22	20 21 12 11 3 8	fucoridid	⊢ ( 𝜑 → ( 𝐴 ( ⟨ 𝐹 , 𝐼 ⟩ ( 2^nd ‘ 𝐿 ) ⟨ 𝐺 , 𝐼 ⟩ ) ( 𝐽 ‘ 𝐼 ) ) = 𝐴 )
23	22	adantr	⊢ ( ( 𝜑 ∧ ( 2^nd ‘ ( 𝐾 ∘_func 𝐿 ) ) = ( 2^nd ‘ 𝐿 ) ) → ( 𝐴 ( ⟨ 𝐹 , 𝐼 ⟩ ( 2^nd ‘ 𝐿 ) ⟨ 𝐺 , 𝐼 ⟩ ) ( 𝐽 ‘ 𝐼 ) ) = 𝐴 )
24	15 17 23	3eqtr3d	⊢ ( ( 𝜑 ∧ ( 2^nd ‘ ( 𝐾 ∘_func 𝐿 ) ) = ( 2^nd ‘ 𝐿 ) ) → ( ( 𝐹 ( 2^nd ‘ 𝐾 ) 𝐺 ) ‘ 𝐴 ) = 𝐴 )
25	9 24	mteqand	⊢ ( 𝜑 → ( 2^nd ‘ ( 𝐾 ∘_func 𝐿 ) ) ≠ ( 2^nd ‘ 𝐿 ) )

Metamath Proof Explorer

Theorem fucoaltnelem

Proof