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	$⊢ ℚ \in V$

Proof

Step	Hyp	Ref	Expression
1		elq	$⊢ x \in ℚ \leftrightarrow \exists y \in ℤ \exists z \in ℕ x = \frac{y}{z}$
2		eqid	$⊢ (y \in ℤ, z \in ℕ ⟼ \frac{y}{z}) = (y \in ℤ, z \in ℕ ⟼ \frac{y}{z})$
3		ovex	$⊢ \frac{y}{z} \in V$
4	2 3	elrnmpo	$⊢ x \in ran (y \in ℤ, z \in ℕ ⟼ \frac{y}{z}) \leftrightarrow \exists y \in ℤ \exists z \in ℕ x = \frac{y}{z}$
5	1 4	bitr4i	$⊢ x \in ℚ \leftrightarrow x \in ran (y \in ℤ, z \in ℕ ⟼ \frac{y}{z})$
6	5	eqriv	$⊢ ℚ = ran (y \in ℤ, z \in ℕ ⟼ \frac{y}{z})$
7		zexALT	$⊢ ℤ \in V$
8		nnexALT	$⊢ ℕ \in V$
9	7 8	mpoex	$⊢ (y \in ℤ, z \in ℕ ⟼ \frac{y}{z}) \in V$
10	9	rnex	$⊢ ran (y \in ℤ, z \in ℕ ⟼ \frac{y}{z}) \in V$
11	6 10	eqeltri	$⊢ ℚ \in V$