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	$$⊢\phi \to C\in U$$
	swapfval.d	$$⊢\phi \to D\in V$$
	swapf2fvala.s	$$⊢S=C{\times }_{c}D$$
	swapf2fvala.b	$$⊢B={\mathrm{Base}}_S$$
	swapf1val.o	No typesetting found for |- ( ph -> ( C swapF D ) = <. O , P >. ) with typecode |-
Assertion	swapf1val	$$⊢\phi \to O=\left(x\in B⟼\bigcup {\left\{x\right\}}^{-1}\right)$$

Proof

Step	Hyp	Ref	Expression
1		swapfval.c	$$⊢\phi \to C\in U$$
2		swapfval.d	$$⊢\phi \to D\in V$$
3		swapf2fvala.s	$$⊢S=C{\times }_{c}D$$
4		swapf2fvala.b	$$⊢B={\mathrm{Base}}_S$$
5		swapf1val.o	Could not format ( ph -> ( C swapF D ) = <. O , P >. ) : No typesetting found for |- ( ph -> ( C swapF D ) = <. O , P >. ) with typecode |-
6	5	fveq2d	Could not format ( ph -> ( 1st ` ( C swapF D ) ) = ( 1st ` <. O , P >. ) ) : No typesetting found for |- ( ph -> ( 1st ` ( C swapF D ) ) = ( 1st ` <. O , P >. ) ) with typecode |-
7	1 2 3 4	swapf1vala	Could not format ( ph -> ( 1st ` ( C swapF D ) ) = ( x e. B |-> U. `' { x } ) ) : No typesetting found for |- ( ph -> ( 1st ` ( C swapF D ) ) = ( x e. B |-> U. `' { x } ) ) with typecode |-
8	1 2	swapfelvv	Could not format ( ph -> ( C swapF D ) e. ( _V X. _V ) ) : No typesetting found for |- ( ph -> ( C swapF D ) e. ( _V X. _V ) ) with typecode |-
9	5 8	eqeltrrd	$$⊢\phi \to ⟨O,P⟩\in \left(\mathrm{V}\times \mathrm{V}\right)$$
10		opelxp	$$⊢⟨O,P⟩\in \left(\mathrm{V}\times \mathrm{V}\right)\leftrightarrow \left(O\in \mathrm{V}\wedge P\in \mathrm{V}\right)$$
11	10	biimpi	$$⊢⟨O,P⟩\in \left(\mathrm{V}\times \mathrm{V}\right)\to \left(O\in \mathrm{V}\wedge P\in \mathrm{V}\right)$$
12		op1stg	$$⊢\left(O\in \mathrm{V}\wedge P\in \mathrm{V}\right)\to 1^{st}\left(⟨O,P⟩\right)=O$$
13	9 11 12	3syl	$$⊢\phi \to 1^{st}\left(⟨O,P⟩\right)=O$$
14	6 7 13	3eqtr3rd	$$⊢\phi \to O=\left(x\in B⟼\bigcup {\left\{x\right\}}^{-1}\right)$$