Theorem swapf1f1o

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

	Ref	Expression
Hypotheses	swapf1f1o.o	|- ( ph -> ( C swapF D ) = <. O , P >. )
	swapf1f1o.s	|- S = ( C Xc. D )
	swapf1f1o.t	|- T = ( D Xc. C )
	swapf1f1o.c	|- ( ph -> C e. U )
	swapf1f1o.d	|- ( ph -> D e. V )
	swapf1f1o.b	|- B = ( Base ` S )
	swapf1f1o.a	|- A = ( Base ` T )
Assertion	swapf1f1o	|- ( ph -> O : B -1-1-onto-> A )

Proof

Step	Hyp	Ref	Expression
1		swapf1f1o.o	|- ( ph -> ( C swapF D ) = <. O , P >. )
2		swapf1f1o.s	|- S = ( C Xc. D )
3		swapf1f1o.t	|- T = ( D Xc. C )
4		swapf1f1o.c	|- ( ph -> C e. U )
5		swapf1f1o.d	|- ( ph -> D e. V )
6		swapf1f1o.b	|- B = ( Base ` S )
7		swapf1f1o.a	|- A = ( Base ` T )
8		eqid	|- ( Base ` C ) = ( Base ` C )
9		eqid	|- ( Base ` D ) = ( Base ` D )
10	2 8 9	xpcbas	|- ( ( Base ` C ) X. ( Base ` D ) ) = ( Base ` S )
11	6 10	eqtr4i	|- B = ( ( Base ` C ) X. ( Base ` D ) )
12	11	mpteq1i	|- ( x e. B |-> U. `' { x } ) = ( x e. ( ( Base ` C ) X. ( Base ` D ) ) |-> U. `' { x } )
13	12	xpcomf1o	|- ( x e. B |-> U. `' { x } ) : ( ( Base ` C ) X. ( Base ` D ) ) -1-1-onto-> ( ( Base ` D ) X. ( Base ` C ) )
14	4 5 2 6 1	swapf1val	|- ( ph -> O = ( x e. B |-> U. `' { x } ) )
15	11	a1i	|- ( ph -> B = ( ( Base ` C ) X. ( Base ` D ) ) )
16	3 9 8	xpcbas	|- ( ( Base ` D ) X. ( Base ` C ) ) = ( Base ` T )
17	7 16	eqtr4i	|- A = ( ( Base ` D ) X. ( Base ` C ) )
18	17	a1i	|- ( ph -> A = ( ( Base ` D ) X. ( Base ` C ) ) )
19	14 15 18	f1oeq123d	|- ( ph -> ( O : B -1-1-onto-> A <-> ( x e. B |-> U. `' { x } ) : ( ( Base ` C ) X. ( Base ` D ) ) -1-1-onto-> ( ( Base ` D ) X. ( Base ` C ) ) ) )
20	13 19	mpbiri	|- ( ph -> O : B -1-1-onto-> A )