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

Metamath Proof Explorer

Theorem 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 e. _V
brtxp.2 
|- Y e. _V
brtxp.3 
|- Z e. _V
Assertion brtxp 
|- ( X ( A (x) B ) <. Y , Z >. <-> ( X A Y /\ X B Z ) )

Proof

Step Hyp Ref Expression
1 brtxp.1 
 |-  X e. _V
2 brtxp.2 
 |-  Y e. _V
3 brtxp.3 
 |-  Z e. _V
4 df-txp 
 |-  ( A (x) B ) = ( ( `' ( 1st |` ( _V X. _V ) ) o. A ) i^i ( `' ( 2nd |` ( _V X. _V ) ) o. B ) )
5 4 breqi 
 |-  ( X ( A (x) B ) <. Y , Z >. <-> X ( ( `' ( 1st |` ( _V X. _V ) ) o. A ) i^i ( `' ( 2nd |` ( _V X. _V ) ) o. B ) ) <. Y , Z >. )
6 brin 
 |-  ( X ( ( `' ( 1st |` ( _V X. _V ) ) o. A ) i^i ( `' ( 2nd |` ( _V X. _V ) ) o. B ) ) <. Y , Z >. <-> ( X ( `' ( 1st |` ( _V X. _V ) ) o. A ) <. Y , Z >. /\ X ( `' ( 2nd |` ( _V X. _V ) ) o. B ) <. Y , Z >. ) )
7 opex 
 |-  <. Y , Z >. e. _V
8 1 7 brco 
 |-  ( X ( `' ( 1st |` ( _V X. _V ) ) o. A ) <. Y , Z >. <-> E. y ( X A y /\ y `' ( 1st |` ( _V X. _V ) ) <. Y , Z >. ) )
9 vex 
 |-  y e. _V
10 9 7 brcnv 
 |-  ( y `' ( 1st |` ( _V X. _V ) ) <. Y , Z >. <-> <. Y , Z >. ( 1st |` ( _V X. _V ) ) y )
11 2 3 opelvv 
 |-  <. Y , Z >. e. ( _V X. _V )
12 9 brresi 
 |-  ( <. Y , Z >. ( 1st |` ( _V X. _V ) ) y <-> ( <. Y , Z >. e. ( _V X. _V ) /\ <. Y , Z >. 1st y ) )
13 11 12 mpbiran 
 |-  ( <. Y , Z >. ( 1st |` ( _V X. _V ) ) y <-> <. Y , Z >. 1st y )
14 2 3 br1steq 
 |-  ( <. Y , Z >. 1st y <-> y = Y )
15 10 13 14 3bitri 
 |-  ( y `' ( 1st |` ( _V X. _V ) ) <. Y , Z >. <-> y = Y )
16 15 anbi1ci 
 |-  ( ( X A y /\ y `' ( 1st |` ( _V X. _V ) ) <. Y , Z >. ) <-> ( y = Y /\ X A y ) )
17 16 exbii 
 |-  ( E. y ( X A y /\ y `' ( 1st |` ( _V X. _V ) ) <. Y , Z >. ) <-> E. y ( y = Y /\ X A y ) )
18 breq2 
 |-  ( y = Y -> ( X A y <-> X A Y ) )
19 2 18 ceqsexv 
 |-  ( E. y ( y = Y /\ X A y ) <-> X A Y )
20 8 17 19 3bitri 
 |-  ( X ( `' ( 1st |` ( _V X. _V ) ) o. A ) <. Y , Z >. <-> X A Y )
21 1 7 brco 
 |-  ( X ( `' ( 2nd |` ( _V X. _V ) ) o. B ) <. Y , Z >. <-> E. z ( X B z /\ z `' ( 2nd |` ( _V X. _V ) ) <. Y , Z >. ) )
22 vex 
 |-  z e. _V
23 22 7 brcnv 
 |-  ( z `' ( 2nd |` ( _V X. _V ) ) <. Y , Z >. <-> <. Y , Z >. ( 2nd |` ( _V X. _V ) ) z )
24 22 brresi 
 |-  ( <. Y , Z >. ( 2nd |` ( _V X. _V ) ) z <-> ( <. Y , Z >. e. ( _V X. _V ) /\ <. Y , Z >. 2nd z ) )
25 11 24 mpbiran 
 |-  ( <. Y , Z >. ( 2nd |` ( _V X. _V ) ) z <-> <. Y , Z >. 2nd z )
26 2 3 br2ndeq 
 |-  ( <. Y , Z >. 2nd z <-> z = Z )
27 23 25 26 3bitri 
 |-  ( z `' ( 2nd |` ( _V X. _V ) ) <. Y , Z >. <-> z = Z )
28 27 anbi1ci 
 |-  ( ( X B z /\ z `' ( 2nd |` ( _V X. _V ) ) <. Y , Z >. ) <-> ( z = Z /\ X B z ) )
29 28 exbii 
 |-  ( E. z ( X B z /\ z `' ( 2nd |` ( _V X. _V ) ) <. Y , Z >. ) <-> E. z ( z = Z /\ X B z ) )
30 breq2 
 |-  ( z = Z -> ( X B z <-> X B Z ) )
31 3 30 ceqsexv 
 |-  ( E. z ( z = Z /\ X B z ) <-> X B Z )
32 21 29 31 3bitri 
 |-  ( X ( `' ( 2nd |` ( _V X. _V ) ) o. B ) <. Y , Z >. <-> X B Z )
33 20 32 anbi12i 
 |-  ( ( X ( `' ( 1st |` ( _V X. _V ) ) o. A ) <. Y , Z >. /\ X ( `' ( 2nd |` ( _V X. _V ) ) o. B ) <. Y , Z >. ) <-> ( X A Y /\ X B Z ) )
34 5 6 33 3bitri 
 |-  ( X ( A (x) B ) <. Y , Z >. <-> ( X A Y /\ X B Z ) )