Step | Hyp | Ref
| Expression |
1 | | prnmax 10762 |
. . . . . . . . 9
⊢ ((𝐵 ∈ P ∧
(𝑦
+Q 𝑥) ∈ 𝐵) → ∃𝑤 ∈ 𝐵 (𝑦 +Q 𝑥) <Q
𝑤) |
2 | | df-rex 3072 |
. . . . . . . . 9
⊢
(∃𝑤 ∈
𝐵 (𝑦 +Q 𝑥) <Q
𝑤 ↔ ∃𝑤(𝑤 ∈ 𝐵 ∧ (𝑦 +Q 𝑥) <Q
𝑤)) |
3 | 1, 2 | sylib 217 |
. . . . . . . 8
⊢ ((𝐵 ∈ P ∧
(𝑦
+Q 𝑥) ∈ 𝐵) → ∃𝑤(𝑤 ∈ 𝐵 ∧ (𝑦 +Q 𝑥) <Q
𝑤)) |
4 | | ltrelnq 10693 |
. . . . . . . . . . . . . . . . . . . 20
⊢
<Q ⊆ (Q ×
Q) |
5 | 4 | brel 5653 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 +Q
𝑥)
<Q 𝑤 → ((𝑦 +Q 𝑥) ∈ Q ∧
𝑤 ∈
Q)) |
6 | 5 | simpld 495 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 +Q
𝑥)
<Q 𝑤 → (𝑦 +Q 𝑥) ∈
Q) |
7 | | addnqf 10715 |
. . . . . . . . . . . . . . . . . . . 20
⊢
+Q :(Q ×
Q)⟶Q |
8 | 7 | fdmi 6610 |
. . . . . . . . . . . . . . . . . . 19
⊢ dom
+Q = (Q ×
Q) |
9 | | 0nnq 10691 |
. . . . . . . . . . . . . . . . . . 19
⊢ ¬
∅ ∈ Q |
10 | 8, 9 | ndmovrcl 7453 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 +Q
𝑥) ∈ Q
→ (𝑦 ∈
Q ∧ 𝑥
∈ Q)) |
11 | 6, 10 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 +Q
𝑥)
<Q 𝑤 → (𝑦 ∈ Q ∧ 𝑥 ∈
Q)) |
12 | | ltaddnq 10741 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ Q ∧
𝑥 ∈ Q)
→ 𝑦
<Q (𝑦 +Q 𝑥)) |
13 | | ltsonq 10736 |
. . . . . . . . . . . . . . . . . . 19
⊢
<Q Or Q |
14 | 13, 4 | sotri 6031 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 <Q
(𝑦
+Q 𝑥) ∧ (𝑦 +Q 𝑥) <Q
𝑤) → 𝑦 <Q
𝑤) |
15 | 12, 14 | sylan 580 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑦 ∈ Q ∧
𝑥 ∈ Q)
∧ (𝑦
+Q 𝑥) <Q 𝑤) → 𝑦 <Q 𝑤) |
16 | 11, 15 | mpancom 685 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 +Q
𝑥)
<Q 𝑤 → 𝑦 <Q 𝑤) |
17 | 4 | brel 5653 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 <Q
𝑤 → (𝑦 ∈ Q ∧
𝑤 ∈
Q)) |
18 | 17 | simprd 496 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 <Q
𝑤 → 𝑤 ∈ Q) |
19 | | ltexnq 10742 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ Q →
(𝑦
<Q 𝑤 ↔ ∃𝑧(𝑦 +Q 𝑧) = 𝑤)) |
20 | 19 | biimpd 228 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ Q →
(𝑦
<Q 𝑤 → ∃𝑧(𝑦 +Q 𝑧) = 𝑤)) |
21 | 18, 20 | mpcom 38 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 <Q
𝑤 → ∃𝑧(𝑦 +Q 𝑧) = 𝑤) |
22 | 16, 21 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 +Q
𝑥)
<Q 𝑤 → ∃𝑧(𝑦 +Q 𝑧) = 𝑤) |
23 | | eqcom 2747 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = (𝑦 +Q 𝑧) ↔ (𝑦 +Q 𝑧) = 𝑤) |
24 | 23 | exbii 1854 |
. . . . . . . . . . . . . . 15
⊢
(∃𝑧 𝑤 = (𝑦 +Q 𝑧) ↔ ∃𝑧(𝑦 +Q 𝑧) = 𝑤) |
25 | 22, 24 | sylibr 233 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 +Q
𝑥)
<Q 𝑤 → ∃𝑧 𝑤 = (𝑦 +Q 𝑧)) |
26 | 25 | ancri 550 |
. . . . . . . . . . . . 13
⊢ ((𝑦 +Q
𝑥)
<Q 𝑤 → (∃𝑧 𝑤 = (𝑦 +Q 𝑧) ∧ (𝑦 +Q 𝑥) <Q
𝑤)) |
27 | 26 | anim2i 617 |
. . . . . . . . . . . 12
⊢ ((𝑤 ∈ 𝐵 ∧ (𝑦 +Q 𝑥) <Q
𝑤) → (𝑤 ∈ 𝐵 ∧ (∃𝑧 𝑤 = (𝑦 +Q 𝑧) ∧ (𝑦 +Q 𝑥) <Q
𝑤))) |
28 | | an12 642 |
. . . . . . . . . . . 12
⊢
((∃𝑧 𝑤 = (𝑦 +Q 𝑧) ∧ (𝑤 ∈ 𝐵 ∧ (𝑦 +Q 𝑥) <Q
𝑤)) ↔ (𝑤 ∈ 𝐵 ∧ (∃𝑧 𝑤 = (𝑦 +Q 𝑧) ∧ (𝑦 +Q 𝑥) <Q
𝑤))) |
29 | 27, 28 | sylibr 233 |
. . . . . . . . . . 11
⊢ ((𝑤 ∈ 𝐵 ∧ (𝑦 +Q 𝑥) <Q
𝑤) → (∃𝑧 𝑤 = (𝑦 +Q 𝑧) ∧ (𝑤 ∈ 𝐵 ∧ (𝑦 +Q 𝑥) <Q
𝑤))) |
30 | | 19.41v 1957 |
. . . . . . . . . . 11
⊢
(∃𝑧(𝑤 = (𝑦 +Q 𝑧) ∧ (𝑤 ∈ 𝐵 ∧ (𝑦 +Q 𝑥) <Q
𝑤)) ↔ (∃𝑧 𝑤 = (𝑦 +Q 𝑧) ∧ (𝑤 ∈ 𝐵 ∧ (𝑦 +Q 𝑥) <Q
𝑤))) |
31 | 29, 30 | sylibr 233 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ 𝐵 ∧ (𝑦 +Q 𝑥) <Q
𝑤) → ∃𝑧(𝑤 = (𝑦 +Q 𝑧) ∧ (𝑤 ∈ 𝐵 ∧ (𝑦 +Q 𝑥) <Q
𝑤))) |
32 | 31 | eximi 1841 |
. . . . . . . . 9
⊢
(∃𝑤(𝑤 ∈ 𝐵 ∧ (𝑦 +Q 𝑥) <Q
𝑤) → ∃𝑤∃𝑧(𝑤 = (𝑦 +Q 𝑧) ∧ (𝑤 ∈ 𝐵 ∧ (𝑦 +Q 𝑥) <Q
𝑤))) |
33 | | excom 2166 |
. . . . . . . . 9
⊢
(∃𝑧∃𝑤(𝑤 = (𝑦 +Q 𝑧) ∧ (𝑤 ∈ 𝐵 ∧ (𝑦 +Q 𝑥) <Q
𝑤)) ↔ ∃𝑤∃𝑧(𝑤 = (𝑦 +Q 𝑧) ∧ (𝑤 ∈ 𝐵 ∧ (𝑦 +Q 𝑥) <Q
𝑤))) |
34 | 32, 33 | sylibr 233 |
. . . . . . . 8
⊢
(∃𝑤(𝑤 ∈ 𝐵 ∧ (𝑦 +Q 𝑥) <Q
𝑤) → ∃𝑧∃𝑤(𝑤 = (𝑦 +Q 𝑧) ∧ (𝑤 ∈ 𝐵 ∧ (𝑦 +Q 𝑥) <Q
𝑤))) |
35 | | ovex 7305 |
. . . . . . . . . . 11
⊢ (𝑦 +Q
𝑧) ∈
V |
36 | | eleq1 2828 |
. . . . . . . . . . . 12
⊢ (𝑤 = (𝑦 +Q 𝑧) → (𝑤 ∈ 𝐵 ↔ (𝑦 +Q 𝑧) ∈ 𝐵)) |
37 | | breq2 5083 |
. . . . . . . . . . . 12
⊢ (𝑤 = (𝑦 +Q 𝑧) → ((𝑦 +Q 𝑥) <Q
𝑤 ↔ (𝑦 +Q
𝑥)
<Q (𝑦 +Q 𝑧))) |
38 | 36, 37 | anbi12d 631 |
. . . . . . . . . . 11
⊢ (𝑤 = (𝑦 +Q 𝑧) → ((𝑤 ∈ 𝐵 ∧ (𝑦 +Q 𝑥) <Q
𝑤) ↔ ((𝑦 +Q
𝑧) ∈ 𝐵 ∧ (𝑦 +Q 𝑥) <Q
(𝑦
+Q 𝑧)))) |
39 | 35, 38 | ceqsexv 3478 |
. . . . . . . . . 10
⊢
(∃𝑤(𝑤 = (𝑦 +Q 𝑧) ∧ (𝑤 ∈ 𝐵 ∧ (𝑦 +Q 𝑥) <Q
𝑤)) ↔ ((𝑦 +Q
𝑧) ∈ 𝐵 ∧ (𝑦 +Q 𝑥) <Q
(𝑦
+Q 𝑧))) |
40 | | ltanq 10738 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ Q →
(𝑥
<Q 𝑧 ↔ (𝑦 +Q 𝑥) <Q
(𝑦
+Q 𝑧))) |
41 | 8, 4, 9, 40 | ndmovordi 7458 |
. . . . . . . . . . 11
⊢ ((𝑦 +Q
𝑥)
<Q (𝑦 +Q 𝑧) → 𝑥 <Q 𝑧) |
42 | 41 | anim2i 617 |
. . . . . . . . . 10
⊢ (((𝑦 +Q
𝑧) ∈ 𝐵 ∧ (𝑦 +Q 𝑥) <Q
(𝑦
+Q 𝑧)) → ((𝑦 +Q 𝑧) ∈ 𝐵 ∧ 𝑥 <Q 𝑧)) |
43 | 39, 42 | sylbi 216 |
. . . . . . . . 9
⊢
(∃𝑤(𝑤 = (𝑦 +Q 𝑧) ∧ (𝑤 ∈ 𝐵 ∧ (𝑦 +Q 𝑥) <Q
𝑤)) → ((𝑦 +Q
𝑧) ∈ 𝐵 ∧ 𝑥 <Q 𝑧)) |
44 | 43 | eximi 1841 |
. . . . . . . 8
⊢
(∃𝑧∃𝑤(𝑤 = (𝑦 +Q 𝑧) ∧ (𝑤 ∈ 𝐵 ∧ (𝑦 +Q 𝑥) <Q
𝑤)) → ∃𝑧((𝑦 +Q 𝑧) ∈ 𝐵 ∧ 𝑥 <Q 𝑧)) |
45 | 3, 34, 44 | 3syl 18 |
. . . . . . 7
⊢ ((𝐵 ∈ P ∧
(𝑦
+Q 𝑥) ∈ 𝐵) → ∃𝑧((𝑦 +Q 𝑧) ∈ 𝐵 ∧ 𝑥 <Q 𝑧)) |
46 | 45 | anim2i 617 |
. . . . . 6
⊢ ((¬
𝑦 ∈ 𝐴 ∧ (𝐵 ∈ P ∧ (𝑦 +Q
𝑥) ∈ 𝐵)) → (¬ 𝑦 ∈ 𝐴 ∧ ∃𝑧((𝑦 +Q 𝑧) ∈ 𝐵 ∧ 𝑥 <Q 𝑧))) |
47 | 46 | an12s 646 |
. . . . 5
⊢ ((𝐵 ∈ P ∧
(¬ 𝑦 ∈ 𝐴 ∧ (𝑦 +Q 𝑥) ∈ 𝐵)) → (¬ 𝑦 ∈ 𝐴 ∧ ∃𝑧((𝑦 +Q 𝑧) ∈ 𝐵 ∧ 𝑥 <Q 𝑧))) |
48 | | 19.42v 1961 |
. . . . 5
⊢
(∃𝑧(¬
𝑦 ∈ 𝐴 ∧ ((𝑦 +Q 𝑧) ∈ 𝐵 ∧ 𝑥 <Q 𝑧)) ↔ (¬ 𝑦 ∈ 𝐴 ∧ ∃𝑧((𝑦 +Q 𝑧) ∈ 𝐵 ∧ 𝑥 <Q 𝑧))) |
49 | 47, 48 | sylibr 233 |
. . . 4
⊢ ((𝐵 ∈ P ∧
(¬ 𝑦 ∈ 𝐴 ∧ (𝑦 +Q 𝑥) ∈ 𝐵)) → ∃𝑧(¬ 𝑦 ∈ 𝐴 ∧ ((𝑦 +Q 𝑧) ∈ 𝐵 ∧ 𝑥 <Q 𝑧))) |
50 | 49 | ex 413 |
. . 3
⊢ (𝐵 ∈ P →
((¬ 𝑦 ∈ 𝐴 ∧ (𝑦 +Q 𝑥) ∈ 𝐵) → ∃𝑧(¬ 𝑦 ∈ 𝐴 ∧ ((𝑦 +Q 𝑧) ∈ 𝐵 ∧ 𝑥 <Q 𝑧)))) |
51 | 50 | eximdv 1924 |
. 2
⊢ (𝐵 ∈ P →
(∃𝑦(¬ 𝑦 ∈ 𝐴 ∧ (𝑦 +Q 𝑥) ∈ 𝐵) → ∃𝑦∃𝑧(¬ 𝑦 ∈ 𝐴 ∧ ((𝑦 +Q 𝑧) ∈ 𝐵 ∧ 𝑥 <Q 𝑧)))) |
52 | | ltexprlem.1 |
. . 3
⊢ 𝐶 = {𝑥 ∣ ∃𝑦(¬ 𝑦 ∈ 𝐴 ∧ (𝑦 +Q 𝑥) ∈ 𝐵)} |
53 | 52 | abeq2i 2877 |
. 2
⊢ (𝑥 ∈ 𝐶 ↔ ∃𝑦(¬ 𝑦 ∈ 𝐴 ∧ (𝑦 +Q 𝑥) ∈ 𝐵)) |
54 | | vex 3435 |
. . . . . . 7
⊢ 𝑧 ∈ V |
55 | | oveq2 7280 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → (𝑦 +Q 𝑥) = (𝑦 +Q 𝑧)) |
56 | 55 | eleq1d 2825 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → ((𝑦 +Q 𝑥) ∈ 𝐵 ↔ (𝑦 +Q 𝑧) ∈ 𝐵)) |
57 | 56 | anbi2d 629 |
. . . . . . . 8
⊢ (𝑥 = 𝑧 → ((¬ 𝑦 ∈ 𝐴 ∧ (𝑦 +Q 𝑥) ∈ 𝐵) ↔ (¬ 𝑦 ∈ 𝐴 ∧ (𝑦 +Q 𝑧) ∈ 𝐵))) |
58 | 57 | exbidv 1928 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (∃𝑦(¬ 𝑦 ∈ 𝐴 ∧ (𝑦 +Q 𝑥) ∈ 𝐵) ↔ ∃𝑦(¬ 𝑦 ∈ 𝐴 ∧ (𝑦 +Q 𝑧) ∈ 𝐵))) |
59 | 54, 58, 52 | elab2 3615 |
. . . . . 6
⊢ (𝑧 ∈ 𝐶 ↔ ∃𝑦(¬ 𝑦 ∈ 𝐴 ∧ (𝑦 +Q 𝑧) ∈ 𝐵)) |
60 | 59 | anbi1i 624 |
. . . . 5
⊢ ((𝑧 ∈ 𝐶 ∧ 𝑥 <Q 𝑧) ↔ (∃𝑦(¬ 𝑦 ∈ 𝐴 ∧ (𝑦 +Q 𝑧) ∈ 𝐵) ∧ 𝑥 <Q 𝑧)) |
61 | | 19.41v 1957 |
. . . . 5
⊢
(∃𝑦((¬
𝑦 ∈ 𝐴 ∧ (𝑦 +Q 𝑧) ∈ 𝐵) ∧ 𝑥 <Q 𝑧) ↔ (∃𝑦(¬ 𝑦 ∈ 𝐴 ∧ (𝑦 +Q 𝑧) ∈ 𝐵) ∧ 𝑥 <Q 𝑧)) |
62 | | anass 469 |
. . . . . 6
⊢ (((¬
𝑦 ∈ 𝐴 ∧ (𝑦 +Q 𝑧) ∈ 𝐵) ∧ 𝑥 <Q 𝑧) ↔ (¬ 𝑦 ∈ 𝐴 ∧ ((𝑦 +Q 𝑧) ∈ 𝐵 ∧ 𝑥 <Q 𝑧))) |
63 | 62 | exbii 1854 |
. . . . 5
⊢
(∃𝑦((¬
𝑦 ∈ 𝐴 ∧ (𝑦 +Q 𝑧) ∈ 𝐵) ∧ 𝑥 <Q 𝑧) ↔ ∃𝑦(¬ 𝑦 ∈ 𝐴 ∧ ((𝑦 +Q 𝑧) ∈ 𝐵 ∧ 𝑥 <Q 𝑧))) |
64 | 60, 61, 63 | 3bitr2i 299 |
. . . 4
⊢ ((𝑧 ∈ 𝐶 ∧ 𝑥 <Q 𝑧) ↔ ∃𝑦(¬ 𝑦 ∈ 𝐴 ∧ ((𝑦 +Q 𝑧) ∈ 𝐵 ∧ 𝑥 <Q 𝑧))) |
65 | 64 | exbii 1854 |
. . 3
⊢
(∃𝑧(𝑧 ∈ 𝐶 ∧ 𝑥 <Q 𝑧) ↔ ∃𝑧∃𝑦(¬ 𝑦 ∈ 𝐴 ∧ ((𝑦 +Q 𝑧) ∈ 𝐵 ∧ 𝑥 <Q 𝑧))) |
66 | | excom 2166 |
. . 3
⊢
(∃𝑦∃𝑧(¬ 𝑦 ∈ 𝐴 ∧ ((𝑦 +Q 𝑧) ∈ 𝐵 ∧ 𝑥 <Q 𝑧)) ↔ ∃𝑧∃𝑦(¬ 𝑦 ∈ 𝐴 ∧ ((𝑦 +Q 𝑧) ∈ 𝐵 ∧ 𝑥 <Q 𝑧))) |
67 | 65, 66 | bitr4i 277 |
. 2
⊢
(∃𝑧(𝑧 ∈ 𝐶 ∧ 𝑥 <Q 𝑧) ↔ ∃𝑦∃𝑧(¬ 𝑦 ∈ 𝐴 ∧ ((𝑦 +Q 𝑧) ∈ 𝐵 ∧ 𝑥 <Q 𝑧))) |
68 | 51, 53, 67 | 3imtr4g 296 |
1
⊢ (𝐵 ∈ P →
(𝑥 ∈ 𝐶 → ∃𝑧(𝑧 ∈ 𝐶 ∧ 𝑥 <Q 𝑧))) |