Theorem 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	No typesetting found for |- ( ph -> ( C swapF D ) = <. O , P >. ) with typecode |-
	swapf1f1o.s	$$⊢S=C{\times }_{c}D$$
	swapf1f1o.t	$$⊢T=D{\times }_{c}C$$
	swapf2f1o.h	$$⊢H=\mathrm{Hom}\left(S\right)$$
	swapf2f1o.j	$$⊢J=\mathrm{Hom}\left(T\right)$$
	swapf2f1oa.b	$$⊢B={\mathrm{Base}}_S$$
	swapf2f1oa.x	$$⊢\phi \to X\in B$$
	swapf2f1oa.y	$$⊢\phi \to Y\in B$$
Assertion	swapf2f1oaALT	$$⊢\phi \to \left(XPY\right):XHY\underset{1-1\; onto}{⟶}O\left(X\right)JO\left(Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		swapf1f1o.o	Could not format ( ph -> ( C swapF D ) = <. O , P >. ) : No typesetting found for |- ( ph -> ( C swapF D ) = <. O , P >. ) with typecode |-
2		swapf1f1o.s	$$⊢S=C{\times }_{c}D$$
3		swapf1f1o.t	$$⊢T=D{\times }_{c}C$$
4		swapf2f1o.h	$$⊢H=\mathrm{Hom}\left(S\right)$$
5		swapf2f1o.j	$$⊢J=\mathrm{Hom}\left(T\right)$$
6		swapf2f1oa.b	$$⊢B={\mathrm{Base}}_S$$
7		swapf2f1oa.x	$$⊢\phi \to X\in B$$
8		swapf2f1oa.y	$$⊢\phi \to Y\in B$$
9		eqid	$$⊢\left(f\in \left(\left(1^{st}\left(X\right)\mathrm{Hom}\left(C\right)1^{st}\left(Y\right)\right)\times \left(2^{nd}\left(X\right)\mathrm{Hom}\left(D\right)2^{nd}\left(Y\right)\right)\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)=\left(f\in \left(\left(1^{st}\left(X\right)\mathrm{Hom}\left(C\right)1^{st}\left(Y\right)\right)\times \left(2^{nd}\left(X\right)\mathrm{Hom}\left(D\right)2^{nd}\left(Y\right)\right)\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)$$
10	9	xpcomf1o	$$⊢\left(f\in \left(\left(1^{st}\left(X\right)\mathrm{Hom}\left(C\right)1^{st}\left(Y\right)\right)\times \left(2^{nd}\left(X\right)\mathrm{Hom}\left(D\right)2^{nd}\left(Y\right)\right)\right)⟼\bigcup {\left\{f\right\}}^{-1}\right):\left(1^{st}\left(X\right)\mathrm{Hom}\left(C\right)1^{st}\left(Y\right)\right)\times \left(2^{nd}\left(X\right)\mathrm{Hom}\left(D\right)2^{nd}\left(Y\right)\right)\underset{1-1\; onto}{⟶}\left(2^{nd}\left(X\right)\mathrm{Hom}\left(D\right)2^{nd}\left(Y\right)\right)\times \left(1^{st}\left(X\right)\mathrm{Hom}\left(C\right)1^{st}\left(Y\right)\right)$$
11	4	a1i	$$⊢\phi \to H=\mathrm{Hom}\left(S\right)$$
12	1 2 6 7 8 11	swapf2vala	$$⊢\phi \to XPY=\left(f\in \left(XHY\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)$$
13		eqid	$$⊢\mathrm{Hom}\left(C\right)=\mathrm{Hom}\left(C\right)$$
14		eqid	$$⊢\mathrm{Hom}\left(D\right)=\mathrm{Hom}\left(D\right)$$
15	2 6 13 14 4 7 8	xpchom	$$⊢\phi \to XHY=\left(1^{st}\left(X\right)\mathrm{Hom}\left(C\right)1^{st}\left(Y\right)\right)\times \left(2^{nd}\left(X\right)\mathrm{Hom}\left(D\right)2^{nd}\left(Y\right)\right)$$
16	15	mpteq1d	$$⊢\phi \to \left(f\in \left(XHY\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)=\left(f\in \left(\left(1^{st}\left(X\right)\mathrm{Hom}\left(C\right)1^{st}\left(Y\right)\right)\times \left(2^{nd}\left(X\right)\mathrm{Hom}\left(D\right)2^{nd}\left(Y\right)\right)\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)$$
17	12 16	eqtrd	$$⊢\phi \to XPY=\left(f\in \left(\left(1^{st}\left(X\right)\mathrm{Hom}\left(C\right)1^{st}\left(Y\right)\right)\times \left(2^{nd}\left(X\right)\mathrm{Hom}\left(D\right)2^{nd}\left(Y\right)\right)\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)$$
18		eqid	$$⊢{\mathrm{Base}}_T={\mathrm{Base}}_T$$
19	2 6 7	elxpcbasex1	$$⊢\phi \to C\in \mathrm{V}$$
20	2 6 7	elxpcbasex2	$$⊢\phi \to D\in \mathrm{V}$$
21	1 2 3 19 20 6 18	swapf1f1o	$$⊢\phi \to O:B\underset{1-1\; onto}{⟶}{\mathrm{Base}}_T$$
22		f1of	$$⊢O:B\underset{1-1\; onto}{⟶}{\mathrm{Base}}_T\to O:B⟶{\mathrm{Base}}_T$$
23	21 22	syl	$$⊢\phi \to O:B⟶{\mathrm{Base}}_T$$
24	23 7	ffvelcdmd	$$⊢\phi \to O\left(X\right)\in {\mathrm{Base}}_T$$
25	23 8	ffvelcdmd	$$⊢\phi \to O\left(Y\right)\in {\mathrm{Base}}_T$$
26	3 18 14 13 5 24 25	xpchom	$$⊢\phi \to O\left(X\right)JO\left(Y\right)=\left(1^{st}\left(O\left(X\right)\right)\mathrm{Hom}\left(D\right)1^{st}\left(O\left(Y\right)\right)\right)\times \left(2^{nd}\left(O\left(X\right)\right)\mathrm{Hom}\left(C\right)2^{nd}\left(O\left(Y\right)\right)\right)$$
27	1 2 6 7	swapf1a	$$⊢\phi \to O\left(X\right)=⟨2^{nd}\left(X\right),1^{st}\left(X\right)⟩$$
28	27	fveq2d	$$⊢\phi \to 1^{st}\left(O\left(X\right)\right)=1^{st}\left(⟨2^{nd}\left(X\right),1^{st}\left(X\right)⟩\right)$$
29		fvex	$$⊢2^{nd}\left(X\right)\in \mathrm{V}$$
30		fvex	$$⊢1^{st}\left(X\right)\in \mathrm{V}$$
31	29 30	op1st	$$⊢1^{st}\left(⟨2^{nd}\left(X\right),1^{st}\left(X\right)⟩\right)=2^{nd}\left(X\right)$$
32	28 31	eqtrdi	$$⊢\phi \to 1^{st}\left(O\left(X\right)\right)=2^{nd}\left(X\right)$$
33	1 2 6 8	swapf1a	$$⊢\phi \to O\left(Y\right)=⟨2^{nd}\left(Y\right),1^{st}\left(Y\right)⟩$$
34	33	fveq2d	$$⊢\phi \to 1^{st}\left(O\left(Y\right)\right)=1^{st}\left(⟨2^{nd}\left(Y\right),1^{st}\left(Y\right)⟩\right)$$
35		fvex	$$⊢2^{nd}\left(Y\right)\in \mathrm{V}$$
36		fvex	$$⊢1^{st}\left(Y\right)\in \mathrm{V}$$
37	35 36	op1st	$$⊢1^{st}\left(⟨2^{nd}\left(Y\right),1^{st}\left(Y\right)⟩\right)=2^{nd}\left(Y\right)$$
38	34 37	eqtrdi	$$⊢\phi \to 1^{st}\left(O\left(Y\right)\right)=2^{nd}\left(Y\right)$$
39	32 38	oveq12d	$$⊢\phi \to 1^{st}\left(O\left(X\right)\right)\mathrm{Hom}\left(D\right)1^{st}\left(O\left(Y\right)\right)=2^{nd}\left(X\right)\mathrm{Hom}\left(D\right)2^{nd}\left(Y\right)$$
40	27	fveq2d	$$⊢\phi \to 2^{nd}\left(O\left(X\right)\right)=2^{nd}\left(⟨2^{nd}\left(X\right),1^{st}\left(X\right)⟩\right)$$
41	29 30	op2nd	$$⊢2^{nd}\left(⟨2^{nd}\left(X\right),1^{st}\left(X\right)⟩\right)=1^{st}\left(X\right)$$
42	40 41	eqtrdi	$$⊢\phi \to 2^{nd}\left(O\left(X\right)\right)=1^{st}\left(X\right)$$
43	33	fveq2d	$$⊢\phi \to 2^{nd}\left(O\left(Y\right)\right)=2^{nd}\left(⟨2^{nd}\left(Y\right),1^{st}\left(Y\right)⟩\right)$$
44	35 36	op2nd	$$⊢2^{nd}\left(⟨2^{nd}\left(Y\right),1^{st}\left(Y\right)⟩\right)=1^{st}\left(Y\right)$$
45	43 44	eqtrdi	$$⊢\phi \to 2^{nd}\left(O\left(Y\right)\right)=1^{st}\left(Y\right)$$
46	42 45	oveq12d	$$⊢\phi \to 2^{nd}\left(O\left(X\right)\right)\mathrm{Hom}\left(C\right)2^{nd}\left(O\left(Y\right)\right)=1^{st}\left(X\right)\mathrm{Hom}\left(C\right)1^{st}\left(Y\right)$$
47	39 46	xpeq12d	$$⊢\phi \to \left(1^{st}\left(O\left(X\right)\right)\mathrm{Hom}\left(D\right)1^{st}\left(O\left(Y\right)\right)\right)\times \left(2^{nd}\left(O\left(X\right)\right)\mathrm{Hom}\left(C\right)2^{nd}\left(O\left(Y\right)\right)\right)=\left(2^{nd}\left(X\right)\mathrm{Hom}\left(D\right)2^{nd}\left(Y\right)\right)\times \left(1^{st}\left(X\right)\mathrm{Hom}\left(C\right)1^{st}\left(Y\right)\right)$$
48	26 47	eqtrd	$$⊢\phi \to O\left(X\right)JO\left(Y\right)=\left(2^{nd}\left(X\right)\mathrm{Hom}\left(D\right)2^{nd}\left(Y\right)\right)\times \left(1^{st}\left(X\right)\mathrm{Hom}\left(C\right)1^{st}\left(Y\right)\right)$$
49	17 15 48	f1oeq123d	$$⊢\phi \to \left(\left(XPY\right):XHY\underset{1-1\; onto}{⟶}O\left(X\right)JO\left(Y\right)\leftrightarrow \left(f\in \left(\left(1^{st}\left(X\right)\mathrm{Hom}\left(C\right)1^{st}\left(Y\right)\right)\times \left(2^{nd}\left(X\right)\mathrm{Hom}\left(D\right)2^{nd}\left(Y\right)\right)\right)⟼\bigcup {\left\{f\right\}}^{-1}\right):\left(1^{st}\left(X\right)\mathrm{Hom}\left(C\right)1^{st}\left(Y\right)\right)\times \left(2^{nd}\left(X\right)\mathrm{Hom}\left(D\right)2^{nd}\left(Y\right)\right)\underset{1-1\; onto}{⟶}\left(2^{nd}\left(X\right)\mathrm{Hom}\left(D\right)2^{nd}\left(Y\right)\right)\times \left(1^{st}\left(X\right)\mathrm{Hom}\left(C\right)1^{st}\left(Y\right)\right)\right)$$
50	10 49	mpbiri	$$⊢\phi \to \left(XPY\right):XHY\underset{1-1\; onto}{⟶}O\left(X\right)JO\left(Y\right)$$