Theorem dfswapf2

Description: Alternate definition of swapF ( df-swapf ). (Contributed by Zhi Wang, 9-Oct-2025)

	Ref	Expression
Assertion	dfswapf2	Could not format assertion : No typesetting found for |- swapF = ( c e. _V , d e. _V |-> [_ ( c Xc. d ) / s ]_ [_ ( Base ` s ) / b ]_ [_ ( Hom ` s ) / h ]_ <. ( tpos _I |` b ) , ( u e. b , v e. b |-> ( tpos _I |` ( u h v ) ) ) >. ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		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 |-
2		fvex	$$⊢{\mathrm{Base}}_{\left(c{\times }_{c}d\right)}\in \mathrm{V}$$
3		id	$$⊢b={\mathrm{Base}}_{\left(c{\times }_{c}d\right)}\to b={\mathrm{Base}}_{\left(c{\times }_{c}d\right)}$$
4		eqid	$$⊢c{\times }_{c}d=c{\times }_{c}d$$
5		eqid	$$⊢{\mathrm{Base}}_c={\mathrm{Base}}_c$$
6		eqid	$$⊢{\mathrm{Base}}_d={\mathrm{Base}}_d$$
7	4 5 6	xpcbas	$$⊢{\mathrm{Base}}_c\times {\mathrm{Base}}_d={\mathrm{Base}}_{\left(c{\times }_{c}d\right)}$$
8	3 7	eqtr4di	$$⊢b={\mathrm{Base}}_{\left(c{\times }_{c}d\right)}\to b={\mathrm{Base}}_c\times {\mathrm{Base}}_d$$
9	8	mpteq1d	$$⊢b={\mathrm{Base}}_{\left(c{\times }_{c}d\right)}\to \left(x\in b⟼\bigcup {\left\{x\right\}}^{-1}\right)=\left(x\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)⟼\bigcup {\left\{x\right\}}^{-1}\right)$$
10		eqidd	$$⊢b={\mathrm{Base}}_{\left(c{\times }_{c}d\right)}\to \left(f\in \left(uhv\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)=\left(f\in \left(uhv\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)$$
11	8 8 10	mpoeq123dv	$$⊢b={\mathrm{Base}}_{\left(c{\times }_{c}d\right)}\to \left(u\in b,v\in b⟼\left(f\in \left(uhv\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)\right)=\left(u\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right),v\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)⟼\left(f\in \left(uhv\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)\right)$$
12	9 11	opeq12d	$$⊢b={\mathrm{Base}}_{\left(c{\times }_{c}d\right)}\to ⟨\left(x\in b⟼\bigcup {\left\{x\right\}}^{-1}\right),\left(u\in b,v\in b⟼\left(f\in \left(uhv\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)\right)⟩=⟨\left(x\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)⟼\bigcup {\left\{x\right\}}^{-1}\right),\left(u\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right),v\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)⟼\left(f\in \left(uhv\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)\right)⟩$$
13	12	csbeq2dv	$$⊢b={\mathrm{Base}}_{\left(c{\times }_{c}d\right)}\to ⦋\mathrm{Hom}\left(c{\times }_{c}d\right)/h⦌⟨\left(x\in b⟼\bigcup {\left\{x\right\}}^{-1}\right),\left(u\in b,v\in b⟼\left(f\in \left(uhv\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)\right)⟩=⦋\mathrm{Hom}\left(c{\times }_{c}d\right)/h⦌⟨\left(x\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)⟼\bigcup {\left\{x\right\}}^{-1}\right),\left(u\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right),v\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)⟼\left(f\in \left(uhv\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)\right)⟩$$
14	2 13	csbie	$$⊢⦋{\mathrm{Base}}_{\left(c{\times }_{c}d\right)}/b⦌⦋\mathrm{Hom}\left(c{\times }_{c}d\right)/h⦌⟨\left(x\in b⟼\bigcup {\left\{x\right\}}^{-1}\right),\left(u\in b,v\in b⟼\left(f\in \left(uhv\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)\right)⟩=⦋\mathrm{Hom}\left(c{\times }_{c}d\right)/h⦌⟨\left(x\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)⟼\bigcup {\left\{x\right\}}^{-1}\right),\left(u\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right),v\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)⟼\left(f\in \left(uhv\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)\right)⟩$$
15		ovex	$$⊢c{\times }_{c}d\in \mathrm{V}$$
16		fveq2	$$⊢s=c{\times }_{c}d\to {\mathrm{Base}}_s={\mathrm{Base}}_{\left(c{\times }_{c}d\right)}$$
17		fveq2	$$⊢s=c{\times }_{c}d\to \mathrm{Hom}\left(s\right)=\mathrm{Hom}\left(c{\times }_{c}d\right)$$
18	17	csbeq1d	$$⊢s=c{\times }_{c}d\to ⦋\mathrm{Hom}\left(s\right)/h⦌⟨\left(x\in b⟼\bigcup {\left\{x\right\}}^{-1}\right),\left(u\in b,v\in b⟼\left(f\in \left(uhv\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)\right)⟩=⦋\mathrm{Hom}\left(c{\times }_{c}d\right)/h⦌⟨\left(x\in b⟼\bigcup {\left\{x\right\}}^{-1}\right),\left(u\in b,v\in b⟼\left(f\in \left(uhv\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)\right)⟩$$
19	16 18	csbeq12dv	$$⊢s=c{\times }_{c}d\to ⦋{\mathrm{Base}}_s/b⦌⦋\mathrm{Hom}\left(s\right)/h⦌⟨\left(x\in b⟼\bigcup {\left\{x\right\}}^{-1}\right),\left(u\in b,v\in b⟼\left(f\in \left(uhv\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)\right)⟩=⦋{\mathrm{Base}}_{\left(c{\times }_{c}d\right)}/b⦌⦋\mathrm{Hom}\left(c{\times }_{c}d\right)/h⦌⟨\left(x\in b⟼\bigcup {\left\{x\right\}}^{-1}\right),\left(u\in b,v\in b⟼\left(f\in \left(uhv\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)\right)⟩$$
20	15 19	csbie	$$⊢⦋\left(c{\times }_{c}d\right)/s⦌⦋{\mathrm{Base}}_s/b⦌⦋\mathrm{Hom}\left(s\right)/h⦌⟨\left(x\in b⟼\bigcup {\left\{x\right\}}^{-1}\right),\left(u\in b,v\in b⟼\left(f\in \left(uhv\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)\right)⟩=⦋{\mathrm{Base}}_{\left(c{\times }_{c}d\right)}/b⦌⦋\mathrm{Hom}\left(c{\times }_{c}d\right)/h⦌⟨\left(x\in b⟼\bigcup {\left\{x\right\}}^{-1}\right),\left(u\in b,v\in b⟼\left(f\in \left(uhv\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)\right)⟩$$
21	17	csbeq1d	$$⊢s=c{\times }_{c}d\to ⦋\mathrm{Hom}\left(s\right)/h⦌⟨{tpos\mathrm{I}\upharpoonright }_b,\left(u\in b,v\in b⟼{tpos\mathrm{I}\upharpoonright }_{\left(uhv\right)}\right)⟩=⦋\mathrm{Hom}\left(c{\times }_{c}d\right)/h⦌⟨{tpos\mathrm{I}\upharpoonright }_b,\left(u\in b,v\in b⟼{tpos\mathrm{I}\upharpoonright }_{\left(uhv\right)}\right)⟩$$
22	16 21	csbeq12dv	$$⊢s=c{\times }_{c}d\to ⦋{\mathrm{Base}}_s/b⦌⦋\mathrm{Hom}\left(s\right)/h⦌⟨{tpos\mathrm{I}\upharpoonright }_b,\left(u\in b,v\in b⟼{tpos\mathrm{I}\upharpoonright }_{\left(uhv\right)}\right)⟩=⦋{\mathrm{Base}}_{\left(c{\times }_{c}d\right)}/b⦌⦋\mathrm{Hom}\left(c{\times }_{c}d\right)/h⦌⟨{tpos\mathrm{I}\upharpoonright }_b,\left(u\in b,v\in b⟼{tpos\mathrm{I}\upharpoonright }_{\left(uhv\right)}\right)⟩$$
23	15 22	csbie	$$⊢⦋\left(c{\times }_{c}d\right)/s⦌⦋{\mathrm{Base}}_s/b⦌⦋\mathrm{Hom}\left(s\right)/h⦌⟨{tpos\mathrm{I}\upharpoonright }_b,\left(u\in b,v\in b⟼{tpos\mathrm{I}\upharpoonright }_{\left(uhv\right)}\right)⟩=⦋{\mathrm{Base}}_{\left(c{\times }_{c}d\right)}/b⦌⦋\mathrm{Hom}\left(c{\times }_{c}d\right)/h⦌⟨{tpos\mathrm{I}\upharpoonright }_b,\left(u\in b,v\in b⟼{tpos\mathrm{I}\upharpoonright }_{\left(uhv\right)}\right)⟩$$
24	8	reseq2d	$$⊢b={\mathrm{Base}}_{\left(c{\times }_{c}d\right)}\to {tpos\mathrm{I}\upharpoonright }_b={tpos\mathrm{I}\upharpoonright }_{\left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)}$$
25		eqidd	$$⊢b={\mathrm{Base}}_{\left(c{\times }_{c}d\right)}\to {tpos\mathrm{I}\upharpoonright }_{\left(uhv\right)}={tpos\mathrm{I}\upharpoonright }_{\left(uhv\right)}$$
26	8 8 25	mpoeq123dv	$$⊢b={\mathrm{Base}}_{\left(c{\times }_{c}d\right)}\to \left(u\in b,v\in b⟼{tpos\mathrm{I}\upharpoonright }_{\left(uhv\right)}\right)=\left(u\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right),v\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)⟼{tpos\mathrm{I}\upharpoonright }_{\left(uhv\right)}\right)$$
27	24 26	opeq12d	$$⊢b={\mathrm{Base}}_{\left(c{\times }_{c}d\right)}\to ⟨{tpos\mathrm{I}\upharpoonright }_b,\left(u\in b,v\in b⟼{tpos\mathrm{I}\upharpoonright }_{\left(uhv\right)}\right)⟩=⟨{tpos\mathrm{I}\upharpoonright }_{\left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)},\left(u\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right),v\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)⟼{tpos\mathrm{I}\upharpoonright }_{\left(uhv\right)}\right)⟩$$
28	27	csbeq2dv	$$⊢b={\mathrm{Base}}_{\left(c{\times }_{c}d\right)}\to ⦋\mathrm{Hom}\left(c{\times }_{c}d\right)/h⦌⟨{tpos\mathrm{I}\upharpoonright }_b,\left(u\in b,v\in b⟼{tpos\mathrm{I}\upharpoonright }_{\left(uhv\right)}\right)⟩=⦋\mathrm{Hom}\left(c{\times }_{c}d\right)/h⦌⟨{tpos\mathrm{I}\upharpoonright }_{\left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)},\left(u\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right),v\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)⟼{tpos\mathrm{I}\upharpoonright }_{\left(uhv\right)}\right)⟩$$
29	2 28	csbie	$$⊢⦋{\mathrm{Base}}_{\left(c{\times }_{c}d\right)}/b⦌⦋\mathrm{Hom}\left(c{\times }_{c}d\right)/h⦌⟨{tpos\mathrm{I}\upharpoonright }_b,\left(u\in b,v\in b⟼{tpos\mathrm{I}\upharpoonright }_{\left(uhv\right)}\right)⟩=⦋\mathrm{Hom}\left(c{\times }_{c}d\right)/h⦌⟨{tpos\mathrm{I}\upharpoonright }_{\left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)},\left(u\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right),v\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)⟼{tpos\mathrm{I}\upharpoonright }_{\left(uhv\right)}\right)⟩$$
30		eqid	$$⊢{\mathrm{Base}}_c\times {\mathrm{Base}}_d={\mathrm{Base}}_c\times {\mathrm{Base}}_d$$
31	30	tposideq2	$$⊢{tpos\mathrm{I}\upharpoonright }_{\left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)}=\left(x\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)⟼\bigcup {\left\{x\right\}}^{-1}\right)$$
32		eqid	$$⊢\left(1^{st}\left(u\right)\mathrm{Hom}\left(c\right)1^{st}\left(v\right)\right)\times \left(2^{nd}\left(u\right)\mathrm{Hom}\left(d\right)2^{nd}\left(v\right)\right)=\left(1^{st}\left(u\right)\mathrm{Hom}\left(c\right)1^{st}\left(v\right)\right)\times \left(2^{nd}\left(u\right)\mathrm{Hom}\left(d\right)2^{nd}\left(v\right)\right)$$
33	32	tposideq2	$$⊢{tpos\mathrm{I}\upharpoonright }_{\left(\left(1^{st}\left(u\right)\mathrm{Hom}\left(c\right)1^{st}\left(v\right)\right)\times \left(2^{nd}\left(u\right)\mathrm{Hom}\left(d\right)2^{nd}\left(v\right)\right)\right)}=\left(f\in \left(\left(1^{st}\left(u\right)\mathrm{Hom}\left(c\right)1^{st}\left(v\right)\right)\times \left(2^{nd}\left(u\right)\mathrm{Hom}\left(d\right)2^{nd}\left(v\right)\right)\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)$$
34		eqid	$$⊢\mathrm{Hom}\left(c\right)=\mathrm{Hom}\left(c\right)$$
35		eqid	$$⊢\mathrm{Hom}\left(d\right)=\mathrm{Hom}\left(d\right)$$
36		eqid	$$⊢\mathrm{Hom}\left(c{\times }_{c}d\right)=\mathrm{Hom}\left(c{\times }_{c}d\right)$$
37		simpl	$$⊢\left(u\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)\wedge v\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)\right)\to u\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)$$
38		simpr	$$⊢\left(u\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)\wedge v\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)\right)\to v\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)$$
39	4 7 34 35 36 37 38	xpchom	$$⊢\left(u\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)\wedge v\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)\right)\to u\mathrm{Hom}\left(c{\times }_{c}d\right)v=\left(1^{st}\left(u\right)\mathrm{Hom}\left(c\right)1^{st}\left(v\right)\right)\times \left(2^{nd}\left(u\right)\mathrm{Hom}\left(d\right)2^{nd}\left(v\right)\right)$$
40	39	reseq2d	$$⊢\left(u\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)\wedge v\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)\right)\to {tpos\mathrm{I}\upharpoonright }_{\left(u\mathrm{Hom}\left(c{\times }_{c}d\right)v\right)}={tpos\mathrm{I}\upharpoonright }_{\left(\left(1^{st}\left(u\right)\mathrm{Hom}\left(c\right)1^{st}\left(v\right)\right)\times \left(2^{nd}\left(u\right)\mathrm{Hom}\left(d\right)2^{nd}\left(v\right)\right)\right)}$$
41	39	mpteq1d	$$⊢\left(u\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)\wedge v\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)\right)\to \left(f\in \left(u\mathrm{Hom}\left(c{\times }_{c}d\right)v\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)=\left(f\in \left(\left(1^{st}\left(u\right)\mathrm{Hom}\left(c\right)1^{st}\left(v\right)\right)\times \left(2^{nd}\left(u\right)\mathrm{Hom}\left(d\right)2^{nd}\left(v\right)\right)\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)$$
42	33 40 41	3eqtr4a	$$⊢\left(u\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)\wedge v\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)\right)\to {tpos\mathrm{I}\upharpoonright }_{\left(u\mathrm{Hom}\left(c{\times }_{c}d\right)v\right)}=\left(f\in \left(u\mathrm{Hom}\left(c{\times }_{c}d\right)v\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)$$
43	42	mpoeq3ia	$$⊢\left(u\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right),v\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)⟼{tpos\mathrm{I}\upharpoonright }_{\left(u\mathrm{Hom}\left(c{\times }_{c}d\right)v\right)}\right)=\left(u\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right),v\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)⟼\left(f\in \left(u\mathrm{Hom}\left(c{\times }_{c}d\right)v\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)\right)$$
44	31 43	opeq12i	$$⊢⟨{tpos\mathrm{I}\upharpoonright }_{\left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)},\left(u\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right),v\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)⟼{tpos\mathrm{I}\upharpoonright }_{\left(u\mathrm{Hom}\left(c{\times }_{c}d\right)v\right)}\right)⟩=⟨\left(x\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)⟼\bigcup {\left\{x\right\}}^{-1}\right),\left(u\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right),v\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)⟼\left(f\in \left(u\mathrm{Hom}\left(c{\times }_{c}d\right)v\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)\right)⟩$$
45		fvex	$$⊢\mathrm{Hom}\left(c{\times }_{c}d\right)\in \mathrm{V}$$
46		oveq	$$⊢h=\mathrm{Hom}\left(c{\times }_{c}d\right)\to uhv=u\mathrm{Hom}\left(c{\times }_{c}d\right)v$$
47	46	reseq2d	$$⊢h=\mathrm{Hom}\left(c{\times }_{c}d\right)\to {tpos\mathrm{I}\upharpoonright }_{\left(uhv\right)}={tpos\mathrm{I}\upharpoonright }_{\left(u\mathrm{Hom}\left(c{\times }_{c}d\right)v\right)}$$
48	47	mpoeq3dv	$$⊢h=\mathrm{Hom}\left(c{\times }_{c}d\right)\to \left(u\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right),v\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)⟼{tpos\mathrm{I}\upharpoonright }_{\left(uhv\right)}\right)=\left(u\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right),v\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)⟼{tpos\mathrm{I}\upharpoonright }_{\left(u\mathrm{Hom}\left(c{\times }_{c}d\right)v\right)}\right)$$
49	48	opeq2d	$$⊢h=\mathrm{Hom}\left(c{\times }_{c}d\right)\to ⟨{tpos\mathrm{I}\upharpoonright }_{\left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)},\left(u\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right),v\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)⟼{tpos\mathrm{I}\upharpoonright }_{\left(uhv\right)}\right)⟩=⟨{tpos\mathrm{I}\upharpoonright }_{\left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)},\left(u\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right),v\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)⟼{tpos\mathrm{I}\upharpoonright }_{\left(u\mathrm{Hom}\left(c{\times }_{c}d\right)v\right)}\right)⟩$$
50	45 49	csbie	$$⊢⦋\mathrm{Hom}\left(c{\times }_{c}d\right)/h⦌⟨{tpos\mathrm{I}\upharpoonright }_{\left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)},\left(u\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right),v\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)⟼{tpos\mathrm{I}\upharpoonright }_{\left(uhv\right)}\right)⟩=⟨{tpos\mathrm{I}\upharpoonright }_{\left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)},\left(u\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right),v\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)⟼{tpos\mathrm{I}\upharpoonright }_{\left(u\mathrm{Hom}\left(c{\times }_{c}d\right)v\right)}\right)⟩$$
51	46	mpteq1d	$$⊢h=\mathrm{Hom}\left(c{\times }_{c}d\right)\to \left(f\in \left(uhv\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)=\left(f\in \left(u\mathrm{Hom}\left(c{\times }_{c}d\right)v\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)$$
52	51	mpoeq3dv	$$⊢h=\mathrm{Hom}\left(c{\times }_{c}d\right)\to \left(u\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right),v\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)⟼\left(f\in \left(uhv\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)\right)=\left(u\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right),v\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)⟼\left(f\in \left(u\mathrm{Hom}\left(c{\times }_{c}d\right)v\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)\right)$$
53	52	opeq2d	$$⊢h=\mathrm{Hom}\left(c{\times }_{c}d\right)\to ⟨\left(x\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)⟼\bigcup {\left\{x\right\}}^{-1}\right),\left(u\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right),v\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)⟼\left(f\in \left(uhv\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)\right)⟩=⟨\left(x\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)⟼\bigcup {\left\{x\right\}}^{-1}\right),\left(u\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right),v\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)⟼\left(f\in \left(u\mathrm{Hom}\left(c{\times }_{c}d\right)v\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)\right)⟩$$
54	45 53	csbie	$$⊢⦋\mathrm{Hom}\left(c{\times }_{c}d\right)/h⦌⟨\left(x\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)⟼\bigcup {\left\{x\right\}}^{-1}\right),\left(u\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right),v\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)⟼\left(f\in \left(uhv\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)\right)⟩=⟨\left(x\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)⟼\bigcup {\left\{x\right\}}^{-1}\right),\left(u\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right),v\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)⟼\left(f\in \left(u\mathrm{Hom}\left(c{\times }_{c}d\right)v\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)\right)⟩$$
55	44 50 54	3eqtr4i	$$⊢⦋\mathrm{Hom}\left(c{\times }_{c}d\right)/h⦌⟨{tpos\mathrm{I}\upharpoonright }_{\left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)},\left(u\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right),v\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)⟼{tpos\mathrm{I}\upharpoonright }_{\left(uhv\right)}\right)⟩=⦋\mathrm{Hom}\left(c{\times }_{c}d\right)/h⦌⟨\left(x\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)⟼\bigcup {\left\{x\right\}}^{-1}\right),\left(u\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right),v\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)⟼\left(f\in \left(uhv\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)\right)⟩$$
56	23 29 55	3eqtri	$$⊢⦋\left(c{\times }_{c}d\right)/s⦌⦋{\mathrm{Base}}_s/b⦌⦋\mathrm{Hom}\left(s\right)/h⦌⟨{tpos\mathrm{I}\upharpoonright }_b,\left(u\in b,v\in b⟼{tpos\mathrm{I}\upharpoonright }_{\left(uhv\right)}\right)⟩=⦋\mathrm{Hom}\left(c{\times }_{c}d\right)/h⦌⟨\left(x\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)⟼\bigcup {\left\{x\right\}}^{-1}\right),\left(u\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right),v\in \left({\mathrm{Base}}_c\times {\mathrm{Base}}_d\right)⟼\left(f\in \left(uhv\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)\right)⟩$$
57	14 20 56	3eqtr4ri	$$⊢⦋\left(c{\times }_{c}d\right)/s⦌⦋{\mathrm{Base}}_s/b⦌⦋\mathrm{Hom}\left(s\right)/h⦌⟨{tpos\mathrm{I}\upharpoonright }_b,\left(u\in b,v\in b⟼{tpos\mathrm{I}\upharpoonright }_{\left(uhv\right)}\right)⟩=⦋\left(c{\times }_{c}d\right)/s⦌⦋{\mathrm{Base}}_s/b⦌⦋\mathrm{Hom}\left(s\right)/h⦌⟨\left(x\in b⟼\bigcup {\left\{x\right\}}^{-1}\right),\left(u\in b,v\in b⟼\left(f\in \left(uhv\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)\right)⟩$$
58	57	a1i	$$⊢\left(c\in \mathrm{V}\wedge d\in \mathrm{V}\right)\to ⦋\left(c{\times }_{c}d\right)/s⦌⦋{\mathrm{Base}}_s/b⦌⦋\mathrm{Hom}\left(s\right)/h⦌⟨{tpos\mathrm{I}\upharpoonright }_b,\left(u\in b,v\in b⟼{tpos\mathrm{I}\upharpoonright }_{\left(uhv\right)}\right)⟩=⦋\left(c{\times }_{c}d\right)/s⦌⦋{\mathrm{Base}}_s/b⦌⦋\mathrm{Hom}\left(s\right)/h⦌⟨\left(x\in b⟼\bigcup {\left\{x\right\}}^{-1}\right),\left(u\in b,v\in b⟼\left(f\in \left(uhv\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)\right)⟩$$
59	58	mpoeq3ia	$$⊢\left(c\in \mathrm{V},d\in \mathrm{V}⟼⦋\left(c{\times }_{c}d\right)/s⦌⦋{\mathrm{Base}}_s/b⦌⦋\mathrm{Hom}\left(s\right)/h⦌⟨{tpos\mathrm{I}\upharpoonright }_b,\left(u\in b,v\in b⟼{tpos\mathrm{I}\upharpoonright }_{\left(uhv\right)}\right)⟩\right)=\left(c\in \mathrm{V},d\in \mathrm{V}⟼⦋\left(c{\times }_{c}d\right)/s⦌⦋{\mathrm{Base}}_s/b⦌⦋\mathrm{Hom}\left(s\right)/h⦌⟨\left(x\in b⟼\bigcup {\left\{x\right\}}^{-1}\right),\left(u\in b,v\in b⟼\left(f\in \left(uhv\right)⟼\bigcup {\left\{f\right\}}^{-1}\right)\right)⟩\right)$$
60	1 59	eqtr4i	Could not format swapF = ( c e. _V , d e. _V |-> [_ ( c Xc. d ) / s ]_ [_ ( Base ` s ) / b ]_ [_ ( Hom ` s ) / h ]_ <. ( tpos _I |` b ) , ( u e. b , v e. b |-> ( tpos _I |` ( u h v ) ) ) >. ) : No typesetting found for |- swapF = ( c e. _V , d e. _V |-> [_ ( c Xc. d ) / s ]_ [_ ( Base ` s ) / b ]_ [_ ( Hom ` s ) / h ]_ <. ( tpos _I |` b ) , ( u e. b , v e. b |-> ( tpos _I |` ( u h v ) ) ) >. ) with typecode |-