nqpr

Description: The canonical embedding of the rationals into the reals. (Contributed by Mario Carneiro, 12-Jun-2013) (New usage is discouraged.)

		Ref	Expression
	Assertion	nqpr	$⊢ A \in 𝑸 \to \{x \| x <_{𝑸} A\} \in 𝑷$

Proof

Step	Hyp	Ref	Expression
1		nsmallnq	$⊢ A \in 𝑸 \to \exists x x <_{𝑸} A$
2		abn0	$⊢ \{x \| x <_{𝑸} A\} \neq \emptyset \leftrightarrow \exists x x <_{𝑸} A$
3	1 2	sylibr	$⊢ A \in 𝑸 \to \{x \| x <_{𝑸} A\} \neq \emptyset$
4		0pss	$⊢ \emptyset \subset \{x \| x <_{𝑸} A\} \leftrightarrow \{x \| x <_{𝑸} A\} \neq \emptyset$
5	3 4	sylibr	$⊢ A \in 𝑸 \to \emptyset \subset \{x \| x <_{𝑸} A\}$
6		ltrelnq	$⊢ <_{𝑸} \subseteq 𝑸 \times 𝑸$
7	6	brel	$⊢ x <_{𝑸} A \to (x \in 𝑸 \land A \in 𝑸)$
8	7	simpld	$⊢ x <_{𝑸} A \to x \in 𝑸$
9	8	abssi	$⊢ \{x \| x <_{𝑸} A\} \subseteq 𝑸$
10		ltsonq	$⊢ <_{𝑸} Or 𝑸$
11	10 6	soirri	$⊢ \neg A <_{𝑸} A$
12		breq1	$⊢ x = A \to (x <_{𝑸} A \leftrightarrow A <_{𝑸} A)$
13	12	elabg	$⊢ A \in 𝑸 \to (A \in \{x \| x <_{𝑸} A\} \leftrightarrow A <_{𝑸} A)$
14	11 13	mtbiri	$⊢ A \in 𝑸 \to \neg A \in \{x \| x <_{𝑸} A\}$
15	14	ancli	$⊢ A \in 𝑸 \to (A \in 𝑸 \land \neg A \in \{x \| x <_{𝑸} A\})$
16		ssnelpss	$⊢ \{x \| x <_{𝑸} A\} \subseteq 𝑸 \to ((A \in 𝑸 \land \neg A \in \{x \| x <_{𝑸} A\}) \to \{x \| x <_{𝑸} A\} \subset 𝑸)$
17	9 15 16	mpsyl	$⊢ A \in 𝑸 \to \{x \| x <_{𝑸} A\} \subset 𝑸$
18		vex	$⊢ y \in V$
19		breq1	$⊢ x = y \to (x <_{𝑸} A \leftrightarrow y <_{𝑸} A)$
20	18 19	elab	$⊢ y \in \{x \| x <_{𝑸} A\} \leftrightarrow y <_{𝑸} A$
21	10 6	sotri	$⊢ (z <_{𝑸} y \land y <_{𝑸} A) \to z <_{𝑸} A$
22	21	expcom	$⊢ y <_{𝑸} A \to (z <_{𝑸} y \to z <_{𝑸} A)$
23	22	adantl	$⊢ (A \in 𝑸 \land y <_{𝑸} A) \to (z <_{𝑸} y \to z <_{𝑸} A)$
24		vex	$⊢ z \in V$
25		breq1	$⊢ x = z \to (x <_{𝑸} A \leftrightarrow z <_{𝑸} A)$
26	24 25	elab	$⊢ z \in \{x \| x <_{𝑸} A\} \leftrightarrow z <_{𝑸} A$
27	23 26	imbitrrdi	$⊢ (A \in 𝑸 \land y <_{𝑸} A) \to (z <_{𝑸} y \to z \in \{x \| x <_{𝑸} A\})$
28	27	alrimiv	$⊢ (A \in 𝑸 \land y <_{𝑸} A) \to \forall z (z <_{𝑸} y \to z \in \{x \| x <_{𝑸} A\})$
29		ltbtwnnq	$⊢ y <_{𝑸} A \leftrightarrow \exists z (y <_{𝑸} z \land z <_{𝑸} A)$
30	26	anbi2i	$⊢ (y <_{𝑸} z \land z \in \{x \| x <_{𝑸} A\}) \leftrightarrow (y <_{𝑸} z \land z <_{𝑸} A)$
31	30	biimpri	$⊢ (y <_{𝑸} z \land z <_{𝑸} A) \to (y <_{𝑸} z \land z \in \{x \| x <_{𝑸} A\})$
32	31	ancomd	$⊢ (y <_{𝑸} z \land z <_{𝑸} A) \to (z \in \{x \| x <_{𝑸} A\} \land y <_{𝑸} z)$
33	32	eximi	$⊢ \exists z (y <_{𝑸} z \land z <_{𝑸} A) \to \exists z (z \in \{x \| x <_{𝑸} A\} \land y <_{𝑸} z)$
34	29 33	sylbi	$⊢ y <_{𝑸} A \to \exists z (z \in \{x \| x <_{𝑸} A\} \land y <_{𝑸} z)$
35	34	adantl	$⊢ (A \in 𝑸 \land y <_{𝑸} A) \to \exists z (z \in \{x \| x <_{𝑸} A\} \land y <_{𝑸} z)$
36		df-rex	$⊢ \exists z \in \{x \| x <_{𝑸} A\} y <_{𝑸} z \leftrightarrow \exists z (z \in \{x \| x <_{𝑸} A\} \land y <_{𝑸} z)$
37	35 36	sylibr	$⊢ (A \in 𝑸 \land y <_{𝑸} A) \to \exists z \in \{x \| x <_{𝑸} A\} y <_{𝑸} z$
38	28 37	jca	$⊢ (A \in 𝑸 \land y <_{𝑸} A) \to (\forall z (z <_{𝑸} y \to z \in \{x \| x <_{𝑸} A\}) \land \exists z \in \{x \| x <_{𝑸} A\} y <_{𝑸} z)$
39	20 38	sylan2b	$⊢ (A \in 𝑸 \land y \in \{x \| x <_{𝑸} A\}) \to (\forall z (z <_{𝑸} y \to z \in \{x \| x <_{𝑸} A\}) \land \exists z \in \{x \| x <_{𝑸} A\} y <_{𝑸} z)$
40	39	ralrimiva	$⊢ A \in 𝑸 \to \forall y \in \{x \| x <_{𝑸} A\} (\forall z (z <_{𝑸} y \to z \in \{x \| x <_{𝑸} A\}) \land \exists z \in \{x \| x <_{𝑸} A\} y <_{𝑸} z)$
41		elnp	$⊢ \{x \| x <_{𝑸} A\} \in 𝑷 \leftrightarrow ((\emptyset \subset \{x \| x <_{𝑸} A\} \land \{x \| x <_{𝑸} A\} \subset 𝑸) \land \forall y \in \{x \| x <_{𝑸} A\} (\forall z (z <_{𝑸} y \to z \in \{x \| x <_{𝑸} A\}) \land \exists z \in \{x \| x <_{𝑸} A\} y <_{𝑸} z))$
42	5 17 40 41	syl21anbrc	$⊢ A \in 𝑸 \to \{x \| x <_{𝑸} A\} \in 𝑷$

Metamath Proof Explorer

Theorem nqpr

Proof