Step | Hyp | Ref
| Expression |
1 | | ltexprlem.1 |
. . . . . 6
⊢ 𝐶 = {𝑥 ∣ ∃𝑦(¬ 𝑦 ∈ 𝐴 ∧ (𝑦 +Q 𝑥) ∈ 𝐵)} |
2 | 1 | ltexprlem5 10795 |
. . . . 5
⊢ ((𝐵 ∈ P ∧
𝐴 ⊊ 𝐵) → 𝐶 ∈ P) |
3 | | df-plp 10738 |
. . . . . 6
⊢
+P = (𝑧 ∈ P, 𝑦 ∈ P ↦ {𝑓 ∣ ∃𝑔 ∈ 𝑧 ∃ℎ ∈ 𝑦 𝑓 = (𝑔 +Q ℎ)}) |
4 | | addclnq 10700 |
. . . . . 6
⊢ ((𝑔 ∈ Q ∧
ℎ ∈ Q)
→ (𝑔
+Q ℎ) ∈ Q) |
5 | 3, 4 | genpelv 10755 |
. . . . 5
⊢ ((𝐴 ∈ P ∧
𝐶 ∈ P)
→ (𝑧 ∈ (𝐴 +P
𝐶) ↔ ∃𝑤 ∈ 𝐴 ∃𝑥 ∈ 𝐶 𝑧 = (𝑤 +Q 𝑥))) |
6 | 2, 5 | sylan2 593 |
. . . 4
⊢ ((𝐴 ∈ P ∧
(𝐵 ∈ P
∧ 𝐴 ⊊ 𝐵)) → (𝑧 ∈ (𝐴 +P 𝐶) ↔ ∃𝑤 ∈ 𝐴 ∃𝑥 ∈ 𝐶 𝑧 = (𝑤 +Q 𝑥))) |
7 | 1 | abeq2i 2877 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ 𝐶 ↔ ∃𝑦(¬ 𝑦 ∈ 𝐴 ∧ (𝑦 +Q 𝑥) ∈ 𝐵)) |
8 | | elprnq 10746 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐵 ∈ P ∧
(𝑦
+Q 𝑥) ∈ 𝐵) → (𝑦 +Q 𝑥) ∈
Q) |
9 | | addnqf 10703 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
+Q :(Q ×
Q)⟶Q |
10 | 9 | fdmi 6609 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ dom
+Q = (Q ×
Q) |
11 | | 0nnq 10679 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ¬
∅ ∈ Q |
12 | 10, 11 | ndmovrcl 7450 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 +Q
𝑥) ∈ Q
→ (𝑦 ∈
Q ∧ 𝑥
∈ Q)) |
13 | 12 | simpld 495 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 +Q
𝑥) ∈ Q
→ 𝑦 ∈
Q) |
14 | 8, 13 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐵 ∈ P ∧
(𝑦
+Q 𝑥) ∈ 𝐵) → 𝑦 ∈ Q) |
15 | | prub 10749 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ∈ P ∧
𝑤 ∈ 𝐴) ∧ 𝑦 ∈ Q) → (¬ 𝑦 ∈ 𝐴 → 𝑤 <Q 𝑦)) |
16 | 14, 15 | sylan2 593 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ P ∧
𝑤 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ (𝑦 +Q
𝑥) ∈ 𝐵)) → (¬ 𝑦 ∈ 𝐴 → 𝑤 <Q 𝑦)) |
17 | 12 | simprd 496 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑦 +Q
𝑥) ∈ Q
→ 𝑥 ∈
Q) |
18 | | vex 3435 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑤 ∈ V |
19 | | vex 3435 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑦 ∈ V |
20 | | ltanq 10726 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑢 ∈ Q →
(𝑧
<Q 𝑣 ↔ (𝑢 +Q 𝑧) <Q
(𝑢
+Q 𝑣))) |
21 | | vex 3435 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑥 ∈ V |
22 | | addcomnq 10706 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 +Q
𝑣) = (𝑣 +Q 𝑧) |
23 | 18, 19, 20, 21, 22 | caovord2 7476 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ Q →
(𝑤
<Q 𝑦 ↔ (𝑤 +Q 𝑥) <Q
(𝑦
+Q 𝑥))) |
24 | 8, 17, 23 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐵 ∈ P ∧
(𝑦
+Q 𝑥) ∈ 𝐵) → (𝑤 <Q 𝑦 ↔ (𝑤 +Q 𝑥) <Q
(𝑦
+Q 𝑥))) |
25 | | prcdnq 10748 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐵 ∈ P ∧
(𝑦
+Q 𝑥) ∈ 𝐵) → ((𝑤 +Q 𝑥) <Q
(𝑦
+Q 𝑥) → (𝑤 +Q 𝑥) ∈ 𝐵)) |
26 | 24, 25 | sylbid 239 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐵 ∈ P ∧
(𝑦
+Q 𝑥) ∈ 𝐵) → (𝑤 <Q 𝑦 → (𝑤 +Q 𝑥) ∈ 𝐵)) |
27 | 26 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ P ∧
𝑤 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ (𝑦 +Q
𝑥) ∈ 𝐵)) → (𝑤 <Q 𝑦 → (𝑤 +Q 𝑥) ∈ 𝐵)) |
28 | 16, 27 | syld 47 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ P ∧
𝑤 ∈ 𝐴) ∧ (𝐵 ∈ P ∧ (𝑦 +Q
𝑥) ∈ 𝐵)) → (¬ 𝑦 ∈ 𝐴 → (𝑤 +Q 𝑥) ∈ 𝐵)) |
29 | 28 | exp32 421 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ P ∧
𝑤 ∈ 𝐴) → (𝐵 ∈ P → ((𝑦 +Q
𝑥) ∈ 𝐵 → (¬ 𝑦 ∈ 𝐴 → (𝑤 +Q 𝑥) ∈ 𝐵)))) |
30 | 29 | com34 91 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ P ∧
𝑤 ∈ 𝐴) → (𝐵 ∈ P → (¬ 𝑦 ∈ 𝐴 → ((𝑦 +Q 𝑥) ∈ 𝐵 → (𝑤 +Q 𝑥) ∈ 𝐵)))) |
31 | 30 | imp4b 422 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ P ∧
𝑤 ∈ 𝐴) ∧ 𝐵 ∈ P) → ((¬
𝑦 ∈ 𝐴 ∧ (𝑦 +Q 𝑥) ∈ 𝐵) → (𝑤 +Q 𝑥) ∈ 𝐵)) |
32 | 31 | exlimdv 1940 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ P ∧
𝑤 ∈ 𝐴) ∧ 𝐵 ∈ P) →
(∃𝑦(¬ 𝑦 ∈ 𝐴 ∧ (𝑦 +Q 𝑥) ∈ 𝐵) → (𝑤 +Q 𝑥) ∈ 𝐵)) |
33 | 7, 32 | syl5bi 241 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ P ∧
𝑤 ∈ 𝐴) ∧ 𝐵 ∈ P) → (𝑥 ∈ 𝐶 → (𝑤 +Q 𝑥) ∈ 𝐵)) |
34 | 33 | exp31 420 |
. . . . . . . . . 10
⊢ (𝐴 ∈ P →
(𝑤 ∈ 𝐴 → (𝐵 ∈ P → (𝑥 ∈ 𝐶 → (𝑤 +Q 𝑥) ∈ 𝐵)))) |
35 | 34 | com23 86 |
. . . . . . . . 9
⊢ (𝐴 ∈ P →
(𝐵 ∈ P
→ (𝑤 ∈ 𝐴 → (𝑥 ∈ 𝐶 → (𝑤 +Q 𝑥) ∈ 𝐵)))) |
36 | 35 | imp43 428 |
. . . . . . . 8
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P)
∧ (𝑤 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶)) → (𝑤 +Q 𝑥) ∈ 𝐵) |
37 | | eleq1 2828 |
. . . . . . . . 9
⊢ (𝑧 = (𝑤 +Q 𝑥) → (𝑧 ∈ 𝐵 ↔ (𝑤 +Q 𝑥) ∈ 𝐵)) |
38 | 37 | biimparc 480 |
. . . . . . . 8
⊢ (((𝑤 +Q
𝑥) ∈ 𝐵 ∧ 𝑧 = (𝑤 +Q 𝑥)) → 𝑧 ∈ 𝐵) |
39 | 36, 38 | sylan 580 |
. . . . . . 7
⊢ ((((𝐴 ∈ P ∧
𝐵 ∈ P)
∧ (𝑤 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶)) ∧ 𝑧 = (𝑤 +Q 𝑥)) → 𝑧 ∈ 𝐵) |
40 | 39 | exp31 420 |
. . . . . 6
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ ((𝑤 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶) → (𝑧 = (𝑤 +Q 𝑥) → 𝑧 ∈ 𝐵))) |
41 | 40 | rexlimdvv 3224 |
. . . . 5
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ (∃𝑤 ∈
𝐴 ∃𝑥 ∈ 𝐶 𝑧 = (𝑤 +Q 𝑥) → 𝑧 ∈ 𝐵)) |
42 | 41 | adantrr 714 |
. . . 4
⊢ ((𝐴 ∈ P ∧
(𝐵 ∈ P
∧ 𝐴 ⊊ 𝐵)) → (∃𝑤 ∈ 𝐴 ∃𝑥 ∈ 𝐶 𝑧 = (𝑤 +Q 𝑥) → 𝑧 ∈ 𝐵)) |
43 | 6, 42 | sylbid 239 |
. . 3
⊢ ((𝐴 ∈ P ∧
(𝐵 ∈ P
∧ 𝐴 ⊊ 𝐵)) → (𝑧 ∈ (𝐴 +P 𝐶) → 𝑧 ∈ 𝐵)) |
44 | 43 | ssrdv 3932 |
. 2
⊢ ((𝐴 ∈ P ∧
(𝐵 ∈ P
∧ 𝐴 ⊊ 𝐵)) → (𝐴 +P 𝐶) ⊆ 𝐵) |
45 | 44 | anassrs 468 |
1
⊢ (((𝐴 ∈ P ∧
𝐵 ∈ P)
∧ 𝐴 ⊊ 𝐵) → (𝐴 +P 𝐶) ⊆ 𝐵) |