This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dfrn5

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

Ref Expression
Assertion dfrn5 
|- ran A = ( ( 2nd |` ( _V X. _V ) ) " A )

Proof

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