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