Theorem swapfelvv

Description: A swap functor is an ordered pair. (Contributed by Zhi Wang, 7-Oct-2025)

	Ref	Expression
Hypotheses	swapfval.c	$$⊢\phi \to C\in U$$
	swapfval.d	$$⊢\phi \to D\in V$$
Assertion	swapfelvv	Could not format assertion : No typesetting found for |- ( ph -> ( C swapF D ) e. ( _V X. _V ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		swapfval.c	$$⊢\phi \to C\in U$$
2		swapfval.d	$$⊢\phi \to D\in V$$
3		eqid	$$⊢C{\times }_{c}D=C{\times }_{c}D$$
4		eqid	$$⊢{\mathrm{Base}}_{\left(C{\times }_{c}D\right)}={\mathrm{Base}}_{\left(C{\times }_{c}D\right)}$$
5		eqidd	$$⊢\phi \to \mathrm{Hom}\left(C{\times }_{c}D\right)=\mathrm{Hom}\left(C{\times }_{c}D\right)$$
6	1 2 3 4 5	swapfval	Could not format ( ph -> ( C swapF D ) = <. ( x e. ( Base ` ( C Xc. D ) ) |-> U. `' { x } ) , ( u e. ( Base ` ( C Xc. D ) ) , v e. ( Base ` ( C Xc. D ) ) |-> ( f e. ( u ( Hom ` ( C Xc. D ) ) v ) |-> U. `' { f } ) ) >. ) : No typesetting found for |- ( ph -> ( C swapF D ) = <. ( x e. ( Base ` ( C Xc. D ) ) |-> U. `' { x } ) , ( u e. ( Base ` ( C Xc. D ) ) , v e. ( Base ` ( C Xc. D ) ) |-> ( f e. ( u ( Hom ` ( C Xc. D ) ) v ) |-> U. `' { f } ) ) >. ) with typecode |-
7		fvex	$$⊢{\mathrm{Base}}_{\left(C{\times }_{c}D\right)}\in \mathrm{V}$$
8	7	mptex	$$⊢\left(x\in {\mathrm{Base}}_{\left(C{\times }_{c}D\right)}⟼\bigcup {\left\{x\right\}}^{-1}\right)\in \mathrm{V}$$
9	7 7	mpoex	$$⊢\left(u\in {\mathrm{Base}}_{\left(C{\times }_{c}D\right)},v\in {\mathrm{Base}}_{\left(C{\times }_{c}D\right)}⟼\left(f\in \left(u\mathrm{Hom}\left(C{\times }_{c}D\right)v\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)\right)\in \mathrm{V}$$
10	8 9	opelvv	$$⊢⟨\left(x\in {\mathrm{Base}}_{\left(C{\times }_{c}D\right)}⟼\bigcup {\left\{x\right\}}^{-1}\right),\left(u\in {\mathrm{Base}}_{\left(C{\times }_{c}D\right)},v\in {\mathrm{Base}}_{\left(C{\times }_{c}D\right)}⟼\left(f\in \left(u\mathrm{Hom}\left(C{\times }_{c}D\right)v\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)\right)⟩\in \left(\mathrm{V}\times \mathrm{V}\right)$$
11	6 10	eqeltrdi	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 |-