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

Metamath Proof Explorer

Theorem qexALT

Description: Alternate proof of qex . (Contributed by NM, 30-Jul-2004) (Revised by Mario Carneiro, 16-Jun-2013) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion qexALT 
|- QQ e. _V

Proof

Step Hyp Ref Expression
1 elq 
 |-  ( x e. QQ <-> E. y e. ZZ E. z e. NN x = ( y / z ) )
2 eqid 
 |-  ( y e. ZZ , z e. NN |-> ( y / z ) ) = ( y e. ZZ , z e. NN |-> ( y / z ) )
3 ovex 
 |-  ( y / z ) e. _V
4 2 3 elrnmpo 
 |-  ( x e. ran ( y e. ZZ , z e. NN |-> ( y / z ) ) <-> E. y e. ZZ E. z e. NN x = ( y / z ) )
5 1 4 bitr4i 
 |-  ( x e. QQ <-> x e. ran ( y e. ZZ , z e. NN |-> ( y / z ) ) )
6 5 eqriv 
 |-  QQ = ran ( y e. ZZ , z e. NN |-> ( y / z ) )
7 zexALT 
 |-  ZZ e. _V
8 nnexALT 
 |-  NN e. _V
9 7 8 mpoex 
 |-  ( y e. ZZ , z e. NN |-> ( y / z ) ) e. _V
10 9 rnex 
 |-  ran ( y e. ZZ , z e. NN |-> ( y / z ) ) e. _V
11 6 10 eqeltri 
 |-  QQ e. _V