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 ⊢ x ∈ ℚ ↔ ∃ y ∈ ℤ ∃ z ∈ ℕ x = y z
2 eqid ⊢ y ∈ ℤ , z ∈ ℕ ⟼ y z = y ∈ ℤ , z ∈ ℕ ⟼ y z
3 ovex ⊢ y z ∈ V
4 2 3 elrnmpo ⊢ x ∈ ran ⁡ y ∈ ℤ , z ∈ ℕ ⟼ y z ↔ ∃ y ∈ ℤ ∃ z ∈ ℕ x = y z
5 1 4 bitr4i ⊢ x ∈ ℚ ↔ x ∈ ran ⁡ y ∈ ℤ , z ∈ ℕ ⟼ y z
6 5 eqriv ⊢ ℚ = ran ⁡ y ∈ ℤ , z ∈ ℕ ⟼ y z
7 zexALT ⊢ ℤ ∈ V
8 nnexALT ⊢ ℕ ∈ V
9 7 8 mpoex ⊢ y ∈ ℤ , z ∈ ℕ ⟼ y z ∈ V
10 9 rnex ⊢ ran ⁡ y ∈ ℤ , z ∈ ℕ ⟼ y z ∈ V
11 6 10 eqeltri ⊢ ℚ ∈ V