swapf2f1oaALT

Description: Alternate proof of swapf2f1oa . (Contributed by Zhi Wang, 8-Oct-2025) (Proof modification is discouraged.) (New usage is discouraged.)

	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	swapf2f1oaALT	⊢ ( 𝜑 → ( 𝑋 𝑃 𝑌 ) : ( 𝑋 𝐻 𝑌 ) –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	⊢ ( 𝑓 ∈ ( ( ( 1^st ‘ 𝑋 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑌 ) ) × ( ( 2^nd ‘ 𝑋 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑌 ) ) ) ↦ ∪ ^◡ { 𝑓 } ) = ( 𝑓 ∈ ( ( ( 1^st ‘ 𝑋 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑌 ) ) × ( ( 2^nd ‘ 𝑋 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑌 ) ) ) ↦ ∪ ^◡ { 𝑓 } )
10	9	xpcomf1o	⊢ ( 𝑓 ∈ ( ( ( 1^st ‘ 𝑋 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑌 ) ) × ( ( 2^nd ‘ 𝑋 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑌 ) ) ) ↦ ∪ ^◡ { 𝑓 } ) : ( ( ( 1^st ‘ 𝑋 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑌 ) ) × ( ( 2^nd ‘ 𝑋 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑌 ) ) ) –1-1-onto→ ( ( ( 2^nd ‘ 𝑋 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑌 ) ) × ( ( 1^st ‘ 𝑋 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑌 ) ) )
11	4	a1i	⊢ ( 𝜑 → 𝐻 = ( Hom ‘ 𝑆 ) )
12	1 2 6 7 8 11	swapf2vala	⊢ ( 𝜑 → ( 𝑋 𝑃 𝑌 ) = ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ↦ ∪ ^◡ { 𝑓 } ) )
13		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
14		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
15	2 6 13 14 4 7 8	xpchom	⊢ ( 𝜑 → ( 𝑋 𝐻 𝑌 ) = ( ( ( 1^st ‘ 𝑋 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑌 ) ) × ( ( 2^nd ‘ 𝑋 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑌 ) ) ) )
16	15	mpteq1d	⊢ ( 𝜑 → ( 𝑓 ∈ ( 𝑋 𝐻 𝑌 ) ↦ ∪ ^◡ { 𝑓 } ) = ( 𝑓 ∈ ( ( ( 1^st ‘ 𝑋 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑌 ) ) × ( ( 2^nd ‘ 𝑋 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑌 ) ) ) ↦ ∪ ^◡ { 𝑓 } ) )
17	12 16	eqtrd	⊢ ( 𝜑 → ( 𝑋 𝑃 𝑌 ) = ( 𝑓 ∈ ( ( ( 1^st ‘ 𝑋 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑌 ) ) × ( ( 2^nd ‘ 𝑋 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑌 ) ) ) ↦ ∪ ^◡ { 𝑓 } ) )
18		eqid	⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
19	2 6 7	elxpcbasex1	⊢ ( 𝜑 → 𝐶 ∈ V )
20	2 6 7	elxpcbasex2	⊢ ( 𝜑 → 𝐷 ∈ V )
21	1 2 3 19 20 6 18	swapf1f1o	⊢ ( 𝜑 → 𝑂 : 𝐵 –1-1-onto→ ( Base ‘ 𝑇 ) )
22		f1of	⊢ ( 𝑂 : 𝐵 –1-1-onto→ ( Base ‘ 𝑇 ) → 𝑂 : 𝐵 ⟶ ( Base ‘ 𝑇 ) )
23	21 22	syl	⊢ ( 𝜑 → 𝑂 : 𝐵 ⟶ ( Base ‘ 𝑇 ) )
24	23 7	ffvelcdmd	⊢ ( 𝜑 → ( 𝑂 ‘ 𝑋 ) ∈ ( Base ‘ 𝑇 ) )
25	23 8	ffvelcdmd	⊢ ( 𝜑 → ( 𝑂 ‘ 𝑌 ) ∈ ( Base ‘ 𝑇 ) )
26	3 18 14 13 5 24 25	xpchom	⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝑋 ) 𝐽 ( 𝑂 ‘ 𝑌 ) ) = ( ( ( 1^st ‘ ( 𝑂 ‘ 𝑋 ) ) ( Hom ‘ 𝐷 ) ( 1^st ‘ ( 𝑂 ‘ 𝑌 ) ) ) × ( ( 2^nd ‘ ( 𝑂 ‘ 𝑋 ) ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ ( 𝑂 ‘ 𝑌 ) ) ) ) )
27	1 2 6 7	swapf1a	⊢ ( 𝜑 → ( 𝑂 ‘ 𝑋 ) = ⟨ ( 2^nd ‘ 𝑋 ) , ( 1^st ‘ 𝑋 ) ⟩ )
28	27	fveq2d	⊢ ( 𝜑 → ( 1^st ‘ ( 𝑂 ‘ 𝑋 ) ) = ( 1^st ‘ ⟨ ( 2^nd ‘ 𝑋 ) , ( 1^st ‘ 𝑋 ) ⟩ ) )
29		fvex	⊢ ( 2^nd ‘ 𝑋 ) ∈ V
30		fvex	⊢ ( 1^st ‘ 𝑋 ) ∈ V
31	29 30	op1st	⊢ ( 1^st ‘ ⟨ ( 2^nd ‘ 𝑋 ) , ( 1^st ‘ 𝑋 ) ⟩ ) = ( 2^nd ‘ 𝑋 )
32	28 31	eqtrdi	⊢ ( 𝜑 → ( 1^st ‘ ( 𝑂 ‘ 𝑋 ) ) = ( 2^nd ‘ 𝑋 ) )
33	1 2 6 8	swapf1a	⊢ ( 𝜑 → ( 𝑂 ‘ 𝑌 ) = ⟨ ( 2^nd ‘ 𝑌 ) , ( 1^st ‘ 𝑌 ) ⟩ )
34	33	fveq2d	⊢ ( 𝜑 → ( 1^st ‘ ( 𝑂 ‘ 𝑌 ) ) = ( 1^st ‘ ⟨ ( 2^nd ‘ 𝑌 ) , ( 1^st ‘ 𝑌 ) ⟩ ) )
35		fvex	⊢ ( 2^nd ‘ 𝑌 ) ∈ V
36		fvex	⊢ ( 1^st ‘ 𝑌 ) ∈ V
37	35 36	op1st	⊢ ( 1^st ‘ ⟨ ( 2^nd ‘ 𝑌 ) , ( 1^st ‘ 𝑌 ) ⟩ ) = ( 2^nd ‘ 𝑌 )
38	34 37	eqtrdi	⊢ ( 𝜑 → ( 1^st ‘ ( 𝑂 ‘ 𝑌 ) ) = ( 2^nd ‘ 𝑌 ) )
39	32 38	oveq12d	⊢ ( 𝜑 → ( ( 1^st ‘ ( 𝑂 ‘ 𝑋 ) ) ( Hom ‘ 𝐷 ) ( 1^st ‘ ( 𝑂 ‘ 𝑌 ) ) ) = ( ( 2^nd ‘ 𝑋 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑌 ) ) )
40	27	fveq2d	⊢ ( 𝜑 → ( 2^nd ‘ ( 𝑂 ‘ 𝑋 ) ) = ( 2^nd ‘ ⟨ ( 2^nd ‘ 𝑋 ) , ( 1^st ‘ 𝑋 ) ⟩ ) )
41	29 30	op2nd	⊢ ( 2^nd ‘ ⟨ ( 2^nd ‘ 𝑋 ) , ( 1^st ‘ 𝑋 ) ⟩ ) = ( 1^st ‘ 𝑋 )
42	40 41	eqtrdi	⊢ ( 𝜑 → ( 2^nd ‘ ( 𝑂 ‘ 𝑋 ) ) = ( 1^st ‘ 𝑋 ) )
43	33	fveq2d	⊢ ( 𝜑 → ( 2^nd ‘ ( 𝑂 ‘ 𝑌 ) ) = ( 2^nd ‘ ⟨ ( 2^nd ‘ 𝑌 ) , ( 1^st ‘ 𝑌 ) ⟩ ) )
44	35 36	op2nd	⊢ ( 2^nd ‘ ⟨ ( 2^nd ‘ 𝑌 ) , ( 1^st ‘ 𝑌 ) ⟩ ) = ( 1^st ‘ 𝑌 )
45	43 44	eqtrdi	⊢ ( 𝜑 → ( 2^nd ‘ ( 𝑂 ‘ 𝑌 ) ) = ( 1^st ‘ 𝑌 ) )
46	42 45	oveq12d	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 𝑂 ‘ 𝑋 ) ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ ( 𝑂 ‘ 𝑌 ) ) ) = ( ( 1^st ‘ 𝑋 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑌 ) ) )
47	39 46	xpeq12d	⊢ ( 𝜑 → ( ( ( 1^st ‘ ( 𝑂 ‘ 𝑋 ) ) ( Hom ‘ 𝐷 ) ( 1^st ‘ ( 𝑂 ‘ 𝑌 ) ) ) × ( ( 2^nd ‘ ( 𝑂 ‘ 𝑋 ) ) ( Hom ‘ 𝐶 ) ( 2^nd ‘ ( 𝑂 ‘ 𝑌 ) ) ) ) = ( ( ( 2^nd ‘ 𝑋 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑌 ) ) × ( ( 1^st ‘ 𝑋 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑌 ) ) ) )
48	26 47	eqtrd	⊢ ( 𝜑 → ( ( 𝑂 ‘ 𝑋 ) 𝐽 ( 𝑂 ‘ 𝑌 ) ) = ( ( ( 2^nd ‘ 𝑋 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑌 ) ) × ( ( 1^st ‘ 𝑋 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑌 ) ) ) )
49	17 15 48	f1oeq123d	⊢ ( 𝜑 → ( ( 𝑋 𝑃 𝑌 ) : ( 𝑋 𝐻 𝑌 ) –1-1-onto→ ( ( 𝑂 ‘ 𝑋 ) 𝐽 ( 𝑂 ‘ 𝑌 ) ) ↔ ( 𝑓 ∈ ( ( ( 1^st ‘ 𝑋 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑌 ) ) × ( ( 2^nd ‘ 𝑋 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑌 ) ) ) ↦ ∪ ^◡ { 𝑓 } ) : ( ( ( 1^st ‘ 𝑋 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑌 ) ) × ( ( 2^nd ‘ 𝑋 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑌 ) ) ) –1-1-onto→ ( ( ( 2^nd ‘ 𝑋 ) ( Hom ‘ 𝐷 ) ( 2^nd ‘ 𝑌 ) ) × ( ( 1^st ‘ 𝑋 ) ( Hom ‘ 𝐶 ) ( 1^st ‘ 𝑌 ) ) ) ) )
50	10 49	mpbiri	⊢ ( 𝜑 → ( 𝑋 𝑃 𝑌 ) : ( 𝑋 𝐻 𝑌 ) –1-1-onto→ ( ( 𝑂 ‘ 𝑋 ) 𝐽 ( 𝑂 ‘ 𝑌 ) ) )

Metamath Proof Explorer

Theorem swapf2f1oaALT

Proof