| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | prnmax 11036 | . . . . . . . . 9
⊢ ((𝐵 ∈ P ∧
(𝑦
+Q 𝑥) ∈ 𝐵) → ∃𝑤 ∈ 𝐵 (𝑦 +Q 𝑥) <Q
𝑤) | 
| 2 |  | df-rex 3070 | . . . . . . . . 9
⊢
(∃𝑤 ∈
𝐵 (𝑦 +Q 𝑥) <Q
𝑤 ↔ ∃𝑤(𝑤 ∈ 𝐵 ∧ (𝑦 +Q 𝑥) <Q
𝑤)) | 
| 3 | 1, 2 | sylib 218 | . . . . . . . 8
⊢ ((𝐵 ∈ P ∧
(𝑦
+Q 𝑥) ∈ 𝐵) → ∃𝑤(𝑤 ∈ 𝐵 ∧ (𝑦 +Q 𝑥) <Q
𝑤)) | 
| 4 |  | ltrelnq 10967 | . . . . . . . . . . . . . . . . . . . 20
⊢ 
<Q ⊆ (Q ×
Q) | 
| 5 | 4 | brel 5749 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 +Q
𝑥)
<Q 𝑤 → ((𝑦 +Q 𝑥) ∈ Q ∧
𝑤 ∈
Q)) | 
| 6 | 5 | simpld 494 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 +Q
𝑥)
<Q 𝑤 → (𝑦 +Q 𝑥) ∈
Q) | 
| 7 |  | addnqf 10989 | . . . . . . . . . . . . . . . . . . . 20
⊢ 
+Q :(Q ×
Q)⟶Q | 
| 8 | 7 | fdmi 6746 | . . . . . . . . . . . . . . . . . . 19
⊢ dom
+Q = (Q ×
Q) | 
| 9 |  | 0nnq 10965 | . . . . . . . . . . . . . . . . . . 19
⊢  ¬
∅ ∈ Q | 
| 10 | 8, 9 | ndmovrcl 7620 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 +Q
𝑥) ∈ Q
→ (𝑦 ∈
Q ∧ 𝑥
∈ Q)) | 
| 11 | 6, 10 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑦 +Q
𝑥)
<Q 𝑤 → (𝑦 ∈ Q ∧ 𝑥 ∈
Q)) | 
| 12 |  | ltaddnq 11015 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 ∈ Q ∧
𝑥 ∈ Q)
→ 𝑦
<Q (𝑦 +Q 𝑥)) | 
| 13 |  | ltsonq 11010 | . . . . . . . . . . . . . . . . . . 19
⊢ 
<Q Or Q | 
| 14 | 13, 4 | sotri 6146 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑦 <Q
(𝑦
+Q 𝑥) ∧ (𝑦 +Q 𝑥) <Q
𝑤) → 𝑦 <Q
𝑤) | 
| 15 | 12, 14 | sylan 580 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑦 ∈ Q ∧
𝑥 ∈ Q)
∧ (𝑦
+Q 𝑥) <Q 𝑤) → 𝑦 <Q 𝑤) | 
| 16 | 11, 15 | mpancom 688 | . . . . . . . . . . . . . . . 16
⊢ ((𝑦 +Q
𝑥)
<Q 𝑤 → 𝑦 <Q 𝑤) | 
| 17 | 4 | brel 5749 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑦 <Q
𝑤 → (𝑦 ∈ Q ∧
𝑤 ∈
Q)) | 
| 18 | 17 | simprd 495 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 <Q
𝑤 → 𝑤 ∈ Q) | 
| 19 |  | ltexnq 11016 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ Q →
(𝑦
<Q 𝑤 ↔ ∃𝑧(𝑦 +Q 𝑧) = 𝑤)) | 
| 20 | 19 | biimpd 229 | . . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ Q →
(𝑦
<Q 𝑤 → ∃𝑧(𝑦 +Q 𝑧) = 𝑤)) | 
| 21 | 18, 20 | mpcom 38 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 <Q
𝑤 → ∃𝑧(𝑦 +Q 𝑧) = 𝑤) | 
| 22 | 16, 21 | syl 17 | . . . . . . . . . . . . . . 15
⊢ ((𝑦 +Q
𝑥)
<Q 𝑤 → ∃𝑧(𝑦 +Q 𝑧) = 𝑤) | 
| 23 |  | eqcom 2743 | . . . . . . . . . . . . . . . 16
⊢ (𝑤 = (𝑦 +Q 𝑧) ↔ (𝑦 +Q 𝑧) = 𝑤) | 
| 24 | 23 | exbii 1847 | . . . . . . . . . . . . . . 15
⊢
(∃𝑧 𝑤 = (𝑦 +Q 𝑧) ↔ ∃𝑧(𝑦 +Q 𝑧) = 𝑤) | 
| 25 | 22, 24 | sylibr 234 | . . . . . . . . . . . . . 14
⊢ ((𝑦 +Q
𝑥)
<Q 𝑤 → ∃𝑧 𝑤 = (𝑦 +Q 𝑧)) | 
| 26 | 25 | ancri 549 | . . . . . . . . . . . . 13
⊢ ((𝑦 +Q
𝑥)
<Q 𝑤 → (∃𝑧 𝑤 = (𝑦 +Q 𝑧) ∧ (𝑦 +Q 𝑥) <Q
𝑤)) | 
| 27 | 26 | anim2i 617 | . . . . . . . . . . . 12
⊢ ((𝑤 ∈ 𝐵 ∧ (𝑦 +Q 𝑥) <Q
𝑤) → (𝑤 ∈ 𝐵 ∧ (∃𝑧 𝑤 = (𝑦 +Q 𝑧) ∧ (𝑦 +Q 𝑥) <Q
𝑤))) | 
| 28 |  | an12 645 | . . . . . . . . . . . 12
⊢
((∃𝑧 𝑤 = (𝑦 +Q 𝑧) ∧ (𝑤 ∈ 𝐵 ∧ (𝑦 +Q 𝑥) <Q
𝑤)) ↔ (𝑤 ∈ 𝐵 ∧ (∃𝑧 𝑤 = (𝑦 +Q 𝑧) ∧ (𝑦 +Q 𝑥) <Q
𝑤))) | 
| 29 | 27, 28 | sylibr 234 | . . . . . . . . . . 11
⊢ ((𝑤 ∈ 𝐵 ∧ (𝑦 +Q 𝑥) <Q
𝑤) → (∃𝑧 𝑤 = (𝑦 +Q 𝑧) ∧ (𝑤 ∈ 𝐵 ∧ (𝑦 +Q 𝑥) <Q
𝑤))) | 
| 30 |  | 19.41v 1948 | . . . . . . . . . . 11
⊢
(∃𝑧(𝑤 = (𝑦 +Q 𝑧) ∧ (𝑤 ∈ 𝐵 ∧ (𝑦 +Q 𝑥) <Q
𝑤)) ↔ (∃𝑧 𝑤 = (𝑦 +Q 𝑧) ∧ (𝑤 ∈ 𝐵 ∧ (𝑦 +Q 𝑥) <Q
𝑤))) | 
| 31 | 29, 30 | sylibr 234 | . . . . . . . . . 10
⊢ ((𝑤 ∈ 𝐵 ∧ (𝑦 +Q 𝑥) <Q
𝑤) → ∃𝑧(𝑤 = (𝑦 +Q 𝑧) ∧ (𝑤 ∈ 𝐵 ∧ (𝑦 +Q 𝑥) <Q
𝑤))) | 
| 32 | 31 | eximi 1834 | . . . . . . . . 9
⊢
(∃𝑤(𝑤 ∈ 𝐵 ∧ (𝑦 +Q 𝑥) <Q
𝑤) → ∃𝑤∃𝑧(𝑤 = (𝑦 +Q 𝑧) ∧ (𝑤 ∈ 𝐵 ∧ (𝑦 +Q 𝑥) <Q
𝑤))) | 
| 33 |  | excom 2161 | . . . . . . . . 9
⊢
(∃𝑧∃𝑤(𝑤 = (𝑦 +Q 𝑧) ∧ (𝑤 ∈ 𝐵 ∧ (𝑦 +Q 𝑥) <Q
𝑤)) ↔ ∃𝑤∃𝑧(𝑤 = (𝑦 +Q 𝑧) ∧ (𝑤 ∈ 𝐵 ∧ (𝑦 +Q 𝑥) <Q
𝑤))) | 
| 34 | 32, 33 | sylibr 234 | . . . . . . . 8
⊢
(∃𝑤(𝑤 ∈ 𝐵 ∧ (𝑦 +Q 𝑥) <Q
𝑤) → ∃𝑧∃𝑤(𝑤 = (𝑦 +Q 𝑧) ∧ (𝑤 ∈ 𝐵 ∧ (𝑦 +Q 𝑥) <Q
𝑤))) | 
| 35 |  | ovex 7465 | . . . . . . . . . . 11
⊢ (𝑦 +Q
𝑧) ∈
V | 
| 36 |  | eleq1 2828 | . . . . . . . . . . . 12
⊢ (𝑤 = (𝑦 +Q 𝑧) → (𝑤 ∈ 𝐵 ↔ (𝑦 +Q 𝑧) ∈ 𝐵)) | 
| 37 |  | breq2 5146 | . . . . . . . . . . . 12
⊢ (𝑤 = (𝑦 +Q 𝑧) → ((𝑦 +Q 𝑥) <Q
𝑤 ↔ (𝑦 +Q
𝑥)
<Q (𝑦 +Q 𝑧))) | 
| 38 | 36, 37 | anbi12d 632 | . . . . . . . . . . 11
⊢ (𝑤 = (𝑦 +Q 𝑧) → ((𝑤 ∈ 𝐵 ∧ (𝑦 +Q 𝑥) <Q
𝑤) ↔ ((𝑦 +Q
𝑧) ∈ 𝐵 ∧ (𝑦 +Q 𝑥) <Q
(𝑦
+Q 𝑧)))) | 
| 39 | 35, 38 | ceqsexv 3531 | . . . . . . . . . 10
⊢
(∃𝑤(𝑤 = (𝑦 +Q 𝑧) ∧ (𝑤 ∈ 𝐵 ∧ (𝑦 +Q 𝑥) <Q
𝑤)) ↔ ((𝑦 +Q
𝑧) ∈ 𝐵 ∧ (𝑦 +Q 𝑥) <Q
(𝑦
+Q 𝑧))) | 
| 40 |  | ltanq 11012 | . . . . . . . . . . . 12
⊢ (𝑦 ∈ Q →
(𝑥
<Q 𝑧 ↔ (𝑦 +Q 𝑥) <Q
(𝑦
+Q 𝑧))) | 
| 41 | 8, 4, 9, 40 | ndmovordi 7625 | . . . . . . . . . . 11
⊢ ((𝑦 +Q
𝑥)
<Q (𝑦 +Q 𝑧) → 𝑥 <Q 𝑧) | 
| 42 | 41 | anim2i 617 | . . . . . . . . . 10
⊢ (((𝑦 +Q
𝑧) ∈ 𝐵 ∧ (𝑦 +Q 𝑥) <Q
(𝑦
+Q 𝑧)) → ((𝑦 +Q 𝑧) ∈ 𝐵 ∧ 𝑥 <Q 𝑧)) | 
| 43 | 39, 42 | sylbi 217 | . . . . . . . . 9
⊢
(∃𝑤(𝑤 = (𝑦 +Q 𝑧) ∧ (𝑤 ∈ 𝐵 ∧ (𝑦 +Q 𝑥) <Q
𝑤)) → ((𝑦 +Q
𝑧) ∈ 𝐵 ∧ 𝑥 <Q 𝑧)) | 
| 44 | 43 | eximi 1834 | . . . . . . . 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 649 | . . . . 5
⊢ ((𝐵 ∈ P ∧
(¬ 𝑦 ∈ 𝐴 ∧ (𝑦 +Q 𝑥) ∈ 𝐵)) → (¬ 𝑦 ∈ 𝐴 ∧ ∃𝑧((𝑦 +Q 𝑧) ∈ 𝐵 ∧ 𝑥 <Q 𝑧))) | 
| 48 |  | 19.42v 1952 | . . . . 5
⊢
(∃𝑧(¬
𝑦 ∈ 𝐴 ∧ ((𝑦 +Q 𝑧) ∈ 𝐵 ∧ 𝑥 <Q 𝑧)) ↔ (¬ 𝑦 ∈ 𝐴 ∧ ∃𝑧((𝑦 +Q 𝑧) ∈ 𝐵 ∧ 𝑥 <Q 𝑧))) | 
| 49 | 47, 48 | sylibr 234 | . . . 4
⊢ ((𝐵 ∈ P ∧
(¬ 𝑦 ∈ 𝐴 ∧ (𝑦 +Q 𝑥) ∈ 𝐵)) → ∃𝑧(¬ 𝑦 ∈ 𝐴 ∧ ((𝑦 +Q 𝑧) ∈ 𝐵 ∧ 𝑥 <Q 𝑧))) | 
| 50 | 49 | ex 412 | . . 3
⊢ (𝐵 ∈ P →
((¬ 𝑦 ∈ 𝐴 ∧ (𝑦 +Q 𝑥) ∈ 𝐵) → ∃𝑧(¬ 𝑦 ∈ 𝐴 ∧ ((𝑦 +Q 𝑧) ∈ 𝐵 ∧ 𝑥 <Q 𝑧)))) | 
| 51 | 50 | eximdv 1916 | . 2
⊢ (𝐵 ∈ P →
(∃𝑦(¬ 𝑦 ∈ 𝐴 ∧ (𝑦 +Q 𝑥) ∈ 𝐵) → ∃𝑦∃𝑧(¬ 𝑦 ∈ 𝐴 ∧ ((𝑦 +Q 𝑧) ∈ 𝐵 ∧ 𝑥 <Q 𝑧)))) | 
| 52 |  | ltexprlem.1 | . . 3
⊢ 𝐶 = {𝑥 ∣ ∃𝑦(¬ 𝑦 ∈ 𝐴 ∧ (𝑦 +Q 𝑥) ∈ 𝐵)} | 
| 53 | 52 | eqabri 2884 | . 2
⊢ (𝑥 ∈ 𝐶 ↔ ∃𝑦(¬ 𝑦 ∈ 𝐴 ∧ (𝑦 +Q 𝑥) ∈ 𝐵)) | 
| 54 |  | vex 3483 | . . . . . . 7
⊢ 𝑧 ∈ V | 
| 55 |  | oveq2 7440 | . . . . . . . . . 10
⊢ (𝑥 = 𝑧 → (𝑦 +Q 𝑥) = (𝑦 +Q 𝑧)) | 
| 56 | 55 | eleq1d 2825 | . . . . . . . . 9
⊢ (𝑥 = 𝑧 → ((𝑦 +Q 𝑥) ∈ 𝐵 ↔ (𝑦 +Q 𝑧) ∈ 𝐵)) | 
| 57 | 56 | anbi2d 630 | . . . . . . . 8
⊢ (𝑥 = 𝑧 → ((¬ 𝑦 ∈ 𝐴 ∧ (𝑦 +Q 𝑥) ∈ 𝐵) ↔ (¬ 𝑦 ∈ 𝐴 ∧ (𝑦 +Q 𝑧) ∈ 𝐵))) | 
| 58 | 57 | exbidv 1920 | . . . . . . 7
⊢ (𝑥 = 𝑧 → (∃𝑦(¬ 𝑦 ∈ 𝐴 ∧ (𝑦 +Q 𝑥) ∈ 𝐵) ↔ ∃𝑦(¬ 𝑦 ∈ 𝐴 ∧ (𝑦 +Q 𝑧) ∈ 𝐵))) | 
| 59 | 54, 58, 52 | elab2 3681 | . . . . . 6
⊢ (𝑧 ∈ 𝐶 ↔ ∃𝑦(¬ 𝑦 ∈ 𝐴 ∧ (𝑦 +Q 𝑧) ∈ 𝐵)) | 
| 60 | 59 | anbi1i 624 | . . . . 5
⊢ ((𝑧 ∈ 𝐶 ∧ 𝑥 <Q 𝑧) ↔ (∃𝑦(¬ 𝑦 ∈ 𝐴 ∧ (𝑦 +Q 𝑧) ∈ 𝐵) ∧ 𝑥 <Q 𝑧)) | 
| 61 |  | 19.41v 1948 | . . . . 5
⊢
(∃𝑦((¬
𝑦 ∈ 𝐴 ∧ (𝑦 +Q 𝑧) ∈ 𝐵) ∧ 𝑥 <Q 𝑧) ↔ (∃𝑦(¬ 𝑦 ∈ 𝐴 ∧ (𝑦 +Q 𝑧) ∈ 𝐵) ∧ 𝑥 <Q 𝑧)) | 
| 62 |  | anass 468 | . . . . . 6
⊢ (((¬
𝑦 ∈ 𝐴 ∧ (𝑦 +Q 𝑧) ∈ 𝐵) ∧ 𝑥 <Q 𝑧) ↔ (¬ 𝑦 ∈ 𝐴 ∧ ((𝑦 +Q 𝑧) ∈ 𝐵 ∧ 𝑥 <Q 𝑧))) | 
| 63 | 62 | exbii 1847 | . . . . 5
⊢
(∃𝑦((¬
𝑦 ∈ 𝐴 ∧ (𝑦 +Q 𝑧) ∈ 𝐵) ∧ 𝑥 <Q 𝑧) ↔ ∃𝑦(¬ 𝑦 ∈ 𝐴 ∧ ((𝑦 +Q 𝑧) ∈ 𝐵 ∧ 𝑥 <Q 𝑧))) | 
| 64 | 60, 61, 63 | 3bitr2i 299 | . . . 4
⊢ ((𝑧 ∈ 𝐶 ∧ 𝑥 <Q 𝑧) ↔ ∃𝑦(¬ 𝑦 ∈ 𝐴 ∧ ((𝑦 +Q 𝑧) ∈ 𝐵 ∧ 𝑥 <Q 𝑧))) | 
| 65 | 64 | exbii 1847 | . . 3
⊢
(∃𝑧(𝑧 ∈ 𝐶 ∧ 𝑥 <Q 𝑧) ↔ ∃𝑧∃𝑦(¬ 𝑦 ∈ 𝐴 ∧ ((𝑦 +Q 𝑧) ∈ 𝐵 ∧ 𝑥 <Q 𝑧))) | 
| 66 |  | excom 2161 | . . 3
⊢
(∃𝑦∃𝑧(¬ 𝑦 ∈ 𝐴 ∧ ((𝑦 +Q 𝑧) ∈ 𝐵 ∧ 𝑥 <Q 𝑧)) ↔ ∃𝑧∃𝑦(¬ 𝑦 ∈ 𝐴 ∧ ((𝑦 +Q 𝑧) ∈ 𝐵 ∧ 𝑥 <Q 𝑧))) | 
| 67 | 65, 66 | bitr4i 278 | . 2
⊢
(∃𝑧(𝑧 ∈ 𝐶 ∧ 𝑥 <Q 𝑧) ↔ ∃𝑦∃𝑧(¬ 𝑦 ∈ 𝐴 ∧ ((𝑦 +Q 𝑧) ∈ 𝐵 ∧ 𝑥 <Q 𝑧))) | 
| 68 | 51, 53, 67 | 3imtr4g 296 | 1
⊢ (𝐵 ∈ P →
(𝑥 ∈ 𝐶 → ∃𝑧(𝑧 ∈ 𝐶 ∧ 𝑥 <Q 𝑧))) |