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 ℚ ∈ V

Proof

Step Hyp Ref Expression
1 elq ⊢ ( 𝑥 ∈ ℚ ↔ ∃ 𝑦 ∈ ℤ ∃ 𝑧 ∈ ℕ 𝑥 = ( 𝑦 / 𝑧 ) )
2 eqid ⊢ ( 𝑦 ∈ ℤ , 𝑧 ∈ ℕ ↦ ( 𝑦 / 𝑧 ) ) = ( 𝑦 ∈ ℤ , 𝑧 ∈ ℕ ↦ ( 𝑦 / 𝑧 ) )
3 ovex ⊢ ( 𝑦 / 𝑧 ) ∈ V
4 2 3 elrnmpo ⊢ ( 𝑥 ∈ ran ( 𝑦 ∈ ℤ , 𝑧 ∈ ℕ ↦ ( 𝑦 / 𝑧 ) ) ↔ ∃ 𝑦 ∈ ℤ ∃ 𝑧 ∈ ℕ 𝑥 = ( 𝑦 / 𝑧 ) )
5 1 4 bitr4i ⊢ ( 𝑥 ∈ ℚ ↔ 𝑥 ∈ ran ( 𝑦 ∈ ℤ , 𝑧 ∈ ℕ ↦ ( 𝑦 / 𝑧 ) ) )
6 5 eqriv ⊢ ℚ = ran ( 𝑦 ∈ ℤ , 𝑧 ∈ ℕ ↦ ( 𝑦 / 𝑧 ) )
7 zexALT ⊢ ℤ ∈ V
8 nnexALT ⊢ ℕ ∈ V
9 7 8 mpoex ⊢ ( 𝑦 ∈ ℤ , 𝑧 ∈ ℕ ↦ ( 𝑦 / 𝑧 ) ) ∈ V
10 9 rnex ⊢ ran ( 𝑦 ∈ ℤ , 𝑧 ∈ ℕ ↦ ( 𝑦 / 𝑧 ) ) ∈ V
11 6 10 eqeltri ⊢ ℚ ∈ V