Metamath Proof Explorer

Theorem ltexprlem3

Description: Lemma for Proposition 9-3.5(iv) of Gleason p. 123. (Contributed by NM, 6-Apr-1996) (New usage is discouraged.)

Ref Expression
Hypothesis ltexprlem.1 ⊢ C = x | ∃ y ¬ y ∈ A ∧ y + 𝑸 x ∈ B
Assertion ltexprlem3 ⊢ B ∈ 𝑷 → x ∈ C → ∀ z z < 𝑸 x → z ∈ C

Proof

Step Hyp Ref Expression
1 ltexprlem.1 ⊢ C = x | ∃ y ¬ y ∈ A ∧ y + 𝑸 x ∈ B
2 elprnq ⊢ B ∈ 𝑷 ∧ y + 𝑸 x ∈ B → y + 𝑸 x ∈ 𝑸
3 addnqf ⊢ + 𝑸 : 𝑸 × 𝑸 ⟶ 𝑸
4 3 fdmi ⊢ dom ⁡ + 𝑸 = 𝑸 × 𝑸
5 0nnq ⊢ ¬ ∅ ∈ 𝑸
6 4 5 ndmovrcl ⊢ y + 𝑸 x ∈ 𝑸 → y ∈ 𝑸 ∧ x ∈ 𝑸
7 6 simpld ⊢ y + 𝑸 x ∈ 𝑸 → y ∈ 𝑸
8 ltanq ⊢ y ∈ 𝑸 → z < 𝑸 x ↔ y + 𝑸 z < 𝑸 y + 𝑸 x
9 2 7 8 3syl ⊢ B ∈ 𝑷 ∧ y + 𝑸 x ∈ B → z < 𝑸 x ↔ y + 𝑸 z < 𝑸 y + 𝑸 x
10 prcdnq ⊢ B ∈ 𝑷 ∧ y + 𝑸 x ∈ B → y + 𝑸 z < 𝑸 y + 𝑸 x → y + 𝑸 z ∈ B
11 9 10 sylbid ⊢ B ∈ 𝑷 ∧ y + 𝑸 x ∈ B → z < 𝑸 x → y + 𝑸 z ∈ B
12 11 impancom ⊢ B ∈ 𝑷 ∧ z < 𝑸 x → y + 𝑸 x ∈ B → y + 𝑸 z ∈ B
13 12 anim2d ⊢ B ∈ 𝑷 ∧ z < 𝑸 x → ¬ y ∈ A ∧ y + 𝑸 x ∈ B → ¬ y ∈ A ∧ y + 𝑸 z ∈ B
14 13 eximdv ⊢ B ∈ 𝑷 ∧ z < 𝑸 x → ∃ y ¬ y ∈ A ∧ y + 𝑸 x ∈ B → ∃ y ¬ y ∈ A ∧ y + 𝑸 z ∈ B
15 1 abeq2i ⊢ x ∈ C ↔ ∃ y ¬ y ∈ A ∧ y + 𝑸 x ∈ B
16 vex ⊢ z ∈ V
17 oveq2 ⊢ x = z → y + 𝑸 x = y + 𝑸 z
18 17 eleq1d ⊢ x = z → y + 𝑸 x ∈ B ↔ y + 𝑸 z ∈ B
19 18 anbi2d ⊢ x = z → ¬ y ∈ A ∧ y + 𝑸 x ∈ B ↔ ¬ y ∈ A ∧ y + 𝑸 z ∈ B
20 19 exbidv ⊢ x = z → ∃ y ¬ y ∈ A ∧ y + 𝑸 x ∈ B ↔ ∃ y ¬ y ∈ A ∧ y + 𝑸 z ∈ B
21 16 20 1 elab2 ⊢ z ∈ C ↔ ∃ y ¬ y ∈ A ∧ y + 𝑸 z ∈ B
22 14 15 21 3imtr4g ⊢ B ∈ 𝑷 ∧ z < 𝑸 x → x ∈ C → z ∈ C
23 22 ex ⊢ B ∈ 𝑷 → z < 𝑸 x → x ∈ C → z ∈ C
24 23 com23 ⊢ B ∈ 𝑷 → x ∈ C → z < 𝑸 x → z ∈ C
25 24 alrimdv ⊢ B ∈ 𝑷 → x ∈ C → ∀ z z < 𝑸 x → z ∈ C