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

Metamath Proof Explorer

Theorem brab2d

Description: Expressing that two sets are related by a binary relation which is expressed as a class abstraction of ordered pairs. (Contributed by Thierry Arnoux, 4-May-2025)

Ref Expression
Hypotheses brab2d.1 
|- ( ph -> R = { <. x , y >. | ( ( x e. U /\ y e. V ) /\ ps ) } )
brab2d.2 
|- ( ( ph /\ ( x = A /\ y = B ) ) -> ( ps <-> ch ) )
Assertion brab2d 
|- ( ph -> ( A R B <-> ( ( A e. U /\ B e. V ) /\ ch ) ) )

Proof

Step Hyp Ref Expression
1 brab2d.1 
 |-  ( ph -> R = { <. x , y >. | ( ( x e. U /\ y e. V ) /\ ps ) } )
2 brab2d.2 
 |-  ( ( ph /\ ( x = A /\ y = B ) ) -> ( ps <-> ch ) )
3 df-br 
 |-  ( A R B <-> <. A , B >. e. R )
4 1 eleq2d 
 |-  ( ph -> ( <. A , B >. e. R <-> <. A , B >. e. { <. x , y >. | ( ( x e. U /\ y e. V ) /\ ps ) } ) )
5 3 4 bitrid 
 |-  ( ph -> ( A R B <-> <. A , B >. e. { <. x , y >. | ( ( x e. U /\ y e. V ) /\ ps ) } ) )
6 elopab 
 |-  ( <. A , B >. e. { <. x , y >. | ( ( x e. U /\ y e. V ) /\ ps ) } <-> E. x E. y ( <. A , B >. = <. x , y >. /\ ( ( x e. U /\ y e. V ) /\ ps ) ) )
7 5 6 bitrdi 
 |-  ( ph -> ( A R B <-> E. x E. y ( <. A , B >. = <. x , y >. /\ ( ( x e. U /\ y e. V ) /\ ps ) ) ) )
8 eqcom 
 |-  ( <. x , y >. = <. A , B >. <-> <. A , B >. = <. x , y >. )
9 vex 
 |-  x e. _V
10 vex 
 |-  y e. _V
11 9 10 opth 
 |-  ( <. x , y >. = <. A , B >. <-> ( x = A /\ y = B ) )
12 8 11 sylbb1 
 |-  ( <. A , B >. = <. x , y >. -> ( x = A /\ y = B ) )
13 eleq1 
 |-  ( x = A -> ( x e. U <-> A e. U ) )
14 eleq1 
 |-  ( y = B -> ( y e. V <-> B e. V ) )
15 13 14 bi2anan9 
 |-  ( ( x = A /\ y = B ) -> ( ( x e. U /\ y e. V ) <-> ( A e. U /\ B e. V ) ) )
16 15 biimpa 
 |-  ( ( ( x = A /\ y = B ) /\ ( x e. U /\ y e. V ) ) -> ( A e. U /\ B e. V ) )
17 12 16 sylan 
 |-  ( ( <. A , B >. = <. x , y >. /\ ( x e. U /\ y e. V ) ) -> ( A e. U /\ B e. V ) )
18 17 adantl 
 |-  ( ( ph /\ ( <. A , B >. = <. x , y >. /\ ( x e. U /\ y e. V ) ) ) -> ( A e. U /\ B e. V ) )
19 18 adantrrr 
 |-  ( ( ph /\ ( <. A , B >. = <. x , y >. /\ ( ( x e. U /\ y e. V ) /\ ps ) ) ) -> ( A e. U /\ B e. V ) )
20 19 ex 
 |-  ( ph -> ( ( <. A , B >. = <. x , y >. /\ ( ( x e. U /\ y e. V ) /\ ps ) ) -> ( A e. U /\ B e. V ) ) )
21 20 exlimdvv 
 |-  ( ph -> ( E. x E. y ( <. A , B >. = <. x , y >. /\ ( ( x e. U /\ y e. V ) /\ ps ) ) -> ( A e. U /\ B e. V ) ) )
22 21 imp 
 |-  ( ( ph /\ E. x E. y ( <. A , B >. = <. x , y >. /\ ( ( x e. U /\ y e. V ) /\ ps ) ) ) -> ( A e. U /\ B e. V ) )
23 simprl 
 |-  ( ( ph /\ ( ( A e. U /\ B e. V ) /\ ch ) ) -> ( A e. U /\ B e. V ) )
24 simprl 
 |-  ( ( ph /\ ( A e. U /\ B e. V ) ) -> A e. U )
25 simprr 
 |-  ( ( ph /\ ( A e. U /\ B e. V ) ) -> B e. V )
26 15 adantl 
 |-  ( ( ph /\ ( x = A /\ y = B ) ) -> ( ( x e. U /\ y e. V ) <-> ( A e. U /\ B e. V ) ) )
27 26 2 anbi12d 
 |-  ( ( ph /\ ( x = A /\ y = B ) ) -> ( ( ( x e. U /\ y e. V ) /\ ps ) <-> ( ( A e. U /\ B e. V ) /\ ch ) ) )
28 27 adantlr 
 |-  ( ( ( ph /\ ( A e. U /\ B e. V ) ) /\ ( x = A /\ y = B ) ) -> ( ( ( x e. U /\ y e. V ) /\ ps ) <-> ( ( A e. U /\ B e. V ) /\ ch ) ) )
29 24 25 28 copsex2dv 
 |-  ( ( ph /\ ( A e. U /\ B e. V ) ) -> ( E. x E. y ( <. A , B >. = <. x , y >. /\ ( ( x e. U /\ y e. V ) /\ ps ) ) <-> ( ( A e. U /\ B e. V ) /\ ch ) ) )
30 22 23 29 bibiad 
 |-  ( ph -> ( E. x E. y ( <. A , B >. = <. x , y >. /\ ( ( x e. U /\ y e. V ) /\ ps ) ) <-> ( ( A e. U /\ B e. V ) /\ ch ) ) )
31 7 30 bitrd 
 |-  ( ph -> ( A R B <-> ( ( A e. U /\ B e. V ) /\ ch ) ) )