Metamath Proof Explorer

Theorem oprabv

Description: If a pair and a class are in a relationship given by a class abstraction of a collection of nested ordered pairs, the involved classes are sets. (Contributed by Alexander van der Vekens, 8-Jul-2018)

Ref Expression
Assertion oprabv 
|- ( <. X , Y >. { <. <. x , y >. , z >. | ph } Z -> ( X e. _V /\ Y e. _V /\ Z e. _V ) )

Proof

Step Hyp Ref Expression
1 reloprab 
 |-  Rel { <. <. x , y >. , z >. | ph }
2 1 brrelex12i 
 |-  ( <. X , Y >. { <. <. x , y >. , z >. | ph } Z -> ( <. X , Y >. e. _V /\ Z e. _V ) )
3 df-br 
 |-  ( <. X , Y >. { <. <. x , y >. , z >. | ph } Z <-> <. <. X , Y >. , Z >. e. { <. <. x , y >. , z >. | ph } )
4 opex 
 |-  <. X , Y >. e. _V
5 nfcv 
 |-  F/_ w <. X , Y >.
6 5 nfeq1 
 |-  F/ w <. X , Y >. = <. x , y >.
7 nfv 
 |-  F/ w ph
8 6 7 nfan 
 |-  F/ w ( <. X , Y >. = <. x , y >. /\ ph )
9 8 nfex 
 |-  F/ w E. y ( <. X , Y >. = <. x , y >. /\ ph )
10 9 nfex 
 |-  F/ w E. x E. y ( <. X , Y >. = <. x , y >. /\ ph )
11 nfcv 
 |-  F/_ z <. X , Y >.
12 11 nfeq1 
 |-  F/ z <. X , Y >. = <. x , y >.
13 nfsbc1v 
 |-  F/ z [. Z / z ]. ph
14 12 13 nfan 
 |-  F/ z ( <. X , Y >. = <. x , y >. /\ [. Z / z ]. ph )
15 14 nfex 
 |-  F/ z E. y ( <. X , Y >. = <. x , y >. /\ [. Z / z ]. ph )
16 15 nfex 
 |-  F/ z E. x E. y ( <. X , Y >. = <. x , y >. /\ [. Z / z ]. ph )
17 eqeq1 
 |-  ( w = <. X , Y >. -> ( w = <. x , y >. <-> <. X , Y >. = <. x , y >. ) )
18 17 anbi1d 
 |-  ( w = <. X , Y >. -> ( ( w = <. x , y >. /\ ph ) <-> ( <. X , Y >. = <. x , y >. /\ ph ) ) )
19 18 2exbidv 
 |-  ( w = <. X , Y >. -> ( E. x E. y ( w = <. x , y >. /\ ph ) <-> E. x E. y ( <. X , Y >. = <. x , y >. /\ ph ) ) )
20 sbceq1a 
 |-  ( z = Z -> ( ph <-> [. Z / z ]. ph ) )
21 20 anbi2d 
 |-  ( z = Z -> ( ( <. X , Y >. = <. x , y >. /\ ph ) <-> ( <. X , Y >. = <. x , y >. /\ [. Z / z ]. ph ) ) )
22 21 2exbidv 
 |-  ( z = Z -> ( E. x E. y ( <. X , Y >. = <. x , y >. /\ ph ) <-> E. x E. y ( <. X , Y >. = <. x , y >. /\ [. Z / z ]. ph ) ) )
23 10 16 19 22 opelopabgf 
 |-  ( ( <. X , Y >. e. _V /\ Z e. _V ) -> ( <. <. X , Y >. , Z >. e. { <. w , z >. | E. x E. y ( w = <. x , y >. /\ ph ) } <-> E. x E. y ( <. X , Y >. = <. x , y >. /\ [. Z / z ]. ph ) ) )
24 4 23 mpan 
 |-  ( Z e. _V -> ( <. <. X , Y >. , Z >. e. { <. w , z >. | E. x E. y ( w = <. x , y >. /\ ph ) } <-> E. x E. y ( <. X , Y >. = <. x , y >. /\ [. Z / z ]. ph ) ) )
