Theorem swapf1a

Description: The object part of the swap functor swaps the objects. (Contributed by Zhi Wang, 7-Oct-2025)

	Ref	Expression
Hypotheses	swapf1a.o	|- ( ph -> ( C swapF D ) = <. O , P >. )
	swapf1a.s	|- S = ( C Xc. D )
	swapf1a.b	|- B = ( Base ` S )
	swapf1a.x	|- ( ph -> X e. B )
Assertion	swapf1a	|- ( ph -> ( O ` X ) = <. ( 2nd ` X ) , ( 1st ` X ) >. )

Proof

Step	Hyp	Ref	Expression
1		swapf1a.o	|- ( ph -> ( C swapF D ) = <. O , P >. )
2		swapf1a.s	|- S = ( C Xc. D )
3		swapf1a.b	|- B = ( Base ` S )
4		swapf1a.x	|- ( ph -> X e. B )
5	2 3 4	elxpcbasex1	|- ( ph -> C e. _V )
6	2 3 4	elxpcbasex2	|- ( ph -> D e. _V )
7	5 6 2 3 1	swapf1val	|- ( ph -> O = ( x e. B |-> U. `' { x } ) )
8		simpr	|- ( ( ph /\ x = X ) -> x = X )
9	8	sneqd	|- ( ( ph /\ x = X ) -> { x } = { X } )
10	9	cnveqd	|- ( ( ph /\ x = X ) -> `' { x } = `' { X } )
11	10	unieqd	|- ( ( ph /\ x = X ) -> U. `' { x } = U. `' { X } )
12		eqid	|- ( Base ` C ) = ( Base ` C )
13		eqid	|- ( Base ` D ) = ( Base ` D )
14	2 12 13	xpcbas	|- ( ( Base ` C ) X. ( Base ` D ) ) = ( Base ` S )
15	3 14	eqtr4i	|- B = ( ( Base ` C ) X. ( Base ` D ) )
16	4 15	eleqtrdi	|- ( ph -> X e. ( ( Base ` C ) X. ( Base ` D ) ) )
17		2nd1st	|- ( X e. ( ( Base ` C ) X. ( Base ` D ) ) -> U. `' { X } = <. ( 2nd ` X ) , ( 1st ` X ) >. )
18	16 17	syl	|- ( ph -> U. `' { X } = <. ( 2nd ` X ) , ( 1st ` X ) >. )
19	18	adantr	|- ( ( ph /\ x = X ) -> U. `' { X } = <. ( 2nd ` X ) , ( 1st ` X ) >. )
20	11 19	eqtrd	|- ( ( ph /\ x = X ) -> U. `' { x } = <. ( 2nd ` X ) , ( 1st ` X ) >. )
21		opex	|- <. ( 2nd ` X ) , ( 1st ` X ) >. e. _V
22	21	a1i	|- ( ph -> <. ( 2nd ` X ) , ( 1st ` X ) >. e. _V )
23	7 20 4 22	fvmptd	|- ( ph -> ( O ` X ) = <. ( 2nd ` X ) , ( 1st ` X ) >. )