Metamath Proof Explorer

Theorem ltexpri

Description: Proposition 9-3.5(iv) of Gleason p. 123. (Contributed by NM, 13-May-1996) (Revised by Mario Carneiro, 14-Jun-2013) (New usage is discouraged.)

Ref Expression
Assertion ltexpri ⊢ A < 𝑷 B → ∃ x ∈ 𝑷 A + 𝑷 x = B

Proof

Step Hyp Ref Expression
1 ltrelpr ⊢ < 𝑷 ⊆ 𝑷 × 𝑷
2 1 brel ⊢ A < 𝑷 B → A ∈ 𝑷 ∧ B ∈ 𝑷
3 ltprord ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 → A < 𝑷 B ↔ A ⊂ B
4 oveq2 ⊢ y = z → w + 𝑸 y = w + 𝑸 z
5 4 eleq1d ⊢ y = z → w + 𝑸 y ∈ B ↔ w + 𝑸 z ∈ B
6 5 anbi2d ⊢ y = z → ¬ w ∈ A ∧ w + 𝑸 y ∈ B ↔ ¬ w ∈ A ∧ w + 𝑸 z ∈ B
7 6 exbidv ⊢ y = z → ∃ w ¬ w ∈ A ∧ w + 𝑸 y ∈ B ↔ ∃ w ¬ w ∈ A ∧ w + 𝑸 z ∈ B
8 7 cbvabv ⊢ y | ∃ w ¬ w ∈ A ∧ w + 𝑸 y ∈ B = z | ∃ w ¬ w ∈ A ∧ w + 𝑸 z ∈ B
9 8 ltexprlem5 ⊢ B ∈ 𝑷 ∧ A ⊂ B → y | ∃ w ¬ w ∈ A ∧ w + 𝑸 y ∈ B ∈ 𝑷
10 9 adantll ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ A ⊂ B → y | ∃ w ¬ w ∈ A ∧ w + 𝑸 y ∈ B ∈ 𝑷
11 8 ltexprlem6 ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ A ⊂ B → A + 𝑷 y | ∃ w ¬ w ∈ A ∧ w + 𝑸 y ∈ B ⊆ B
12 8 ltexprlem7 ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ A ⊂ B → B ⊆ A + 𝑷 y | ∃ w ¬ w ∈ A ∧ w + 𝑸 y ∈ B
13 11 12 eqssd ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ A ⊂ B → A + 𝑷 y | ∃ w ¬ w ∈ A ∧ w + 𝑸 y ∈ B = B
14 oveq2 ⊢ x = y | ∃ w ¬ w ∈ A ∧ w + 𝑸 y ∈ B → A + 𝑷 x = A + 𝑷 y | ∃ w ¬ w ∈ A ∧ w + 𝑸 y ∈ B
15 14 eqeq1d ⊢ x = y | ∃ w ¬ w ∈ A ∧ w + 𝑸 y ∈ B → A + 𝑷 x = B ↔ A + 𝑷 y | ∃ w ¬ w ∈ A ∧ w + 𝑸 y ∈ B = B
16 15 rspcev ⊢ y | ∃ w ¬ w ∈ A ∧ w + 𝑸 y ∈ B ∈ 𝑷 ∧ A + 𝑷 y | ∃ w ¬ w ∈ A ∧ w + 𝑸 y ∈ B = B → ∃ x ∈ 𝑷 A + 𝑷 x = B
17 10 13 16 syl2anc ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 ∧ A ⊂ B → ∃ x ∈ 𝑷 A + 𝑷 x = B
18 17 ex ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 → A ⊂ B → ∃ x ∈ 𝑷 A + 𝑷 x = B
19 3 18 sylbid ⊢ A ∈ 𝑷 ∧ B ∈ 𝑷 → A < 𝑷 B → ∃ x ∈ 𝑷 A + 𝑷 x = B
20 2 19 mpcom ⊢ A < 𝑷 B → ∃ x ∈ 𝑷 A + 𝑷 x = B