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

Metamath Proof Explorer

Theorem relopabi

Description: A class of ordered pairs is a relation. (Contributed by Mario Carneiro, 21-Dec-2013) Remove dependency on ax-sep , ax-nul , ax-pr . (Revised by KP, 25-Oct-2021)

Ref Expression
Hypothesis relopabi.1 
|- A = { <. x , y >. | ph }
Assertion relopabi 
|- Rel A

Proof

Step Hyp Ref Expression
1 relopabi.1 
 |-  A = { <. x , y >. | ph }
2 df-opab 
 |-  { <. x , y >. | ph } = { z | E. x E. y ( z = <. x , y >. /\ ph ) }
3 1 2 eqtri 
 |-  A = { z | E. x E. y ( z = <. x , y >. /\ ph ) }
4 3 eqabri 
 |-  ( z e. A <-> E. x E. y ( z = <. x , y >. /\ ph ) )
5 simpl 
 |-  ( ( z = <. x , y >. /\ ph ) -> z = <. x , y >. )
6 5 2eximi 
 |-  ( E. x E. y ( z = <. x , y >. /\ ph ) -> E. x E. y z = <. x , y >. )
7 4 6 sylbi 
 |-  ( z e. A -> E. x E. y z = <. x , y >. )
8 ax6evr 
 |-  E. u y = u
9 pm3.21 
 |-  ( <. x , y >. = z -> ( y = u -> ( y = u /\ <. x , y >. = z ) ) )
10 9 eximdv 
 |-  ( <. x , y >. = z -> ( E. u y = u -> E. u ( y = u /\ <. x , y >. = z ) ) )
11 8 10 mpi 
 |-  ( <. x , y >. = z -> E. u ( y = u /\ <. x , y >. = z ) )
12 opeq2 
 |-  ( y = u -> <. x , y >. = <. x , u >. )
13 eqtr2 
 |-  ( ( <. x , y >. = <. x , u >. /\ <. x , y >. = z ) -> <. x , u >. = z )
14 13 eqcomd 
 |-  ( ( <. x , y >. = <. x , u >. /\ <. x , y >. = z ) -> z = <. x , u >. )
15 12 14 sylan 
 |-  ( ( y = u /\ <. x , y >. = z ) -> z = <. x , u >. )
16 15 eximi 
 |-  ( E. u ( y = u /\ <. x , y >. = z ) -> E. u z = <. x , u >. )
17 11 16 syl 
 |-  ( <. x , y >. = z -> E. u z = <. x , u >. )
18 17 eqcoms 
 |-  ( z = <. x , y >. -> E. u z = <. x , u >. )
19 18 2eximi 
 |-  ( E. x E. y z = <. x , y >. -> E. x E. y E. u z = <. x , u >. )
20 excomim 
 |-  ( E. x E. y E. u z = <. x , u >. -> E. y E. x E. u z = <. x , u >. )
21 19 20 syl 
 |-  ( E. x E. y z = <. x , y >. -> E. y E. x E. u z = <. x , u >. )
22 vex 
 |-  x e. _V
23 vex 
 |-  u e. _V
24 22 23 pm3.2i 
 |-  ( x e. _V /\ u e. _V )
25 24 jctr 
 |-  ( z = <. x , u >. -> ( z = <. x , u >. /\ ( x e. _V /\ u e. _V ) ) )
26 25 2eximi 
 |-  ( E. x E. u z = <. x , u >. -> E. x E. u ( z = <. x , u >. /\ ( x e. _V /\ u e. _V ) ) )
27 df-xp 
 |-  ( _V X. _V ) = { <. x , u >. | ( x e. _V /\ u e. _V ) }
28 df-opab 
 |-  { <. x , u >. | ( x e. _V /\ u e. _V ) } = { z | E. x E. u ( z = <. x , u >. /\ ( x e. _V /\ u e. _V ) ) }
29 27 28 eqtri 
 |-  ( _V X. _V ) = { z | E. x E. u ( z = <. x , u >. /\ ( x e. _V /\ u e. _V ) ) }
30 29 eqabri 
 |-  ( z e. ( _V X. _V ) <-> E. x E. u ( z = <. x , u >. /\ ( x e. _V /\ u e. _V ) ) )
31 26 30 sylibr 
 |-  ( E. x E. u z = <. x , u >. -> z e. ( _V X. _V ) )
32 31 eximi 
 |-  ( E. y E. x E. u z = <. x , u >. -> E. y z e. ( _V X. _V ) )
33 ax5e 
 |-  ( E. y z e. ( _V X. _V ) -> z e. ( _V X. _V ) )
34 7 21 32 33 4syl 
 |-  ( z e. A -> z e. ( _V X. _V ) )
35 34 ssriv 
 |-  A C_ ( _V X. _V )
36 df-rel 
 |-  ( Rel A <-> A C_ ( _V X. _V ) )
37 35 36 mpbir 
 |-  Rel A