Theorem swapf1val

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

	Ref	Expression
Hypotheses	swapfval.c	|- ( ph -> C e. U )
	swapfval.d	|- ( ph -> D e. V )
	swapf2fvala.s	|- S = ( C Xc. D )
	swapf2fvala.b	|- B = ( Base ` S )
	swapf1val.o	|- ( ph -> ( C swapF D ) = <. O , P >. )
Assertion	swapf1val	|- ( ph -> O = ( x e. B |-> U. `' { x } ) )

Proof

Step	Hyp	Ref	Expression
1		swapfval.c	|- ( ph -> C e. U )
2		swapfval.d	|- ( ph -> D e. V )
3		swapf2fvala.s	|- S = ( C Xc. D )
4		swapf2fvala.b	|- B = ( Base ` S )
5		swapf1val.o	|- ( ph -> ( C swapF D ) = <. O , P >. )
6	5	fveq2d	|- ( ph -> ( 1st ` ( C swapF D ) ) = ( 1st ` <. O , P >. ) )
7	1 2 3 4	swapf1vala	|- ( ph -> ( 1st ` ( C swapF D ) ) = ( x e. B |-> U. `' { x } ) )
8	1 2	swapfelvv	|- ( ph -> ( C swapF D ) e. ( _V X. _V ) )
9	5 8	eqeltrrd	|- ( ph -> <. O , P >. e. ( _V X. _V ) )
10		opelxp	|- ( <. O , P >. e. ( _V X. _V ) <-> ( O e. _V /\ P e. _V ) )
11	10	biimpi	|- ( <. O , P >. e. ( _V X. _V ) -> ( O e. _V /\ P e. _V ) )
12		op1stg	|- ( ( O e. _V /\ P e. _V ) -> ( 1st ` <. O , P >. ) = O )
13	9 11 12	3syl	|- ( ph -> ( 1st ` <. O , P >. ) = O )
14	6 7 13	3eqtr3rd	|- ( ph -> O = ( x e. B |-> U. `' { x } ) )