swapfval

Description: Value of the swap functor. (Contributed by Zhi Wang, 7-Oct-2025)

	Ref	Expression
Hypotheses	swapfval.c	$⊢ φ \to C \in U$
	swapfval.d	$⊢ φ \to D \in V$
	swapfval.s	$⊢ S = C \times_{c} D$
	swapfval.b	$⊢ B = {Base}_{S}$
	swapfval.h	$⊢ φ \to H = Hom (S)$
Assertion	swapfval	Could not format assertion : No typesetting found for \|- ( ph -> ( C swapF D ) = <. ( x e. B \|-> U. `' { x } ) , ( u e. B , v e. B \|-> ( f e. ( u H v ) \|-> U. `' { f } ) ) >. ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		swapfval.c	$⊢ φ \to C \in U$
2		swapfval.d	$⊢ φ \to D \in V$
3		swapfval.s	$⊢ S = C \times_{c} D$
4		swapfval.b	$⊢ B = {Base}_{S}$
5		swapfval.h	$⊢ φ \to H = Hom (S)$
6		df-swapf	Could not format swapF = ( c e. _V , d e. _V \|-> [_ ( c Xc. d ) / s ]_ [_ ( Base ` s ) / b ]_ [_ ( Hom ` s ) / h ]_ <. ( x e. b \|-> U. `' { x } ) , ( u e. b , v e. b \|-> ( f e. ( u h v ) \|-> U. `' { f } ) ) >. ) : No typesetting found for \|- swapF = ( c e. _V , d e. _V \|-> [_ ( c Xc. d ) / s ]_ [_ ( Base ` s ) / b ]_ [_ ( Hom ` s ) / h ]_ <. ( x e. b \|-> U. `' { x } ) , ( u e. b , v e. b \|-> ( f e. ( u h v ) \|-> U. `' { f } ) ) >. ) with typecode \|-
7	6	a1i	Could not format ( ph -> swapF = ( c e. _V , d e. _V \|-> [_ ( c Xc. d ) / s ]_ [_ ( Base ` s ) / b ]_ [_ ( Hom ` s ) / h ]_ <. ( x e. b \|-> U. `' { x } ) , ( u e. b , v e. b \|-> ( f e. ( u h v ) \|-> U. `' { f } ) ) >. ) ) : No typesetting found for \|- ( ph -> swapF = ( c e. _V , d e. _V \|-> [_ ( c Xc. d ) / s ]_ [_ ( Base ` s ) / b ]_ [_ ( Hom ` s ) / h ]_ <. ( x e. b \|-> U. `' { x } ) , ( u e. b , v e. b \|-> ( f e. ( u h v ) \|-> U. `' { f } ) ) >. ) ) with typecode \|-
8		ovexd	$⊢ (φ \land (c = C \land d = D)) \to c \times_{c} d \in V$
9		simprl	$⊢ (φ \land (c = C \land d = D)) \to c = C$
10		simprr	$⊢ (φ \land (c = C \land d = D)) \to d = D$
11	9 10	oveq12d	$⊢ (φ \land (c = C \land d = D)) \to c \times_{c} d = C \times_{c} D$
12	11 3	eqtr4di	$⊢ (φ \land (c = C \land d = D)) \to c \times_{c} d = S$
13		fvexd	$⊢ ((φ \land (c = C \land d = D)) \land s = S) \to {Base}_{s} \in V$
14		simpr	$⊢ ((φ \land (c = C \land d = D)) \land s = S) \to s = S$
15	14	fveq2d	$⊢ ((φ \land (c = C \land d = D)) \land s = S) \to {Base}_{s} = {Base}_{S}$
16	15 4	eqtr4di	$⊢ ((φ \land (c = C \land d = D)) \land s = S) \to {Base}_{s} = B$
17		fvexd	$⊢ (((φ \land (c = C \land d = D)) \land s = S) \land b = B) \to Hom (s) \in V$
18		simplr	$⊢ (((φ \land (c = C \land d = D)) \land s = S) \land b = B) \to s = S$
19	18	fveq2d	$⊢ (((φ \land (c = C \land d = D)) \land s = S) \land b = B) \to Hom (s) = Hom (S)$
20	5	ad3antrrr	$⊢ (((φ \land (c = C \land d = D)) \land s = S) \land b = B) \to H = Hom (S)$
21	19 20	eqtr4d	$⊢ (((φ \land (c = C \land d = D)) \land s = S) \land b = B) \to Hom (s) = H$
22		simplr	$⊢ ((((φ \land (c = C \land d = D)) \land s = S) \land b = B) \land h = H) \to b = B$
23	22	mpteq1d	$⊢ ((((φ \land (c = C \land d = D)) \land s = S) \land b = B) \land h = H) \to (x \in b ⟼ ⋃ {\{x\}}^{-1}) = (x \in B ⟼ ⋃ {\{x\}}^{-1})$
24		simpr	$⊢ ((((φ \land (c = C \land d = D)) \land s = S) \land b = B) \land h = H) \to h = H$
25	24	oveqd	$⊢ ((((φ \land (c = C \land d = D)) \land s = S) \land b = B) \land h = H) \to u h v = u H v$
26	25	mpteq1d	$⊢ ((((φ \land (c = C \land d = D)) \land s = S) \land b = B) \land h = H) \to (f \in (u h v) ⟼ ⋃ {\{f\}}^{-1}) = (f \in (u H v) ⟼ ⋃ {\{f\}}^{-1})$
27	22 22 26	mpoeq123dv	$⊢ ((((φ \land (c = C \land d = D)) \land s = S) \land b = B) \land h = H) \to (u \in b, v \in b ⟼ (f \in (u h v) ⟼ ⋃ {\{f\}}^{-1})) = (u \in B, v \in B ⟼ (f \in (u H v) ⟼ ⋃ {\{f\}}^{-1}))$
28	23 27	opeq12d	$⊢ ((((φ \land (c = C \land d = D)) \land s = S) \land b = B) \land h = H) \to ⟨(x \in b ⟼ ⋃ {\{x\}}^{-1}), (u \in b, v \in b ⟼ (f \in (u h v) ⟼ ⋃ {\{f\}}^{-1}))⟩ = ⟨(x \in B ⟼ ⋃ {\{x\}}^{-1}), (u \in B, v \in B ⟼ (f \in (u H v) ⟼ ⋃ {\{f\}}^{-1}))⟩$
29	17 21 28	csbied2	$⊢ (((φ \land (c = C \land d = D)) \land s = S) \land b = B) \to ⦋ Hom (s) / h ⦌ ⟨(x \in b ⟼ ⋃ {\{x\}}^{-1}), (u \in b, v \in b ⟼ (f \in (u h v) ⟼ ⋃ {\{f\}}^{-1}))⟩ = ⟨(x \in B ⟼ ⋃ {\{x\}}^{-1}), (u \in B, v \in B ⟼ (f \in (u H v) ⟼ ⋃ {\{f\}}^{-1}))⟩$
30	13 16 29	csbied2	$⊢ ((φ \land (c = C \land d = D)) \land s = S) \to ⦋ {Base}_{s} / b ⦌ ⦋ Hom (s) / h ⦌ ⟨(x \in b ⟼ ⋃ {\{x\}}^{-1}), (u \in b, v \in b ⟼ (f \in (u h v) ⟼ ⋃ {\{f\}}^{-1}))⟩ = ⟨(x \in B ⟼ ⋃ {\{x\}}^{-1}), (u \in B, v \in B ⟼ (f \in (u H v) ⟼ ⋃ {\{f\}}^{-1}))⟩$
31	8 12 30	csbied2	$⊢ (φ \land (c = C \land d = D)) \to ⦋ (c \times_{c} d) / s ⦌ ⦋ {Base}_{s} / b ⦌ ⦋ Hom (s) / h ⦌ ⟨(x \in b ⟼ ⋃ {\{x\}}^{-1}), (u \in b, v \in b ⟼ (f \in (u h v) ⟼ ⋃ {\{f\}}^{-1}))⟩ = ⟨(x \in B ⟼ ⋃ {\{x\}}^{-1}), (u \in B, v \in B ⟼ (f \in (u H v) ⟼ ⋃ {\{f\}}^{-1}))⟩$
32	1	elexd	$⊢ φ \to C \in V$
33	2	elexd	$⊢ φ \to D \in V$
34		opex	$⊢ ⟨(x \in B ⟼ ⋃ {\{x\}}^{-1}), (u \in B, v \in B ⟼ (f \in (u H v) ⟼ ⋃ {\{f\}}^{-1}))⟩ \in V$
35	34	a1i	$⊢ φ \to ⟨(x \in B ⟼ ⋃ {\{x\}}^{-1}), (u \in B, v \in B ⟼ (f \in (u H v) ⟼ ⋃ {\{f\}}^{-1}))⟩ \in V$
36	7 31 32 33 35	ovmpod	Could not format ( ph -> ( C swapF D ) = <. ( x e. B \|-> U. `' { x } ) , ( u e. B , v e. B \|-> ( f e. ( u H 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 H v ) \|-> U. `' { f } ) ) >. ) with typecode \|-

Metamath Proof Explorer

Theorem swapfval

Proof