prcdnq

Description: A positive real is closed downwards under the positive fractions. Definition 9-3.1 (ii) of Gleason p. 121. (Contributed by NM, 25-Feb-1996) (Revised by Mario Carneiro, 11-May-2013) (New usage is discouraged.)

		Ref	Expression
	Assertion	prcdnq	$⊢ (A \in 𝑷 \land B \in A) \to (C <_{𝑸} B \to C \in A)$

Proof

Step	Hyp	Ref	Expression
1		ltrelnq	$⊢ <_{𝑸} \subseteq 𝑸 \times 𝑸$
2		relxp	$⊢ Rel (𝑸 \times 𝑸)$
3		relss	$⊢ <_{𝑸} \subseteq 𝑸 \times 𝑸 \to (Rel (𝑸 \times 𝑸) \to Rel <_{𝑸})$
4	1 2 3	mp2	$⊢ Rel <_{𝑸}$
5	4	brrelex1i	$⊢ C <_{𝑸} B \to C \in V$
6		eleq1	$⊢ x = B \to (x \in A \leftrightarrow B \in A)$
7	6	anbi2d	$⊢ x = B \to ((A \in 𝑷 \land x \in A) \leftrightarrow (A \in 𝑷 \land B \in A))$
8		breq2	$⊢ x = B \to (y <_{𝑸} x \leftrightarrow y <_{𝑸} B)$
9	7 8	anbi12d	$⊢ x = B \to (((A \in 𝑷 \land x \in A) \land y <_{𝑸} x) \leftrightarrow ((A \in 𝑷 \land B \in A) \land y <_{𝑸} B))$
10	9	imbi1d	$⊢ x = B \to ((((A \in 𝑷 \land x \in A) \land y <_{𝑸} x) \to y \in A) \leftrightarrow (((A \in 𝑷 \land B \in A) \land y <_{𝑸} B) \to y \in A))$
11		breq1	$⊢ y = C \to (y <_{𝑸} B \leftrightarrow C <_{𝑸} B)$
12	11	anbi2d	$⊢ y = C \to (((A \in 𝑷 \land B \in A) \land y <_{𝑸} B) \leftrightarrow ((A \in 𝑷 \land B \in A) \land C <_{𝑸} B))$
13		eleq1	$⊢ y = C \to (y \in A \leftrightarrow C \in A)$
14	12 13	imbi12d	$⊢ y = C \to ((((A \in 𝑷 \land B \in A) \land y <_{𝑸} B) \to y \in A) \leftrightarrow (((A \in 𝑷 \land B \in A) \land C <_{𝑸} B) \to C \in A))$
15		elnpi	$⊢ A \in 𝑷 \leftrightarrow ((A \in V \land \emptyset \subset A \land A \subset 𝑸) \land \forall x \in A (\forall y (y <_{𝑸} x \to y \in A) \land \exists y \in A x <_{𝑸} y))$
16	15	simprbi	$⊢ A \in 𝑷 \to \forall x \in A (\forall y (y <_{𝑸} x \to y \in A) \land \exists y \in A x <_{𝑸} y)$
17	16	r19.21bi	$⊢ (A \in 𝑷 \land x \in A) \to (\forall y (y <_{𝑸} x \to y \in A) \land \exists y \in A x <_{𝑸} y)$
18	17	simpld	$⊢ (A \in 𝑷 \land x \in A) \to \forall y (y <_{𝑸} x \to y \in A)$
19	18	19.21bi	$⊢ (A \in 𝑷 \land x \in A) \to (y <_{𝑸} x \to y \in A)$
20	19	imp	$⊢ ((A \in 𝑷 \land x \in A) \land y <_{𝑸} x) \to y \in A$
21	10 14 20	vtocl2g	$⊢ (B \in A \land C \in V) \to (((A \in 𝑷 \land B \in A) \land C <_{𝑸} B) \to C \in A)$
22	5 21	sylan2	$⊢ (B \in A \land C <_{𝑸} B) \to (((A \in 𝑷 \land B \in A) \land C <_{𝑸} B) \to C \in A)$
23	22	adantll	$⊢ ((A \in 𝑷 \land B \in A) \land C <_{𝑸} B) \to (((A \in 𝑷 \land B \in A) \land C <_{𝑸} B) \to C \in A)$
24	23	pm2.43i	$⊢ ((A \in 𝑷 \land B \in A) \land C <_{𝑸} B) \to C \in A$
25	24	ex	$⊢ (A \in 𝑷 \land B \in A) \to (C <_{𝑸} B \to C \in A)$

Metamath Proof Explorer

Theorem prcdnq

Proof