Metamath Proof Explorer

Theorem oprabid

Description: The law of concretion. Special case of Theorem 9.5 of Quine p. 61. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker oprabidw when possible. (Contributed by Mario Carneiro, 20-Mar-2013) (New usage is discouraged.)

Ref Expression
Assertion oprabid 
|- ( <. <. x , y >. , z >. e. { <. <. x , y >. , z >. | ph } <-> ph )

Proof

Step Hyp Ref Expression
1 opex 
 |-  <. <. x , y >. , z >. e. _V
2 opex 
 |-  <. x , y >. e. _V
3 vex 
 |-  z e. _V
4 2 3 eqvinop 
 |-  ( w = <. <. x , y >. , z >. <-> E. a E. t ( w = <. a , t >. /\ <. a , t >. = <. <. x , y >. , z >. ) )
5 4 biimpi 
 |-  ( w = <. <. x , y >. , z >. -> E. a E. t ( w = <. a , t >. /\ <. a , t >. = <. <. x , y >. , z >. ) )
6 eqeq1 
 |-  ( w = <. a , t >. -> ( w = <. <. x , y >. , z >. <-> <. a , t >. = <. <. x , y >. , z >. ) )
7 vex 
 |-  a e. _V
8 vex 
 |-  t e. _V
9 7 8 opth1 
 |-  ( <. a , t >. = <. <. x , y >. , z >. -> a = <. x , y >. )
10 6 9 biimtrdi 
 |-  ( w = <. a , t >. -> ( w = <. <. x , y >. , z >. -> a = <. x , y >. ) )
11 vex 
 |-  x e. _V
12 vex 
 |-  y e. _V
13 11 12 eqvinop 
 |-  ( a = <. x , y >. <-> E. r E. s ( a = <. r , s >. /\ <. r , s >. = <. x , y >. ) )
14 opeq1 
 |-  ( a = <. r , s >. -> <. a , t >. = <. <. r , s >. , t >. )
15 14 eqeq2d 
 |-  ( a = <. r , s >. -> ( w = <. a , t >. <-> w = <. <. r , s >. , t >. ) )
16 11 12 3 otth2 
 |-  ( <. <. x , y >. , z >. = <. <. r , s >. , t >. <-> ( x = r /\ y = s /\ z = t ) )
17 euequ 
 |-  E! x x = r
18 eupick 
 |-  ( ( E! x x = r /\ E. x ( x = r /\ E. y ( y = s /\ E. z ( z = t /\ ph ) ) ) ) -> ( x = r -> E. y ( y = s /\ E. z ( z = t /\ ph ) ) ) )
19 17 18 mpan 
 |-  ( E. x ( x = r /\ E. y ( y = s /\ E. z ( z = t /\ ph ) ) ) -> ( x = r -> E. y ( y = s /\ E. z ( z = t /\ ph ) ) ) )
20 euequ 
 |-  E! y y = s
21 eupick 
 |-  ( ( E! y y = s /\ E. y ( y = s /\ E. z ( z = t /\ ph ) ) ) -> ( y = s -> E. z ( z = t /\ ph ) ) )
22 20 21 mpan 
 |-  ( E. y ( y = s /\ E. z ( z = t /\ ph ) ) -> ( y = s -> E. z ( z = t /\ ph ) ) )
23 euequ 
 |-  E! z z = t
24 eupick 
 |-  ( ( E! z z = t /\ E. z ( z = t /\ ph ) ) -> ( z = t -> ph ) )
25 23 24 mpan 
 |-  ( E. z ( z = t /\ ph ) -> ( z = t -> ph ) )
26 22 25 syl6 
 |-  ( E. y ( y = s /\ E. z ( z = t /\ ph ) ) -> ( y = s -> ( z = t -> ph ) ) )
27 19 26 syl6 
 |-  ( E. x ( x = r /\ E. y ( y = s /\ E. z ( z = t /\ ph ) ) ) -> ( x = r -> ( y = s -> ( z = t -> ph ) ) ) )
28 27 3impd 
 |-  ( E. x ( x = r /\ E. y ( y = s /\ E. z ( z = t /\ ph ) ) ) -> ( ( x = r /\ y = s /\ z = t ) -> ph ) )
29 16 28 biimtrid 
 |-  ( E. x ( x = r /\ E. y ( y = s /\ E. z ( z = t /\ ph ) ) ) -> ( <. <. x , y >. , z >. = <. <. r , s >. , t >. -> ph ) )
30 df-3an 
 |-  ( ( x = r /\ y = s /\ z = t ) <-> ( ( x = r /\ y = s ) /\ z = t ) )
31 16 30 bitri 
 |-  ( <. <. x , y >. , z >. = <. <. r , s >. , t >. <-> ( ( x = r /\ y = s ) /\ z = t ) )
