Theorem swapf1vala

Description: The object part of the swap functor. See also swapf1val . (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$$
Assertion	swapf1vala	Could not format assertion : No typesetting found for |- ( ph -> ( 1st ` ( C swapF D ) ) = ( x e. B |-> U. `' { x } ) ) with typecode |-

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		eqidd	$$⊢\phi \to \mathrm{Hom}\left(S\right)=\mathrm{Hom}\left(S\right)$$
6	1 2 3 4 5	swapfval	Could not format ( ph -> ( C swapF D ) = <. ( x e. B |-> U. `' { x } ) , ( u e. B , v e. B |-> ( f e. ( u ( Hom ` S ) v ) |-> U. `' { f } ) ) >. ) : No typesetting found for |- ( ph -> ( C swapF D ) = <. ( x e. B |-> U. `' { x } ) , ( u e. B , v e. B |-> ( f e. ( u ( Hom ` S ) v ) |-> U. `' { f } ) ) >. ) with typecode |-
7	6	fveq2d	Could not format ( ph -> ( 1st ` ( C swapF D ) ) = ( 1st ` <. ( x e. B |-> U. `' { x } ) , ( u e. B , v e. B |-> ( f e. ( u ( Hom ` S ) v ) |-> U. `' { f } ) ) >. ) ) : No typesetting found for |- ( ph -> ( 1st ` ( C swapF D ) ) = ( 1st ` <. ( x e. B |-> U. `' { x } ) , ( u e. B , v e. B |-> ( f e. ( u ( Hom ` S ) v ) |-> U. `' { f } ) ) >. ) ) with typecode |-
8	4	fvexi	$$⊢B\in \mathrm{V}$$
9	8	mptex	$$⊢\left(x\in B⟼\bigcup {\left\{x\right\}}^{-1}\right)\in \mathrm{V}$$
10	8 8	mpoex	$$⊢\left(u\in B,v\in B⟼\left(f\in \left(u\mathrm{Hom}\left(S\right)v\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)\right)\in \mathrm{V}$$
11	9 10	op1st	$$⊢1^{st}\left(⟨\left(x\in B⟼\bigcup {\left\{x\right\}}^{-1}\right),\left(u\in B,v\in B⟼\left(f\in \left(u\mathrm{Hom}\left(S\right)v\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)\right)⟩\right)=\left(x\in B⟼\bigcup {\left\{x\right\}}^{-1}\right)$$
12	7 11	eqtrdi	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 |-