brtxp

Description: Characterize a ternary relation over a tail Cartesian product. Together with txpss3v , this completely defines membership in a tail cross. (Contributed by Scott Fenton, 31-Mar-2012) (Proof shortened by Peter Mazsa, 2-Oct-2022)

	Ref	Expression
Hypotheses	brtxp.1	$⊢ X \in V$
	brtxp.2	$⊢ Y \in V$
	brtxp.3	$⊢ Z \in V$
Assertion	brtxp	$⊢ X (A \otimes B) ⟨Y, Z⟩ \leftrightarrow (X A Y \land X B Z)$

Proof

Step	Hyp	Ref	Expression
1		brtxp.1	$⊢ X \in V$
2		brtxp.2	$⊢ Y \in V$
3		brtxp.3	$⊢ Z \in V$
4		df-txp	$⊢ (A \otimes B) = ({({1^{st} ↾}_{(V \times V)})}^{-1} \circ A) \cap ({({2^{nd} ↾}_{(V \times V)})}^{-1} \circ B)$
5	4	breqi	$⊢ X (A \otimes B) ⟨Y, Z⟩ \leftrightarrow X (({({1^{st} ↾}_{(V \times V)})}^{-1} \circ A) \cap ({({2^{nd} ↾}_{(V \times V)})}^{-1} \circ B)) ⟨Y, Z⟩$
6		brin	$⊢ X (({({1^{st} ↾}_{(V \times V)})}^{-1} \circ A) \cap ({({2^{nd} ↾}_{(V \times V)})}^{-1} \circ B)) ⟨Y, Z⟩ \leftrightarrow (X ({({1^{st} ↾}_{(V \times V)})}^{-1} \circ A) ⟨Y, Z⟩ \land X ({({2^{nd} ↾}_{(V \times V)})}^{-1} \circ B) ⟨Y, Z⟩)$
7		opex	$⊢ ⟨Y, Z⟩ \in V$
8	1 7	brco	$⊢ X ({({1^{st} ↾}_{(V \times V)})}^{-1} \circ A) ⟨Y, Z⟩ \leftrightarrow \exists y (X A y \land y {({1^{st} ↾}_{(V \times V)})}^{-1} ⟨Y, Z⟩)$
9		vex	$⊢ y \in V$
10	9 7	brcnv	$⊢ y {({1^{st} ↾}_{(V \times V)})}^{-1} ⟨Y, Z⟩ \leftrightarrow ⟨Y, Z⟩ ({1^{st} ↾}_{(V \times V)}) y$
11	2 3	opelvv	$⊢ ⟨Y, Z⟩ \in (V \times V)$
12	9	brresi	$⊢ ⟨Y, Z⟩ ({1^{st} ↾}_{(V \times V)}) y \leftrightarrow (⟨Y, Z⟩ \in (V \times V) \land ⟨Y, Z⟩ 1^{st} y)$
13	11 12	mpbiran	$⊢ ⟨Y, Z⟩ ({1^{st} ↾}_{(V \times V)}) y \leftrightarrow ⟨Y, Z⟩ 1^{st} y$
14	2 3	br1steq	$⊢ ⟨Y, Z⟩ 1^{st} y \leftrightarrow y = Y$
15	10 13 14	3bitri	$⊢ y {({1^{st} ↾}_{(V \times V)})}^{-1} ⟨Y, Z⟩ \leftrightarrow y = Y$
16	15	anbi1ci	$⊢ (X A y \land y {({1^{st} ↾}_{(V \times V)})}^{-1} ⟨Y, Z⟩) \leftrightarrow (y = Y \land X A y)$
17	16	exbii	$⊢ \exists y (X A y \land y {({1^{st} ↾}_{(V \times V)})}^{-1} ⟨Y, Z⟩) \leftrightarrow \exists y (y = Y \land X A y)$
18		breq2	$⊢ y = Y \to (X A y \leftrightarrow X A Y)$
19	2 18	ceqsexv	$⊢ \exists y (y = Y \land X A y) \leftrightarrow X A Y$
20	8 17 19	3bitri	$⊢ X ({({1^{st} ↾}_{(V \times V)})}^{-1} \circ A) ⟨Y, Z⟩ \leftrightarrow X A Y$
21	1 7	brco	$⊢ X ({({2^{nd} ↾}_{(V \times V)})}^{-1} \circ B) ⟨Y, Z⟩ \leftrightarrow \exists z (X B z \land z {({2^{nd} ↾}_{(V \times V)})}^{-1} ⟨Y, Z⟩)$
22		vex	$⊢ z \in V$
23	22 7	brcnv	$⊢ z {({2^{nd} ↾}_{(V \times V)})}^{-1} ⟨Y, Z⟩ \leftrightarrow ⟨Y, Z⟩ ({2^{nd} ↾}_{(V \times V)}) z$
24	22	brresi	$⊢ ⟨Y, Z⟩ ({2^{nd} ↾}_{(V \times V)}) z \leftrightarrow (⟨Y, Z⟩ \in (V \times V) \land ⟨Y, Z⟩ 2^{nd} z)$
25	11 24	mpbiran	$⊢ ⟨Y, Z⟩ ({2^{nd} ↾}_{(V \times V)}) z \leftrightarrow ⟨Y, Z⟩ 2^{nd} z$
26	2 3	br2ndeq	$⊢ ⟨Y, Z⟩ 2^{nd} z \leftrightarrow z = Z$
27	23 25 26	3bitri	$⊢ z {({2^{nd} ↾}_{(V \times V)})}^{-1} ⟨Y, Z⟩ \leftrightarrow z = Z$
28	27	anbi1ci	$⊢ (X B z \land z {({2^{nd} ↾}_{(V \times V)})}^{-1} ⟨Y, Z⟩) \leftrightarrow (z = Z \land X B z)$
29	28	exbii	$⊢ \exists z (X B z \land z {({2^{nd} ↾}_{(V \times V)})}^{-1} ⟨Y, Z⟩) \leftrightarrow \exists z (z = Z \land X B z)$
30		breq2	$⊢ z = Z \to (X B z \leftrightarrow X B Z)$
31	3 30	ceqsexv	$⊢ \exists z (z = Z \land X B z) \leftrightarrow X B Z$
32	21 29 31	3bitri	$⊢ X ({({2^{nd} ↾}_{(V \times V)})}^{-1} \circ B) ⟨Y, Z⟩ \leftrightarrow X B Z$
33	20 32	anbi12i	$⊢ (X ({({1^{st} ↾}_{(V \times V)})}^{-1} \circ A) ⟨Y, Z⟩ \land X ({({2^{nd} ↾}_{(V \times V)})}^{-1} \circ B) ⟨Y, Z⟩) \leftrightarrow (X A Y \land X B Z)$
34	5 6 33	3bitri	$⊢ X (A \otimes B) ⟨Y, Z⟩ \leftrightarrow (X A Y \land X B Z)$

Metamath Proof Explorer

Theorem brtxp

Proof