32 31 anbi1i 
 |-  ( ( <. <. x , y >. , z >. = <. <. r , s >. , t >. /\ ph ) <-> ( ( ( x = r /\ y = s ) /\ z = t ) /\ ph ) )
33 anass 
 |-  ( ( ( ( x = r /\ y = s ) /\ z = t ) /\ ph ) <-> ( ( x = r /\ y = s ) /\ ( z = t /\ ph ) ) )
34 anass 
 |-  ( ( ( x = r /\ y = s ) /\ ( z = t /\ ph ) ) <-> ( x = r /\ ( y = s /\ ( z = t /\ ph ) ) ) )
35 32 33 34 3bitri 
 |-  ( ( <. <. x , y >. , z >. = <. <. r , s >. , t >. /\ ph ) <-> ( x = r /\ ( y = s /\ ( z = t /\ ph ) ) ) )
36 35 3exbii 
 |-  ( E. x E. y E. z ( <. <. x , y >. , z >. = <. <. r , s >. , t >. /\ ph ) <-> E. x E. y E. z ( x = r /\ ( y = s /\ ( z = t /\ ph ) ) ) )
37 nfcvf2 
 |-  ( -. A. x x = z -> F/_ z x )
38 nfcvd 
 |-  ( -. A. x x = z -> F/_ z r )
39 37 38 nfeqd 
 |-  ( -. A. x x = z -> F/ z x = r )
40 39 exdistrf 
 |-  ( E. x E. z ( x = r /\ ( y = s /\ ( z = t /\ ph ) ) ) -> E. x ( x = r /\ E. z ( y = s /\ ( z = t /\ ph ) ) ) )
41 40 eximi 
 |-  ( E. y E. x E. z ( x = r /\ ( y = s /\ ( z = t /\ ph ) ) ) -> E. y E. x ( x = r /\ E. z ( y = s /\ ( z = t /\ ph ) ) ) )
42 excom 
 |-  ( E. x E. y E. z ( x = r /\ ( y = s /\ ( z = t /\ ph ) ) ) <-> E. y E. x E. z ( x = r /\ ( y = s /\ ( z = t /\ ph ) ) ) )
43 excom 
 |-  ( E. x E. y ( x = r /\ E. z ( y = s /\ ( z = t /\ ph ) ) ) <-> E. y E. x ( x = r /\ E. z ( y = s /\ ( z = t /\ ph ) ) ) )
44 41 42 43 3imtr4i 
 |-  ( E. x E. y E. z ( x = r /\ ( y = s /\ ( z = t /\ ph ) ) ) -> E. x E. y ( x = r /\ E. z ( y = s /\ ( z = t /\ ph ) ) ) )
45 nfcvf2 
 |-  ( -. A. x x = y -> F/_ y x )
46 nfcvd 
 |-  ( -. A. x x = y -> F/_ y r )
47 45 46 nfeqd 
 |-  ( -. A. x x = y -> F/ y x = r )
48 47 exdistrf 
 |-  ( E. x E. y ( x = r /\ E. z ( y = s /\ ( z = t /\ ph ) ) ) -> E. x ( x = r /\ E. y E. z ( y = s /\ ( z = t /\ ph ) ) ) )
49 nfcvf2 
 |-  ( -. A. y y = z -> F/_ z y )
50 nfcvd 
 |-  ( -. A. y y = z -> F/_ z s )
51 49 50 nfeqd 
 |-  ( -. A. y y = z -> F/ z y = s )
52 51 exdistrf 
 |-  ( E. y E. z ( y = s /\ ( z = t /\ ph ) ) -> E. y ( y = s /\ E. z ( z = t /\ ph ) ) )
53 52 anim2i 
 |-  ( ( x = r /\ E. y E. z ( y = s /\ ( z = t /\ ph ) ) ) -> ( x = r /\ E. y ( y = s /\ E. z ( z = t /\ ph ) ) ) )
54 53 eximi 
 |-  ( E. x ( x = r /\ E. y E. z ( y = s /\ ( z = t /\ ph ) ) ) -> E. x ( x = r /\ E. y ( y = s /\ E. z ( z = t /\ ph ) ) ) )
55 44 48 54 3syl 
 |-  ( E. x E. y E. z ( x = r /\ ( y = s /\ ( z = t /\ ph ) ) ) -> E. x ( x = r /\ E. y ( y = s /\ E. z ( z = t /\ ph ) ) ) )
56 36 55 sylbi 
 |-  ( E. x E. y E. z ( <. <. x , y >. , z >. = <. <. r , s >. , t >. /\ ph ) -> E. x ( x = r /\ E. y ( y = s /\ E. z ( z = t /\ ph ) ) ) )
57 29 56 syl11 
 |-  ( <. <. x , y >. , z >. = <. <. r , s >. , t >. -> ( E. x E. y E. z ( <. <. x , y >. , z >. = <. <. r , s >. , t >. /\ ph ) -> ph ) )
