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 ) )