Theorem brtxp2

Description: The binary relation over a tail cross when the second argument is not an ordered pair. (Contributed by Scott Fenton, 14-Apr-2014) (Revised by Mario Carneiro, 3-May-2015)

	Ref	Expression
Hypothesis	brtxp2.1	$$⊢A\in \mathrm{V}$$
Assertion	brtxp2	$$⊢A\left(R\otimes S\right)B\leftrightarrow \exists x\exists y\left(B=⟨x,y⟩\wedge ARx\wedge ASy\right)$$

Proof

Step	Hyp	Ref	Expression
1		brtxp2.1	$$⊢A\in \mathrm{V}$$
2		txpss3v	$$⊢\left(R\otimes S\right)\subseteq \mathrm{V}\times \left(\mathrm{V}\times \mathrm{V}\right)$$
3	2	brel	$$⊢A\left(R\otimes S\right)B\to \left(A\in \mathrm{V}\wedge B\in \left(\mathrm{V}\times \mathrm{V}\right)\right)$$
4	3	simprd	$$⊢A\left(R\otimes S\right)B\to B\in \left(\mathrm{V}\times \mathrm{V}\right)$$
5		elvv	$$⊢B\in \left(\mathrm{V}\times \mathrm{V}\right)\leftrightarrow \exists x\exists yB=⟨x,y⟩$$
6	4 5	sylib	$$⊢A\left(R\otimes S\right)B\to \exists x\exists yB=⟨x,y⟩$$
7	6	pm4.71ri	$$⊢A\left(R\otimes S\right)B\leftrightarrow \left(\exists x\exists yB=⟨x,y⟩\wedge A\left(R\otimes S\right)B\right)$$
8		19.41vv	$$⊢\exists x\exists y\left(B=⟨x,y⟩\wedge A\left(R\otimes S\right)B\right)\leftrightarrow \left(\exists x\exists yB=⟨x,y⟩\wedge A\left(R\otimes S\right)B\right)$$
9	7 8	bitr4i	$$⊢A\left(R\otimes S\right)B\leftrightarrow \exists x\exists y\left(B=⟨x,y⟩\wedge A\left(R\otimes S\right)B\right)$$
10		breq2	$$⊢B=⟨x,y⟩\to \left(A\left(R\otimes S\right)B\leftrightarrow A\left(R\otimes S\right)⟨x,y⟩\right)$$
11	10	pm5.32i	$$⊢\left(B=⟨x,y⟩\wedge A\left(R\otimes S\right)B\right)\leftrightarrow \left(B=⟨x,y⟩\wedge A\left(R\otimes S\right)⟨x,y⟩\right)$$
12	11	2exbii	$$⊢\exists x\exists y\left(B=⟨x,y⟩\wedge A\left(R\otimes S\right)B\right)\leftrightarrow \exists x\exists y\left(B=⟨x,y⟩\wedge A\left(R\otimes S\right)⟨x,y⟩\right)$$
13		vex	$$⊢x\in \mathrm{V}$$
14		vex	$$⊢y\in \mathrm{V}$$
15	1 13 14	brtxp	$$⊢A\left(R\otimes S\right)⟨x,y⟩\leftrightarrow \left(ARx\wedge ASy\right)$$
16	15	anbi2i	$$⊢\left(B=⟨x,y⟩\wedge A\left(R\otimes S\right)⟨x,y⟩\right)\leftrightarrow \left(B=⟨x,y⟩\wedge \left(ARx\wedge ASy\right)\right)$$
17		3anass	$$⊢\left(B=⟨x,y⟩\wedge ARx\wedge ASy\right)\leftrightarrow \left(B=⟨x,y⟩\wedge \left(ARx\wedge ASy\right)\right)$$
18	16 17	bitr4i	$$⊢\left(B=⟨x,y⟩\wedge A\left(R\otimes S\right)⟨x,y⟩\right)\leftrightarrow \left(B=⟨x,y⟩\wedge ARx\wedge ASy\right)$$
19	18	2exbii	$$⊢\exists x\exists y\left(B=⟨x,y⟩\wedge A\left(R\otimes S\right)⟨x,y⟩\right)\leftrightarrow \exists x\exists y\left(B=⟨x,y⟩\wedge ARx\wedge ASy\right)$$
20	9 12 19	3bitri	$$⊢A\left(R\otimes S\right)B\leftrightarrow \exists x\exists y\left(B=⟨x,y⟩\wedge ARx\wedge ASy\right)$$