25 eqcom 
 |-  ( <. X , Y >. = <. x , y >. <-> <. x , y >. = <. X , Y >. )
26 vex 
 |-  x e. _V
27 vex 
 |-  y e. _V
28 26 27 opth 
 |-  ( <. x , y >. = <. X , Y >. <-> ( x = X /\ y = Y ) )
29 25 28 bitri 
 |-  ( <. X , Y >. = <. x , y >. <-> ( x = X /\ y = Y ) )
30 eqvisset 
 |-  ( x = X -> X e. _V )
31 eqvisset 
 |-  ( y = Y -> Y e. _V )
32 30 31 anim12i 
 |-  ( ( x = X /\ y = Y ) -> ( X e. _V /\ Y e. _V ) )
33 29 32 sylbi 
 |-  ( <. X , Y >. = <. x , y >. -> ( X e. _V /\ Y e. _V ) )
34 33 adantr 
 |-  ( ( <. X , Y >. = <. x , y >. /\ [. Z / z ]. ph ) -> ( X e. _V /\ Y e. _V ) )
35 34 exlimivv 
 |-  ( E. x E. y ( <. X , Y >. = <. x , y >. /\ [. Z / z ]. ph ) -> ( X e. _V /\ Y e. _V ) )
36 35 anim1i 
 |-  ( ( E. x E. y ( <. X , Y >. = <. x , y >. /\ [. Z / z ]. ph ) /\ Z e. _V ) -> ( ( X e. _V /\ Y e. _V ) /\ Z e. _V ) )
37 df-3an 
 |-  ( ( X e. _V /\ Y e. _V /\ Z e. _V ) <-> ( ( X e. _V /\ Y e. _V ) /\ Z e. _V ) )
38 36 37 sylibr 
 |-  ( ( E. x E. y ( <. X , Y >. = <. x , y >. /\ [. Z / z ]. ph ) /\ Z e. _V ) -> ( X e. _V /\ Y e. _V /\ Z e. _V ) )
39 38 expcom 
 |-  ( Z e. _V -> ( E. x E. y ( <. X , Y >. = <. x , y >. /\ [. Z / z ]. ph ) -> ( X e. _V /\ Y e. _V /\ Z e. _V ) ) )
40 24 39 sylbid 
 |-  ( Z e. _V -> ( <. <. X , Y >. , Z >. e. { <. w , z >. | E. x E. y ( w = <. x , y >. /\ ph ) } -> ( X e. _V /\ Y e. _V /\ Z e. _V ) ) )
41 40 com12 
 |-  ( <. <. X , Y >. , Z >. e. { <. w , z >. | E. x E. y ( w = <. x , y >. /\ ph ) } -> ( Z e. _V -> ( X e. _V /\ Y e. _V /\ Z e. _V ) ) )
42 dfoprab2 
 |-  { <. <. x , y >. , z >. | ph } = { <. w , z >. | E. x E. y ( w = <. x , y >. /\ ph ) }
43 41 42 eleq2s 
 |-  ( <. <. X , Y >. , Z >. e. { <. <. x , y >. , z >. | ph } -> ( Z e. _V -> ( X e. _V /\ Y e. _V /\ Z e. _V ) ) )
44 3 43 sylbi 
 |-  ( <. X , Y >. { <. <. x , y >. , z >. | ph } Z -> ( Z e. _V -> ( X e. _V /\ Y e. _V /\ Z e. _V ) ) )
45 44 com12 
 |-  ( Z e. _V -> ( <. X , Y >. { <. <. x , y >. , z >. | ph } Z -> ( X e. _V /\ Y e. _V /\ Z e. _V ) ) )
46 45 adantl 
 |-  ( ( <. X , Y >. e. _V /\ Z e. _V ) -> ( <. X , Y >. { <. <. x , y >. , z >. | ph } Z -> ( X e. _V /\ Y e. _V /\ Z e. _V ) ) )
47 2 46 mpcom 
 |-  ( <. X , Y >. { <. <. x , y >. , z >. | ph } Z -> ( X e. _V /\ Y e. _V /\ Z e. _V ) )