This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∈ V
Assertion brtxp2 ⊢ A R ⊗ S B ↔ ∃ x ∃ y B = x y ∧ A R x ∧ A S y

Proof

Step Hyp Ref Expression
1 brtxp2.1 ⊢ A ∈ V
2 txpss3v ⊢ R ⊗ S ⊆ V × V × V
3 2 brel ⊢ A R ⊗ S B → A ∈ V ∧ B ∈ V × V
4 3 simprd ⊢ A R ⊗ S B → B ∈ V × V
5 elvv ⊢ B ∈ V × V ↔ ∃ x ∃ y B = x y
6 4 5 sylib ⊢ A R ⊗ S B → ∃ x ∃ y B = x y
7 6 pm4.71ri ⊢ A R ⊗ S B ↔ ∃ x ∃ y B = x y ∧ A R ⊗ S B
8 19.41vv ⊢ ∃ x ∃ y B = x y ∧ A R ⊗ S B ↔ ∃ x ∃ y B = x y ∧ A R ⊗ S B
9 7 8 bitr4i ⊢ A R ⊗ S B ↔ ∃ x ∃ y B = x y ∧ A R ⊗ S B
10 breq2 ⊢ B = x y → A R ⊗ S B ↔ A R ⊗ S x y
11 10 pm5.32i ⊢ B = x y ∧ A R ⊗ S B ↔ B = x y ∧ A R ⊗ S x y
12 11 2exbii ⊢ ∃ x ∃ y B = x y ∧ A R ⊗ S B ↔ ∃ x ∃ y B = x y ∧ A R ⊗ S x y
13 vex ⊢ x ∈ V
14 vex ⊢ y ∈ V
15 1 13 14 brtxp ⊢ A R ⊗ S x y ↔ A R x ∧ A S y
16 15 anbi2i ⊢ B = x y ∧ A R ⊗ S x y ↔ B = x y ∧ A R x ∧ A S y
17 3anass ⊢ B = x y ∧ A R x ∧ A S y ↔ B = x y ∧ A R x ∧ A S y
18 16 17 bitr4i ⊢ B = x y ∧ A R ⊗ S x y ↔ B = x y ∧ A R x ∧ A S y
19 18 2exbii ⊢ ∃ x ∃ y B = x y ∧ A R ⊗ S x y ↔ ∃ x ∃ y B = x y ∧ A R x ∧ A S y
20 9 12 19 3bitri ⊢ A R ⊗ S B ↔ ∃ x ∃ y B = x y ∧ A R x ∧ A S y