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