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

Theorem ltexprlem2 9897
 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 2764 . . . 4 (𝑥𝐶 ↔ ∃𝑦𝑦𝐴 ∧ (𝑦 +Q 𝑥) ∈ 𝐵))
3 elprnq 9851 . . . . . . . . 9 ((𝐵P ∧ (𝑦 +Q 𝑥) ∈ 𝐵) → (𝑦 +Q 𝑥) ∈ Q)
4 addnqf 9808 . . . . . . . . . . 11 +Q :(Q × Q)⟶Q
54fdmi 6090 . . . . . . . . . 10 dom +Q = (Q × Q)
6 0nnq 9784 . . . . . . . . . 10 ¬ ∅ ∈ Q
75, 6ndmovrcl 6862 . . . . . . . . 9 ((𝑦 +Q 𝑥) ∈ Q → (𝑦Q𝑥Q))
83, 7syl 17 . . . . . . . 8 ((𝐵P ∧ (𝑦 +Q 𝑥) ∈ 𝐵) → (𝑦Q𝑥Q))
9 ltaddnq 9834 . . . . . . . . . . 11 ((𝑥Q𝑦Q) → 𝑥 <Q (𝑥 +Q 𝑦))
109ancoms 468 . . . . . . . . . 10 ((𝑦Q𝑥Q) → 𝑥 <Q (𝑥 +Q 𝑦))
11 addcomnq 9811 . . . . . . . . . 10 (𝑥 +Q 𝑦) = (𝑦 +Q 𝑥)
1210, 11syl6breq 4726 . . . . . . . . 9 ((𝑦Q𝑥Q) → 𝑥 <Q (𝑦 +Q 𝑥))
13 prcdnq 9853 . . . . . . . . 9 ((𝐵P ∧ (𝑦 +Q 𝑥) ∈ 𝐵) → (𝑥 <Q (𝑦 +Q 𝑥) → 𝑥𝐵))
1412, 13syl5 34 . . . . . . . 8 ((𝐵P ∧ (𝑦 +Q 𝑥) ∈ 𝐵) → ((𝑦Q𝑥Q) → 𝑥𝐵))
158, 14mpd 15 . . . . . . 7 ((𝐵P ∧ (𝑦 +Q 𝑥) ∈ 𝐵) → 𝑥𝐵)
1615ex 449 . . . . . 6 (𝐵P → ((𝑦 +Q 𝑥) ∈ 𝐵𝑥𝐵))
1716adantld 482 . . . . 5 (𝐵P → ((¬ 𝑦𝐴 ∧ (𝑦 +Q 𝑥) ∈ 𝐵) → 𝑥𝐵))
1817exlimdv 1901 . . . 4 (𝐵P → (∃𝑦𝑦𝐴 ∧ (𝑦 +Q 𝑥) ∈ 𝐵) → 𝑥𝐵))
192, 18syl5bi 232 . . 3 (𝐵P → (𝑥𝐶𝑥𝐵))
2019ssrdv 3642 . 2 (𝐵P𝐶𝐵)
21 prpssnq 9850 . 2 (𝐵P𝐵Q)
2220, 21sspsstrd 3748 1 (𝐵P𝐶Q)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383   = wceq 1523  ∃wex 1744   ∈ wcel 2030  {cab 2637   ⊊ wpss 3608   class class class wbr 4685   × cxp 5141  (class class class)co 6690  Qcnq 9712   +Q cplq 9715
 Copyright terms: Public domain W3C validator