Theorem 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	⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ 𝐴 ) → ( 𝐶 <Q 𝐵 → 𝐶 ∈ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		ltrelnq	⊢ <Q ⊆ ( Q × Q )
2		relxp	⊢ Rel ( Q × Q )
3		relss	⊢ ( <Q ⊆ ( Q × Q ) → ( Rel ( Q × Q ) → Rel <Q ) )
4	1 2 3	mp2	⊢ Rel <Q
5	4	brrelex1i	⊢ ( 𝐶 <Q 𝐵 → 𝐶 ∈ V )
6		eleq1	⊢ ( 𝑥 = 𝐵 → ( 𝑥 ∈ 𝐴 ↔ 𝐵 ∈ 𝐴 ) )
7	6	anbi2d	⊢ ( 𝑥 = 𝐵 → ( ( 𝐴 ∈ P ∧ 𝑥 ∈ 𝐴 ) ↔ ( 𝐴 ∈ P ∧ 𝐵 ∈ 𝐴 ) ) )
8		breq2	⊢ ( 𝑥 = 𝐵 → ( 𝑦 <Q 𝑥 ↔ 𝑦 <Q 𝐵 ) )
9	7 8	anbi12d	⊢ ( 𝑥 = 𝐵 → ( ( ( 𝐴 ∈ P ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 <Q 𝑥 ) ↔ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ 𝐴 ) ∧ 𝑦 <Q 𝐵 ) ) )
10	9	imbi1d	⊢ ( 𝑥 = 𝐵 → ( ( ( ( 𝐴 ∈ P ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 <Q 𝑥 ) → 𝑦 ∈ 𝐴 ) ↔ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ 𝐴 ) ∧ 𝑦 <Q 𝐵 ) → 𝑦 ∈ 𝐴 ) ) )
11		breq1	⊢ ( 𝑦 = 𝐶 → ( 𝑦 <Q 𝐵 ↔ 𝐶 <Q 𝐵 ) )
12	11	anbi2d	⊢ ( 𝑦 = 𝐶 → ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ 𝐴 ) ∧ 𝑦 <Q 𝐵 ) ↔ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ 𝐴 ) ∧ 𝐶 <Q 𝐵 ) ) )
13		eleq1	⊢ ( 𝑦 = 𝐶 → ( 𝑦 ∈ 𝐴 ↔ 𝐶 ∈ 𝐴 ) )
14	12 13	imbi12d	⊢ ( 𝑦 = 𝐶 → ( ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ 𝐴 ) ∧ 𝑦 <Q 𝐵 ) → 𝑦 ∈ 𝐴 ) ↔ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ 𝐴 ) ∧ 𝐶 <Q 𝐵 ) → 𝐶 ∈ 𝐴 ) ) )
15		elnpi	⊢ ( 𝐴 ∈ P ↔ ( ( 𝐴 ∈ V ∧ ∅ ⊊ 𝐴 ∧ 𝐴 ⊊ Q ) ∧ ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ( 𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴 ) ∧ ∃ 𝑦 ∈ 𝐴 𝑥 <Q 𝑦 ) ) )
16	15	simprbi	⊢ ( 𝐴 ∈ P → ∀ 𝑥 ∈ 𝐴 ( ∀ 𝑦 ( 𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴 ) ∧ ∃ 𝑦 ∈ 𝐴 𝑥 <Q 𝑦 ) )
17	16	r19.21bi	⊢ ( ( 𝐴 ∈ P ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑦 ( 𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴 ) ∧ ∃ 𝑦 ∈ 𝐴 𝑥 <Q 𝑦 ) )
18	17	simpld	⊢ ( ( 𝐴 ∈ P ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑦 ( 𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴 ) )
19	18	19.21bi	⊢ ( ( 𝐴 ∈ P ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 <Q 𝑥 → 𝑦 ∈ 𝐴 ) )
20	19	imp	⊢ ( ( ( 𝐴 ∈ P ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 <Q 𝑥 ) → 𝑦 ∈ 𝐴 )
21	10 14 20	vtocl2g	⊢ ( ( 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ V ) → ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ 𝐴 ) ∧ 𝐶 <Q 𝐵 ) → 𝐶 ∈ 𝐴 ) )
22	5 21	sylan2	⊢ ( ( 𝐵 ∈ 𝐴 ∧ 𝐶 <Q 𝐵 ) → ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ 𝐴 ) ∧ 𝐶 <Q 𝐵 ) → 𝐶 ∈ 𝐴 ) )
23	22	adantll	⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ 𝐴 ) ∧ 𝐶 <Q 𝐵 ) → ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ 𝐴 ) ∧ 𝐶 <Q 𝐵 ) → 𝐶 ∈ 𝐴 ) )
24	23	pm2.43i	⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ 𝐴 ) ∧ 𝐶 <Q 𝐵 ) → 𝐶 ∈ 𝐴 )
25	24	ex	⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ 𝐴 ) → ( 𝐶 <Q 𝐵 → 𝐶 ∈ 𝐴 ) )