Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ltexprlem2 Structured version   Visualization version   GIF version

Theorem ltexprlem2 10502
 Description: Lemma for Proposition 9-3.5(iv) of [Gleason] p. 123. (Contributed by NM, 3-Apr-1996.) (New usage is discouraged.)
Hypothesis
Ref Expression
ltexprlem.1 𝐶 = {𝑥 ∣ ∃𝑦𝑦𝐴 ∧ (𝑦 +Q 𝑥) ∈ 𝐵)}
Assertion
Ref Expression
ltexprlem2 (𝐵P𝐶Q)
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐵,𝑦   𝑥,𝐶
Allowed substitution hint:   𝐶(𝑦)

Proof of Theorem ltexprlem2
StepHypRef Expression
1 ltexprlem.1 . . . . 5 𝐶 = {𝑥 ∣ ∃𝑦𝑦𝐴 ∧ (𝑦 +Q 𝑥) ∈ 𝐵)}
21abeq2i 2887 . . . 4 (𝑥𝐶 ↔ ∃𝑦𝑦𝐴 ∧ (𝑦 +Q 𝑥) ∈ 𝐵))
3 elprnq 10456 . . . . . . . . 9 ((𝐵P ∧ (𝑦 +Q 𝑥) ∈ 𝐵) → (𝑦 +Q 𝑥) ∈ Q)
4 addnqf 10413 . . . . . . . . . . 11 +Q :(Q × Q)⟶Q
54fdmi 6513 . . . . . . . . . 10 dom +Q = (Q × Q)
6 0nnq 10389 . . . . . . . . . 10 ¬ ∅ ∈ Q
75, 6ndmovrcl 7335 . . . . . . . . 9 ((𝑦 +Q 𝑥) ∈ Q → (𝑦Q𝑥Q))
83, 7syl 17 . . . . . . . 8 ((𝐵P ∧ (𝑦 +Q 𝑥) ∈ 𝐵) → (𝑦Q𝑥Q))
9 ltaddnq 10439 . . . . . . . . . . 11 ((𝑥Q𝑦Q) → 𝑥 <Q (𝑥 +Q 𝑦))
109ancoms 462 . . . . . . . . . 10 ((𝑦Q𝑥Q) → 𝑥 <Q (𝑥 +Q 𝑦))
11 addcomnq 10416 . . . . . . . . . 10 (𝑥 +Q 𝑦) = (𝑦 +Q 𝑥)
1210, 11breqtrdi 5076 . . . . . . . . 9 ((𝑦Q𝑥Q) → 𝑥 <Q (𝑦 +Q 𝑥))
13 prcdnq 10458 . . . . . . . . 9 ((𝐵P ∧ (𝑦 +Q 𝑥) ∈ 𝐵) → (𝑥 <Q (𝑦 +Q 𝑥) → 𝑥𝐵))
1412, 13syl5 34 . . . . . . . 8 ((𝐵P ∧ (𝑦 +Q 𝑥) ∈ 𝐵) → ((𝑦Q𝑥Q) → 𝑥𝐵))
158, 14mpd 15 . . . . . . 7 ((𝐵P ∧ (𝑦 +Q 𝑥) ∈ 𝐵) → 𝑥𝐵)
1615ex 416 . . . . . 6 (𝐵P → ((𝑦 +Q 𝑥) ∈ 𝐵𝑥𝐵))
1716adantld 494 . . . . 5 (𝐵P → ((¬ 𝑦𝐴 ∧ (𝑦 +Q 𝑥) ∈ 𝐵) → 𝑥𝐵))
1817exlimdv 1934 . . . 4 (𝐵P → (∃𝑦𝑦𝐴 ∧ (𝑦 +Q 𝑥) ∈ 𝐵) → 𝑥𝐵))
192, 18syl5bi 245 . . 3 (𝐵P → (𝑥𝐶𝑥𝐵))
2019ssrdv 3900 . 2 (𝐵P𝐶𝐵)
21 prpssnq 10455 . 2 (𝐵P𝐵Q)
2220, 21sspsstrd 4016 1 (𝐵P𝐶Q)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2111  {cab 2735   ⊊ wpss 3861   class class class wbr 5035   × cxp 5525  (class class class)co 7155  Qcnq 10317   +Q cplq 10320
 Copyright terms: Public domain W3C validator