Metamath Proof Explorer

Theorem dfdm5

Description: Definition of domain in terms of 1st and image. (Contributed by Scott Fenton, 11-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014) (Proof shortened by Peter Mazsa, 2-Oct-2022)

Ref Expression
Assertion dfdm5 
|- dom A = ( ( 1st |` ( _V X. _V ) ) " A )

Proof

Step Hyp Ref Expression
1 excom 
 |-  ( E. y E. p E. z ( p = <. z , y >. /\ ( p 1st x /\ p e. A ) ) <-> E. p E. y E. z ( p = <. z , y >. /\ ( p 1st x /\ p e. A ) ) )
2 opex 
 |-  <. z , y >. e. _V
3 breq1 
 |-  ( p = <. z , y >. -> ( p 1st x <-> <. z , y >. 1st x ) )
4 eleq1 
 |-  ( p = <. z , y >. -> ( p e. A <-> <. z , y >. e. A ) )
5 3 4 anbi12d 
 |-  ( p = <. z , y >. -> ( ( p 1st x /\ p e. A ) <-> ( <. z , y >. 1st x /\ <. z , y >. e. A ) ) )
6 vex 
 |-  z e. _V
7 vex 
 |-  y e. _V
8 6 7 br1steq 
 |-  ( <. z , y >. 1st x <-> x = z )
9 equcom 
 |-  ( x = z <-> z = x )
10 8 9 bitri 
 |-  ( <. z , y >. 1st x <-> z = x )
11 10 anbi1i 
 |-  ( ( <. z , y >. 1st x /\ <. z , y >. e. A ) <-> ( z = x /\ <. z , y >. e. A ) )
12 5 11 bitrdi 
 |-  ( p = <. z , y >. -> ( ( p 1st x /\ p e. A ) <-> ( z = x /\ <. z , y >. e. A ) ) )
13 2 12 ceqsexv 
 |-  ( E. p ( p = <. z , y >. /\ ( p 1st x /\ p e. A ) ) <-> ( z = x /\ <. z , y >. e. A ) )
14 13 exbii 
 |-  ( E. z E. p ( p = <. z , y >. /\ ( p 1st x /\ p e. A ) ) <-> E. z ( z = x /\ <. z , y >. e. A ) )
15 excom 
 |-  ( E. z E. p ( p = <. z , y >. /\ ( p 1st x /\ p e. A ) ) <-> E. p E. z ( p = <. z , y >. /\ ( p 1st x /\ p e. A ) ) )
16 vex 
 |-  x e. _V
17 opeq1 
 |-  ( z = x -> <. z , y >. = <. x , y >. )
18 17 eleq1d 
 |-  ( z = x -> ( <. z , y >. e. A <-> <. x , y >. e. A ) )
19 16 18 ceqsexv 
 |-  ( E. z ( z = x /\ <. z , y >. e. A ) <-> <. x , y >. e. A )
20 14 15 19 3bitr3ri 
 |-  ( <. x , y >. e. A <-> E. p E. z ( p = <. z , y >. /\ ( p 1st x /\ p e. A ) ) )
21 20 exbii 
 |-  ( E. y <. x , y >. e. A <-> E. y E. p E. z ( p = <. z , y >. /\ ( p 1st x /\ p e. A ) ) )
22 ancom 
 |-  ( ( p e. A /\ p ( 1st |` ( _V X. _V ) ) x ) <-> ( p ( 1st |` ( _V X. _V ) ) x /\ p e. A ) )
23 anass 
 |-  ( ( ( E. y E. z p = <. z , y >. /\ p 1st x ) /\ p e. A ) <-> ( E. y E. z p = <. z , y >. /\ ( p 1st x /\ p e. A ) ) )
24 16 brresi 
 |-  ( p ( 1st |` ( _V X. _V ) ) x <-> ( p e. ( _V X. _V ) /\ p 1st x ) )
25 elvv 
 |-  ( p e. ( _V X. _V ) <-> E. z E. y p = <. z , y >. )
26 excom 
 |-  ( E. z E. y p = <. z , y >. <-> E. y E. z p = <. z , y >. )
27 25 26 bitri 
 |-  ( p e. ( _V X. _V ) <-> E. y E. z p = <. z , y >. )
28 27 anbi1i 
 |-  ( ( p e. ( _V X. _V ) /\ p 1st x ) <-> ( E. y E. z p = <. z , y >. /\ p 1st x ) )
29 24 28 bitri 
 |-  ( p ( 1st |` ( _V X. _V ) ) x <-> ( E. y E. z p = <. z , y >. /\ p 1st x ) )
30 29 anbi1i 
 |-  ( ( p ( 1st |` ( _V X. _V ) ) x /\ p e. A ) <-> ( ( E. y E. z p = <. z , y >. /\ p 1st x ) /\ p e. A ) )
31 19.41vv 
 |-  ( E. y E. z ( p = <. z , y >. /\ ( p 1st x /\ p e. A ) ) <-> ( E. y E. z p = <. z , y >. /\ ( p 1st x /\ p e. A ) ) )
32 23 30 31 3bitr4i 
 |-  ( ( p ( 1st |` ( _V X. _V ) ) x /\ p e. A ) <-> E. y E. z ( p = <. z , y >. /\ ( p 1st x /\ p e. A ) ) )
33 22 32 bitri 
 |-  ( ( p e. A /\ p ( 1st |` ( _V X. _V ) ) x ) <-> E. y E. z ( p = <. z , y >. /\ ( p 1st x /\ p e. A ) ) )
34 33 exbii 
 |-  ( E. p ( p e. A /\ p ( 1st |` ( _V X. _V ) ) x ) <-> E. p E. y E. z ( p = <. z , y >. /\ ( p 1st x /\ p e. A ) ) )
35 1 21 34 3bitr4i 
 |-  ( E. y <. x , y >. e. A <-> E. p ( p e. A /\ p ( 1st |` ( _V X. _V ) ) x ) )
36 16 eldm2 
 |-  ( x e. dom A <-> E. y <. x , y >. e. A )
37 16 elima2 
 |-  ( x e. ( ( 1st |` ( _V X. _V ) ) " A ) <-> E. p ( p e. A /\ p ( 1st |` ( _V X. _V ) ) x ) )
38 35 36 37 3bitr4i 
 |-  ( x e. dom A <-> x e. ( ( 1st |` ( _V X. _V ) ) " A ) )
39 38 eqriv 
 |-  dom A = ( ( 1st |` ( _V X. _V ) ) " A )