fucoid2

Description: Each identity morphism in the source category is mapped to the corresponding identity morphism in the target category. See also fucoid . (Contributed by Zhi Wang, 30-Sep-2025)

	Ref	Expression
Hypotheses	fucoid.o	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) = ⟨ 𝑂 , 𝑃 ⟩ )
	fucoid.t	⊢ 𝑇 = ( ( 𝐷 FuncCat 𝐸 ) ×_c ( 𝐶 FuncCat 𝐷 ) )
	fucoid.1	⊢ 1 = ( Id ‘ 𝑇 )
	fucoid.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐸 )
	fucoid.i	⊢ 𝐼 = ( Id ‘ 𝑄 )
	fucoid2.w	⊢ ( 𝜑 → 𝑊 = ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) )
	fucoid2.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑊 )
Assertion	fucoid2	⊢ ( 𝜑 → ( ( 𝑈 𝑃 𝑈 ) ‘ ( 1 ‘ 𝑈 ) ) = ( 𝐼 ‘ ( 𝑂 ‘ 𝑈 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fucoid.o	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) = ⟨ 𝑂 , 𝑃 ⟩ )
2		fucoid.t	⊢ 𝑇 = ( ( 𝐷 FuncCat 𝐸 ) ×_c ( 𝐶 FuncCat 𝐷 ) )
3		fucoid.1	⊢ 1 = ( Id ‘ 𝑇 )
4		fucoid.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐸 )
5		fucoid.i	⊢ 𝐼 = ( Id ‘ 𝑄 )
6		fucoid2.w	⊢ ( 𝜑 → 𝑊 = ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) )
7		fucoid2.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑊 )
8		relfunc	⊢ Rel ( 𝐷 Func 𝐸 )
9		relfunc	⊢ Rel ( 𝐶 Func 𝐷 )
10	6 7 8 9	fuco2eld2	⊢ ( 𝜑 → 𝑈 = ⟨ ⟨ ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ⟩ , ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑈 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑈 ) ) ⟩ ⟩ )
11	7 10 6	3eltr3d	⊢ ( 𝜑 → ⟨ ⟨ ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ⟩ , ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑈 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑈 ) ) ⟩ ⟩ ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) )
12		opelxp2	⊢ ( ⟨ ⟨ ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ⟩ , ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑈 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑈 ) ) ⟩ ⟩ ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) → ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑈 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑈 ) ) ⟩ ∈ ( 𝐶 Func 𝐷 ) )
13	11 12	syl	⊢ ( 𝜑 → ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑈 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑈 ) ) ⟩ ∈ ( 𝐶 Func 𝐷 ) )
14		df-br	⊢ ( ( 1^st ‘ ( 2^nd ‘ 𝑈 ) ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ ( 2^nd ‘ 𝑈 ) ) ↔ ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑈 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑈 ) ) ⟩ ∈ ( 𝐶 Func 𝐷 ) )
15	13 14	sylibr	⊢ ( 𝜑 → ( 1^st ‘ ( 2^nd ‘ 𝑈 ) ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ ( 2^nd ‘ 𝑈 ) ) )
16		opelxp1	⊢ ( ⟨ ⟨ ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ⟩ , ⟨ ( 1^st ‘ ( 2^nd ‘ 𝑈 ) ) , ( 2^nd ‘ ( 2^nd ‘ 𝑈 ) ) ⟩ ⟩ ∈ ( ( 𝐷 Func 𝐸 ) × ( 𝐶 Func 𝐷 ) ) → ⟨ ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ⟩ ∈ ( 𝐷 Func 𝐸 ) )
17	11 16	syl	⊢ ( 𝜑 → ⟨ ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ⟩ ∈ ( 𝐷 Func 𝐸 ) )
18		df-br	⊢ ( ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ↔ ⟨ ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) , ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) ⟩ ∈ ( 𝐷 Func 𝐸 ) )
19	17 18	sylibr	⊢ ( 𝜑 → ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ ( 1^st ‘ 𝑈 ) ) )
20	1 2 3 4 5 15 19 10	fucoid	⊢ ( 𝜑 → ( ( 𝑈 𝑃 𝑈 ) ‘ ( 1 ‘ 𝑈 ) ) = ( 𝐼 ‘ ( 𝑂 ‘ 𝑈 ) ) )

Metamath Proof Explorer

Theorem fucoid2

Proof