This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐵 → 𝐶 ∈ 𝐴 ) )