58 eqeq1 
 |-  ( w = <. <. r , s >. , t >. -> ( w = <. <. x , y >. , z >. <-> <. <. r , s >. , t >. = <. <. x , y >. , z >. ) )
59 eqcom 
 |-  ( <. <. r , s >. , t >. = <. <. x , y >. , z >. <-> <. <. x , y >. , z >. = <. <. r , s >. , t >. )
60 58 59 bitrdi 
 |-  ( w = <. <. r , s >. , t >. -> ( w = <. <. x , y >. , z >. <-> <. <. x , y >. , z >. = <. <. r , s >. , t >. ) )
61 60 anbi1d 
 |-  ( w = <. <. r , s >. , t >. -> ( ( w = <. <. x , y >. , z >. /\ ph ) <-> ( <. <. x , y >. , z >. = <. <. r , s >. , t >. /\ ph ) ) )
62 61 3exbidv 
 |-  ( w = <. <. r , s >. , t >. -> ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) <-> E. x E. y E. z ( <. <. x , y >. , z >. = <. <. r , s >. , t >. /\ ph ) ) )
63 62 imbi1d 
 |-  ( w = <. <. r , s >. , t >. -> ( ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) -> ph ) <-> ( E. x E. y E. z ( <. <. x , y >. , z >. = <. <. r , s >. , t >. /\ ph ) -> ph ) ) )
64 60 63 imbi12d 
 |-  ( w = <. <. r , s >. , t >. -> ( ( w = <. <. x , y >. , z >. -> ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) -> ph ) ) <-> ( <. <. x , y >. , z >. = <. <. r , s >. , t >. -> ( E. x E. y E. z ( <. <. x , y >. , z >. = <. <. r , s >. , t >. /\ ph ) -> ph ) ) ) )
65 57 64 mpbiri 
 |-  ( w = <. <. r , s >. , t >. -> ( w = <. <. x , y >. , z >. -> ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) -> ph ) ) )
66 15 65 biimtrdi 
 |-  ( a = <. r , s >. -> ( w = <. a , t >. -> ( w = <. <. x , y >. , z >. -> ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) -> ph ) ) ) )
67 66 adantr 
 |-  ( ( a = <. r , s >. /\ <. r , s >. = <. x , y >. ) -> ( w = <. a , t >. -> ( w = <. <. x , y >. , z >. -> ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) -> ph ) ) ) )
68 67 exlimivv 
 |-  ( E. r E. s ( a = <. r , s >. /\ <. r , s >. = <. x , y >. ) -> ( w = <. a , t >. -> ( w = <. <. x , y >. , z >. -> ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) -> ph ) ) ) )
69 13 68 sylbi 
 |-  ( a = <. x , y >. -> ( w = <. a , t >. -> ( w = <. <. x , y >. , z >. -> ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) -> ph ) ) ) )
70 69 com3l 
 |-  ( w = <. a , t >. -> ( w = <. <. x , y >. , z >. -> ( a = <. x , y >. -> ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) -> ph ) ) ) )
71 10 70 mpdd 
 |-  ( w = <. a , t >. -> ( w = <. <. x , y >. , z >. -> ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) -> ph ) ) )
72 71 adantr 
 |-  ( ( w = <. a , t >. /\ <. a , t >. = <. <. x , y >. , z >. ) -> ( w = <. <. x , y >. , z >. -> ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) -> ph ) ) )
73 72 exlimivv 
 |-  ( E. a E. t ( w = <. a , t >. /\ <. a , t >. = <. <. x , y >. , z >. ) -> ( w = <. <. x , y >. , z >. -> ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) -> ph ) ) )
74 5 73 mpcom 
 |-  ( w = <. <. x , y >. , z >. -> ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) -> ph ) )
75 19.8a 
 |-  ( ( w = <. <. x , y >. , z >. /\ ph ) -> E. z ( w = <. <. x , y >. , z >. /\ ph ) )
76 19.8a 
 |-  ( E. z ( w = <. <. x , y >. , z >. /\ ph ) -> E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) )
77 19.8a 
 |-  ( E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) -> E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) )
78 75 76 77 3syl 
 |-  ( ( w = <. <. x , y >. , z >. /\ ph ) -> E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) )
79 78 ex 
 |-  ( w = <. <. x , y >. , z >. -> ( ph -> E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) ) )
80 74 79 impbid 
 |-  ( w = <. <. x , y >. , z >. -> ( E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) <-> ph ) )
81 df-oprab 
 |-  { <. <. x , y >. , z >. | ph } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ph ) }
82 1 80 81 elab2 
 |-  ( <. <. x , y >. , z >. e. { <. <. x , y >. , z >. | ph } <-> ph )