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 ⊢ 𝐴 ∈ V
Assertion brtxp2 ( 𝐴 ( 𝑅 ⊗ 𝑆 ) 𝐵 ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐴 𝑅 𝑥 ∧ 𝐴 𝑆 𝑦 ) )

Proof

Step Hyp Ref Expression
1 brtxp2.1 ⊢ 𝐴 ∈ V
2 txpss3v ⊢ ( 𝑅 ⊗ 𝑆 ) ⊆ ( V × ( V × V ) )
3 2 brel ⊢ ( 𝐴 ( 𝑅 ⊗ 𝑆 ) 𝐵 → ( 𝐴 ∈ V ∧ 𝐵 ∈ ( V × V ) ) )
4 3 simprd ⊢ ( 𝐴 ( 𝑅 ⊗ 𝑆 ) 𝐵 → 𝐵 ∈ ( V × V ) )
5 elvv ⊢ ( 𝐵 ∈ ( V × V ) ↔ ∃ 𝑥 ∃ 𝑦 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ )
6 4 5 sylib ⊢ ( 𝐴 ( 𝑅 ⊗ 𝑆 ) 𝐵 → ∃ 𝑥 ∃ 𝑦 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ )
7 6 pm4.71ri ⊢ ( 𝐴 ( 𝑅 ⊗ 𝑆 ) 𝐵 ↔ ( ∃ 𝑥 ∃ 𝑦 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐴 ( 𝑅 ⊗ 𝑆 ) 𝐵 ) )
8 19.41vv ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐴 ( 𝑅 ⊗ 𝑆 ) 𝐵 ) ↔ ( ∃ 𝑥 ∃ 𝑦 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐴 ( 𝑅 ⊗ 𝑆 ) 𝐵 ) )
9 7 8 bitr4i ⊢ ( 𝐴 ( 𝑅 ⊗ 𝑆 ) 𝐵 ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐴 ( 𝑅 ⊗ 𝑆 ) 𝐵 ) )
10 breq2 ⊢ ( 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐴 ( 𝑅 ⊗ 𝑆 ) 𝐵 ↔ 𝐴 ( 𝑅 ⊗ 𝑆 ) ⟨ 𝑥 , 𝑦 ⟩ ) )
11 10 pm5.32i ⊢ ( ( 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐴 ( 𝑅 ⊗ 𝑆 ) 𝐵 ) ↔ ( 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐴 ( 𝑅 ⊗ 𝑆 ) ⟨ 𝑥 , 𝑦 ⟩ ) )
12 11 2exbii ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐴 ( 𝑅 ⊗ 𝑆 ) 𝐵 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐴 ( 𝑅 ⊗ 𝑆 ) ⟨ 𝑥 , 𝑦 ⟩ ) )
13 vex ⊢ 𝑥 ∈ V
14 vex ⊢ 𝑦 ∈ V
15 1 13 14 brtxp ⊢ ( 𝐴 ( 𝑅 ⊗ 𝑆 ) ⟨ 𝑥 , 𝑦 ⟩ ↔ ( 𝐴 𝑅 𝑥 ∧ 𝐴 𝑆 𝑦 ) )
16 15 anbi2i ⊢ ( ( 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐴 ( 𝑅 ⊗ 𝑆 ) ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ( 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝐴 𝑅 𝑥 ∧ 𝐴 𝑆 𝑦 ) ) )
17 3anass ⊢ ( ( 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐴 𝑅 𝑥 ∧ 𝐴 𝑆 𝑦 ) ↔ ( 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝐴 𝑅 𝑥 ∧ 𝐴 𝑆 𝑦 ) ) )
18 16 17 bitr4i ⊢ ( ( 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐴 ( 𝑅 ⊗ 𝑆 ) ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ( 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐴 𝑅 𝑥 ∧ 𝐴 𝑆 𝑦 ) )
19 18 2exbii ⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐴 ( 𝑅 ⊗ 𝑆 ) ⟨ 𝑥 , 𝑦 ⟩ ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐴 𝑅 𝑥 ∧ 𝐴 𝑆 𝑦 ) )
20 9 12 19 3bitri ⊢ ( 𝐴 ( 𝑅 ⊗ 𝑆 ) 𝐵 ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐵 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝐴 𝑅 𝑥 ∧ 𝐴 𝑆 𝑦 ) )