df-xrn

		Ref	Expression
	Assertion	df-xrn	$⊢ A ⋉ B = ({({1^{st} ↾}_{(V \times V)})}^{-1} \circ A) \cap ({({2^{nd} ↾}_{(V \times V)})}^{-1} \circ B)$

Step	Hyp	Ref	Expression
0		cA	$class A$
1		cB	$class B$
2	0 1	cxrn	$class A ⋉ B$
3		c1st	$class 1^{st}$
4		cvv	$class V$
5	4 4	cxp	$class (V \times V)$
6	3 5	cres	$class ({1^{st} ↾}_{(V \times V)})$
7	6	ccnv	$class {({1^{st} ↾}_{(V \times V)})}^{-1}$
8	7 0	ccom	$class ({({1^{st} ↾}_{(V \times V)})}^{-1} \circ A)$
9		c2nd	$class 2^{nd}$
10	9 5	cres	$class ({2^{nd} ↾}_{(V \times V)})$
11	10	ccnv	$class {({2^{nd} ↾}_{(V \times V)})}^{-1}$
12	11 1	ccom	$class ({({2^{nd} ↾}_{(V \times V)})}^{-1} \circ B)$
13	8 12	cin	$class (({({1^{st} ↾}_{(V \times V)})}^{-1} \circ A) \cap ({({2^{nd} ↾}_{(V \times V)})}^{-1} \circ B))$
14	2 13	wceq	$wff A ⋉ B = ({({1^{st} ↾}_{(V \times V)})}^{-1} \circ A) \cap ({({2^{nd} ↾}_{(V \times V)})}^{-1} \circ B)$

Metamath Proof Explorer