brxrn

Description: Characterize a ternary relation over a range Cartesian product. Together with xrnss3v , this characterizes elementhood in a range cross. (Contributed by Peter Mazsa, 27-Jun-2021)

		Ref	Expression
	Assertion	brxrn	$⊢ (A \in V \land B \in W \land C \in X) \to (A R ⋉ S ⟨B, C⟩ \leftrightarrow (A R B \land A S C))$

Proof

Step	Hyp	Ref	Expression
1		df-xrn	$⊢ R ⋉ S = ({({1^{st} ↾}_{(V \times V)})}^{-1} \circ R) \cap ({({2^{nd} ↾}_{(V \times V)})}^{-1} \circ S)$
2	1	breqi	$⊢ A R ⋉ S ⟨B, C⟩ \leftrightarrow A (({({1^{st} ↾}_{(V \times V)})}^{-1} \circ R) \cap ({({2^{nd} ↾}_{(V \times V)})}^{-1} \circ S)) ⟨B, C⟩$
3	2	a1i	$⊢ (A \in V \land B \in W \land C \in X) \to (A R ⋉ S ⟨B, C⟩ \leftrightarrow A (({({1^{st} ↾}_{(V \times V)})}^{-1} \circ R) \cap ({({2^{nd} ↾}_{(V \times V)})}^{-1} \circ S)) ⟨B, C⟩)$
4		brin	$⊢ A (({({1^{st} ↾}_{(V \times V)})}^{-1} \circ R) \cap ({({2^{nd} ↾}_{(V \times V)})}^{-1} \circ S)) ⟨B, C⟩ \leftrightarrow (A ({({1^{st} ↾}_{(V \times V)})}^{-1} \circ R) ⟨B, C⟩ \land A ({({2^{nd} ↾}_{(V \times V)})}^{-1} \circ S) ⟨B, C⟩)$
5	4	a1i	$⊢ (A \in V \land B \in W \land C \in X) \to (A (({({1^{st} ↾}_{(V \times V)})}^{-1} \circ R) \cap ({({2^{nd} ↾}_{(V \times V)})}^{-1} \circ S)) ⟨B, C⟩ \leftrightarrow (A ({({1^{st} ↾}_{(V \times V)})}^{-1} \circ R) ⟨B, C⟩ \land A ({({2^{nd} ↾}_{(V \times V)})}^{-1} \circ S) ⟨B, C⟩))$
6		opex	$⊢ ⟨B, C⟩ \in V$
7		brcog	$⊢ (A \in V \land ⟨B, C⟩ \in V) \to (A ({({1^{st} ↾}_{(V \times V)})}^{-1} \circ R) ⟨B, C⟩ \leftrightarrow \exists x (A R x \land x {({1^{st} ↾}_{(V \times V)})}^{-1} ⟨B, C⟩))$
8	6 7	mpan2	$⊢ A \in V \to (A ({({1^{st} ↾}_{(V \times V)})}^{-1} \circ R) ⟨B, C⟩ \leftrightarrow \exists x (A R x \land x {({1^{st} ↾}_{(V \times V)})}^{-1} ⟨B, C⟩))$
9	8	3ad2ant1	$⊢ (A \in V \land B \in W \land C \in X) \to (A ({({1^{st} ↾}_{(V \times V)})}^{-1} \circ R) ⟨B, C⟩ \leftrightarrow \exists x (A R x \land x {({1^{st} ↾}_{(V \times V)})}^{-1} ⟨B, C⟩))$
10		brcnvg	$⊢ (x \in V \land ⟨B, C⟩ \in V) \to (x {({1^{st} ↾}_{(V \times V)})}^{-1} ⟨B, C⟩ \leftrightarrow ⟨B, C⟩ ({1^{st} ↾}_{(V \times V)}) x)$
11	6 10	mpan2	$⊢ x \in V \to (x {({1^{st} ↾}_{(V \times V)})}^{-1} ⟨B, C⟩ \leftrightarrow ⟨B, C⟩ ({1^{st} ↾}_{(V \times V)}) x)$
12	11	elv	$⊢ x {({1^{st} ↾}_{(V \times V)})}^{-1} ⟨B, C⟩ \leftrightarrow ⟨B, C⟩ ({1^{st} ↾}_{(V \times V)}) x$
13		brres	$⊢ x \in V \to (⟨B, C⟩ ({1^{st} ↾}_{(V \times V)}) x \leftrightarrow (⟨B, C⟩ \in (V \times V) \land ⟨B, C⟩ 1^{st} x))$
14	13	elv	$⊢ ⟨B, C⟩ ({1^{st} ↾}_{(V \times V)}) x \leftrightarrow (⟨B, C⟩ \in (V \times V) \land ⟨B, C⟩ 1^{st} x)$
15		opelvvg	$⊢ (B \in W \land C \in X) \to ⟨B, C⟩ \in (V \times V)$
16	15	biantrurd	$⊢ (B \in W \land C \in X) \to (⟨B, C⟩ 1^{st} x \leftrightarrow (⟨B, C⟩ \in (V \times V) \land ⟨B, C⟩ 1^{st} x))$
17	14 16	bitr4id	$⊢ (B \in W \land C \in X) \to (⟨B, C⟩ ({1^{st} ↾}_{(V \times V)}) x \leftrightarrow ⟨B, C⟩ 1^{st} x)$
18		br1steqg	$⊢ (B \in W \land C \in X) \to (⟨B, C⟩ 1^{st} x \leftrightarrow x = B)$
19	17 18	bitrd	$⊢ (B \in W \land C \in X) \to (⟨B, C⟩ ({1^{st} ↾}_{(V \times V)}) x \leftrightarrow x = B)$
20	19	3adant1	$⊢ (A \in V \land B \in W \land C \in X) \to (⟨B, C⟩ ({1^{st} ↾}_{(V \times V)}) x \leftrightarrow x = B)$
21	12 20	syl5bb	$⊢ (A \in V \land B \in W \land C \in X) \to (x {({1^{st} ↾}_{(V \times V)})}^{-1} ⟨B, C⟩ \leftrightarrow x = B)$
22	21	anbi1cd	$⊢ (A \in V \land B \in W \land C \in X) \to ((A R x \land x {({1^{st} ↾}_{(V \times V)})}^{-1} ⟨B, C⟩) \leftrightarrow (x = B \land A R x))$
23	22	exbidv	$⊢ (A \in V \land B \in W \land C \in X) \to (\exists x (A R x \land x {({1^{st} ↾}_{(V \times V)})}^{-1} ⟨B, C⟩) \leftrightarrow \exists x (x = B \land A R x))$
24		breq2	$⊢ x = B \to (A R x \leftrightarrow A R B)$
25	24	ceqsexgv	$⊢ B \in W \to (\exists x (x = B \land A R x) \leftrightarrow A R B)$
26	25	3ad2ant2	$⊢ (A \in V \land B \in W \land C \in X) \to (\exists x (x = B \land A R x) \leftrightarrow A R B)$
27	9 23 26	3bitrd	$⊢ (A \in V \land B \in W \land C \in X) \to (A ({({1^{st} ↾}_{(V \times V)})}^{-1} \circ R) ⟨B, C⟩ \leftrightarrow A R B)$
28		brcog	$⊢ (A \in V \land ⟨B, C⟩ \in V) \to (A ({({2^{nd} ↾}_{(V \times V)})}^{-1} \circ S) ⟨B, C⟩ \leftrightarrow \exists y (A S y \land y {({2^{nd} ↾}_{(V \times V)})}^{-1} ⟨B, C⟩))$
29	6 28	mpan2	$⊢ A \in V \to (A ({({2^{nd} ↾}_{(V \times V)})}^{-1} \circ S) ⟨B, C⟩ \leftrightarrow \exists y (A S y \land y {({2^{nd} ↾}_{(V \times V)})}^{-1} ⟨B, C⟩))$
30	29	3ad2ant1	$⊢ (A \in V \land B \in W \land C \in X) \to (A ({({2^{nd} ↾}_{(V \times V)})}^{-1} \circ S) ⟨B, C⟩ \leftrightarrow \exists y (A S y \land y {({2^{nd} ↾}_{(V \times V)})}^{-1} ⟨B, C⟩))$
31		brcnvg	$⊢ (y \in V \land ⟨B, C⟩ \in V) \to (y {({2^{nd} ↾}_{(V \times V)})}^{-1} ⟨B, C⟩ \leftrightarrow ⟨B, C⟩ ({2^{nd} ↾}_{(V \times V)}) y)$
32	6 31	mpan2	$⊢ y \in V \to (y {({2^{nd} ↾}_{(V \times V)})}^{-1} ⟨B, C⟩ \leftrightarrow ⟨B, C⟩ ({2^{nd} ↾}_{(V \times V)}) y)$
33	32	elv	$⊢ y {({2^{nd} ↾}_{(V \times V)})}^{-1} ⟨B, C⟩ \leftrightarrow ⟨B, C⟩ ({2^{nd} ↾}_{(V \times V)}) y$
34		brres	$⊢ y \in V \to (⟨B, C⟩ ({2^{nd} ↾}_{(V \times V)}) y \leftrightarrow (⟨B, C⟩ \in (V \times V) \land ⟨B, C⟩ 2^{nd} y))$
35	34	elv	$⊢ ⟨B, C⟩ ({2^{nd} ↾}_{(V \times V)}) y \leftrightarrow (⟨B, C⟩ \in (V \times V) \land ⟨B, C⟩ 2^{nd} y)$
36	15	biantrurd	$⊢ (B \in W \land C \in X) \to (⟨B, C⟩ 2^{nd} y \leftrightarrow (⟨B, C⟩ \in (V \times V) \land ⟨B, C⟩ 2^{nd} y))$
37	35 36	bitr4id	$⊢ (B \in W \land C \in X) \to (⟨B, C⟩ ({2^{nd} ↾}_{(V \times V)}) y \leftrightarrow ⟨B, C⟩ 2^{nd} y)$
38		br2ndeqg	$⊢ (B \in W \land C \in X) \to (⟨B, C⟩ 2^{nd} y \leftrightarrow y = C)$
39	37 38	bitrd	$⊢ (B \in W \land C \in X) \to (⟨B, C⟩ ({2^{nd} ↾}_{(V \times V)}) y \leftrightarrow y = C)$
40	39	3adant1	$⊢ (A \in V \land B \in W \land C \in X) \to (⟨B, C⟩ ({2^{nd} ↾}_{(V \times V)}) y \leftrightarrow y = C)$
41	33 40	syl5bb	$⊢ (A \in V \land B \in W \land C \in X) \to (y {({2^{nd} ↾}_{(V \times V)})}^{-1} ⟨B, C⟩ \leftrightarrow y = C)$
42	41	anbi1cd	$⊢ (A \in V \land B \in W \land C \in X) \to ((A S y \land y {({2^{nd} ↾}_{(V \times V)})}^{-1} ⟨B, C⟩) \leftrightarrow (y = C \land A S y))$
43	42	exbidv	$⊢ (A \in V \land B \in W \land C \in X) \to (\exists y (A S y \land y {({2^{nd} ↾}_{(V \times V)})}^{-1} ⟨B, C⟩) \leftrightarrow \exists y (y = C \land A S y))$
44		breq2	$⊢ y = C \to (A S y \leftrightarrow A S C)$
45	44	ceqsexgv	$⊢ C \in X \to (\exists y (y = C \land A S y) \leftrightarrow A S C)$
46	45	3ad2ant3	$⊢ (A \in V \land B \in W \land C \in X) \to (\exists y (y = C \land A S y) \leftrightarrow A S C)$
47	30 43 46	3bitrd	$⊢ (A \in V \land B \in W \land C \in X) \to (A ({({2^{nd} ↾}_{(V \times V)})}^{-1} \circ S) ⟨B, C⟩ \leftrightarrow A S C)$
48	27 47	anbi12d	$⊢ (A \in V \land B \in W \land C \in X) \to ((A ({({1^{st} ↾}_{(V \times V)})}^{-1} \circ R) ⟨B, C⟩ \land A ({({2^{nd} ↾}_{(V \times V)})}^{-1} \circ S) ⟨B, C⟩) \leftrightarrow (A R B \land A S C))$
49	3 5 48	3bitrd	$⊢ (A \in V \land B \in W \land C \in X) \to (A R ⋉ S ⟨B, C⟩ \leftrightarrow (A R B \land A S C))$

Metamath Proof Explorer

Theorem brxrn

Proof