swapf2f1oa

Description: The morphism part of the swap functor is a bijection between hom-sets. (Contributed by Zhi Wang, 9-Oct-2025)

	Ref	Expression
Hypotheses	swapf1f1o.o	⊢ ( 𝜑 → ( 𝐶 swap_F 𝐷 ) = ⟨ 𝑂 , 𝑃 ⟩ )
	swapf1f1o.s	⊢ 𝑆 = ( 𝐶 ×_c 𝐷 )
	swapf1f1o.t	⊢ 𝑇 = ( 𝐷 ×_c 𝐶 )
	swapf2f1o.h	⊢ 𝐻 = ( Hom ‘ 𝑆 )
	swapf2f1o.j	⊢ 𝐽 = ( Hom ‘ 𝑇 )
	swapf2f1oa.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
	swapf2f1oa.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	swapf2f1oa.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
Assertion	swapf2f1oa	⊢ ( 𝜑 → ( 𝑋 𝑃 𝑌 ) : ( 𝑋 𝐻 𝑌 ) –1-1-onto→ ( ( 𝑂 ‘ 𝑋 ) 𝐽 ( 𝑂 ‘ 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		swapf1f1o.o	⊢ ( 𝜑 → ( 𝐶 swap_F 𝐷 ) = ⟨ 𝑂 , 𝑃 ⟩ )
2		swapf1f1o.s	⊢ 𝑆 = ( 𝐶 ×_c 𝐷 )
3		swapf1f1o.t	⊢ 𝑇 = ( 𝐷 ×_c 𝐶 )
4		swapf2f1o.h	⊢ 𝐻 = ( Hom ‘ 𝑆 )
5		swapf2f1o.j	⊢ 𝐽 = ( Hom ‘ 𝑇 )
6		swapf2f1oa.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
7		swapf2f1oa.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
8		swapf2f1oa.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
9		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
10		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
11	2 9 10	xpcbas	⊢ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) = ( Base ‘ 𝑆 )
12	6 11	eqtr4i	⊢ 𝐵 = ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) )
13	7 12	eleqtrdi	⊢ ( 𝜑 → 𝑋 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
14		xp1st	⊢ ( 𝑋 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) → ( 1^st ‘ 𝑋 ) ∈ ( Base ‘ 𝐶 ) )
15	13 14	syl	⊢ ( 𝜑 → ( 1^st ‘ 𝑋 ) ∈ ( Base ‘ 𝐶 ) )
16		xp2nd	⊢ ( 𝑋 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) → ( 2^nd ‘ 𝑋 ) ∈ ( Base ‘ 𝐷 ) )
17	13 16	syl	⊢ ( 𝜑 → ( 2^nd ‘ 𝑋 ) ∈ ( Base ‘ 𝐷 ) )
18	8 12	eleqtrdi	⊢ ( 𝜑 → 𝑌 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) )
19		xp1st	⊢ ( 𝑌 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) → ( 1^st ‘ 𝑌 ) ∈ ( Base ‘ 𝐶 ) )
20	18 19	syl	⊢ ( 𝜑 → ( 1^st ‘ 𝑌 ) ∈ ( Base ‘ 𝐶 ) )
21		xp2nd	⊢ ( 𝑌 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) → ( 2^nd ‘ 𝑌 ) ∈ ( Base ‘ 𝐷 ) )
22	18 21	syl	⊢ ( 𝜑 → ( 2^nd ‘ 𝑌 ) ∈ ( Base ‘ 𝐷 ) )
23	1 2 3 4 5 15 17 20 22	swapf2f1o	⊢ ( 𝜑 → ( ⟨ ( 1^st ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) ⟩ 𝑃 ⟨ ( 1^st ‘ 𝑌 ) , ( 2^nd ‘ 𝑌 ) ⟩ ) : ( ⟨ ( 1^st ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) ⟩ 𝐻 ⟨ ( 1^st ‘ 𝑌 ) , ( 2^nd ‘ 𝑌 ) ⟩ ) –1-1-onto→ ( ⟨ ( 2^nd ‘ 𝑋 ) , ( 1^st ‘ 𝑋 ) ⟩ 𝐽 ⟨ ( 2^nd ‘ 𝑌 ) , ( 1^st ‘ 𝑌 ) ⟩ ) )
24		1st2nd2	⊢ ( 𝑋 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) → 𝑋 = ⟨ ( 1^st ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) ⟩ )
25	13 24	syl	⊢ ( 𝜑 → 𝑋 = ⟨ ( 1^st ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) ⟩ )
26		1st2nd2	⊢ ( 𝑌 ∈ ( ( Base ‘ 𝐶 ) × ( Base ‘ 𝐷 ) ) → 𝑌 = ⟨ ( 1^st ‘ 𝑌 ) , ( 2^nd ‘ 𝑌 ) ⟩ )
27	18 26	syl	⊢ ( 𝜑 → 𝑌 = ⟨ ( 1^st ‘ 𝑌 ) , ( 2^nd ‘ 𝑌 ) ⟩ )
28	25 27	oveq12d	⊢ ( 𝜑 → ( 𝑋 𝑃 𝑌 ) = ( ⟨ ( 1^st ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) ⟩ 𝑃 ⟨ ( 1^st ‘ 𝑌 ) , ( 2^nd ‘ 𝑌 ) ⟩ ) )
29	25 27	oveq12d	⊢ ( 𝜑 → ( 𝑋 𝐻 𝑌 ) = ( ⟨ ( 1^st ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) ⟩ 𝐻 ⟨ ( 1^st ‘ 𝑌 ) , ( 2^nd ‘ 𝑌 ) ⟩ ) )
30	1 2 6 7	swapf1a	⊢ ( 𝜑 → ( 𝑂 ‘ 𝑋 ) = ⟨ ( 2^nd ‘ 𝑋 ) , ( 1^st ‘ 𝑋 ) ⟩ )
31	1 2 6 8	swapf1a	⊢ ( 𝜑 → ( 𝑂 ‘ 𝑌 ) = ⟨ ( 2^nd ‘ 𝑌 ) , ( 1^st ‘ 𝑌 ) ⟩ )
32	30 31	oveq12d	⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝑋 ) 𝐽 ( 𝑂 ‘ 𝑌 ) ) = ( ⟨ ( 2^nd ‘ 𝑋 ) , ( 1^st ‘ 𝑋 ) ⟩ 𝐽 ⟨ ( 2^nd ‘ 𝑌 ) , ( 1^st ‘ 𝑌 ) ⟩ ) )
33	28 29 32	f1oeq123d	⊢ ( 𝜑 → ( ( 𝑋 𝑃 𝑌 ) : ( 𝑋 𝐻 𝑌 ) –1-1-onto→ ( ( 𝑂 ‘ 𝑋 ) 𝐽 ( 𝑂 ‘ 𝑌 ) ) ↔ ( ⟨ ( 1^st ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) ⟩ 𝑃 ⟨ ( 1^st ‘ 𝑌 ) , ( 2^nd ‘ 𝑌 ) ⟩ ) : ( ⟨ ( 1^st ‘ 𝑋 ) , ( 2^nd ‘ 𝑋 ) ⟩ 𝐻 ⟨ ( 1^st ‘ 𝑌 ) , ( 2^nd ‘ 𝑌 ) ⟩ ) –1-1-onto→ ( ⟨ ( 2^nd ‘ 𝑋 ) , ( 1^st ‘ 𝑋 ) ⟩ 𝐽 ⟨ ( 2^nd ‘ 𝑌 ) , ( 1^st ‘ 𝑌 ) ⟩ ) ) )
34	23 33	mpbird	⊢ ( 𝜑 → ( 𝑋 𝑃 𝑌 ) : ( 𝑋 𝐻 𝑌 ) –1-1-onto→ ( ( 𝑂 ‘ 𝑋 ) 𝐽 ( 𝑂 ‘ 𝑌 ) ) )

Metamath Proof Explorer

Theorem swapf2f1oa

Proof