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