Step | Hyp | Ref
| Expression |
1 | | ltsonq 7339 |
. . . . . 6
⊢
<Q Or Q |
2 | | ltrelnq 7306 |
. . . . . 6
⊢
<Q ⊆ (Q ×
Q) |
3 | 1, 2 | son2lpi 5000 |
. . . . 5
⊢ ¬
(𝑦
<Q 𝑧 ∧ 𝑧 <Q 𝑦) |
4 | | ltrelpr 7446 |
. . . . . . . . . . . . . . . 16
⊢
<P ⊆ (P ×
P) |
5 | 4 | brel 4656 |
. . . . . . . . . . . . . . 15
⊢ (𝐴<P
𝐵 → (𝐴 ∈ P ∧ 𝐵 ∈
P)) |
6 | 5 | simprd 113 |
. . . . . . . . . . . . . 14
⊢ (𝐴<P
𝐵 → 𝐵 ∈ P) |
7 | | prop 7416 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈ P →
〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈
P) |
8 | 6, 7 | syl 14 |
. . . . . . . . . . . . 13
⊢ (𝐴<P
𝐵 →
〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈
P) |
9 | | prltlu 7428 |
. . . . . . . . . . . . 13
⊢
((〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈ P ∧ (𝑦 +Q
𝑞) ∈ (1st
‘𝐵) ∧ (𝑧 +Q
𝑞) ∈ (2nd
‘𝐵)) → (𝑦 +Q
𝑞)
<Q (𝑧 +Q 𝑞)) |
10 | 8, 9 | syl3an1 1261 |
. . . . . . . . . . . 12
⊢ ((𝐴<P
𝐵 ∧ (𝑦 +Q 𝑞) ∈ (1st
‘𝐵) ∧ (𝑧 +Q
𝑞) ∈ (2nd
‘𝐵)) → (𝑦 +Q
𝑞)
<Q (𝑧 +Q 𝑞)) |
11 | 10 | 3expb 1194 |
. . . . . . . . . . 11
⊢ ((𝐴<P
𝐵 ∧ ((𝑦 +Q
𝑞) ∈ (1st
‘𝐵) ∧ (𝑧 +Q
𝑞) ∈ (2nd
‘𝐵))) → (𝑦 +Q
𝑞)
<Q (𝑧 +Q 𝑞)) |
12 | 11 | adantlr 469 |
. . . . . . . . . 10
⊢ (((𝐴<P
𝐵 ∧ 𝑞 ∈ Q) ∧ ((𝑦 +Q
𝑞) ∈ (1st
‘𝐵) ∧ (𝑧 +Q
𝑞) ∈ (2nd
‘𝐵))) → (𝑦 +Q
𝑞)
<Q (𝑧 +Q 𝑞)) |
13 | 12 | adantrll 476 |
. . . . . . . . 9
⊢ (((𝐴<P
𝐵 ∧ 𝑞 ∈ Q) ∧ ((𝑦 ∈ (2nd
‘𝐴) ∧ (𝑦 +Q
𝑞) ∈ (1st
‘𝐵)) ∧ (𝑧 +Q
𝑞) ∈ (2nd
‘𝐵))) → (𝑦 +Q
𝑞)
<Q (𝑧 +Q 𝑞)) |
14 | 13 | adantrrl 478 |
. . . . . . . 8
⊢ (((𝐴<P
𝐵 ∧ 𝑞 ∈ Q) ∧ ((𝑦 ∈ (2nd
‘𝐴) ∧ (𝑦 +Q
𝑞) ∈ (1st
‘𝐵)) ∧ (𝑧 ∈ (1st
‘𝐴) ∧ (𝑧 +Q
𝑞) ∈ (2nd
‘𝐵)))) → (𝑦 +Q
𝑞)
<Q (𝑧 +Q 𝑞)) |
15 | | ltanqg 7341 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ Q ∧
𝑔 ∈ Q
∧ ℎ ∈
Q) → (𝑓
<Q 𝑔 ↔ (ℎ +Q 𝑓) <Q
(ℎ
+Q 𝑔))) |
16 | 15 | adantl 275 |
. . . . . . . . 9
⊢ ((((𝐴<P
𝐵 ∧ 𝑞 ∈ Q) ∧ ((𝑦 ∈ (2nd
‘𝐴) ∧ (𝑦 +Q
𝑞) ∈ (1st
‘𝐵)) ∧ (𝑧 ∈ (1st
‘𝐴) ∧ (𝑧 +Q
𝑞) ∈ (2nd
‘𝐵)))) ∧ (𝑓 ∈ Q ∧
𝑔 ∈ Q
∧ ℎ ∈
Q)) → (𝑓
<Q 𝑔 ↔ (ℎ +Q 𝑓) <Q
(ℎ
+Q 𝑔))) |
17 | 5 | simpld 111 |
. . . . . . . . . . . . 13
⊢ (𝐴<P
𝐵 → 𝐴 ∈ P) |
18 | | prop 7416 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ P →
〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈
P) |
19 | 17, 18 | syl 14 |
. . . . . . . . . . . 12
⊢ (𝐴<P
𝐵 →
〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈
P) |
20 | | elprnqu 7423 |
. . . . . . . . . . . 12
⊢
((〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈ P ∧ 𝑦 ∈ (2nd
‘𝐴)) → 𝑦 ∈
Q) |
21 | 19, 20 | sylan 281 |
. . . . . . . . . . 11
⊢ ((𝐴<P
𝐵 ∧ 𝑦 ∈ (2nd ‘𝐴)) → 𝑦 ∈ Q) |
22 | 21 | ad2ant2r 501 |
. . . . . . . . . 10
⊢ (((𝐴<P
𝐵 ∧ 𝑞 ∈ Q) ∧ (𝑦 ∈ (2nd
‘𝐴) ∧ (𝑦 +Q
𝑞) ∈ (1st
‘𝐵))) → 𝑦 ∈
Q) |
23 | 22 | adantrr 471 |
. . . . . . . . 9
⊢ (((𝐴<P
𝐵 ∧ 𝑞 ∈ Q) ∧ ((𝑦 ∈ (2nd
‘𝐴) ∧ (𝑦 +Q
𝑞) ∈ (1st
‘𝐵)) ∧ (𝑧 ∈ (1st
‘𝐴) ∧ (𝑧 +Q
𝑞) ∈ (2nd
‘𝐵)))) → 𝑦 ∈
Q) |
24 | | elprnql 7422 |
. . . . . . . . . . . 12
⊢
((〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈ P ∧ 𝑧 ∈ (1st
‘𝐴)) → 𝑧 ∈
Q) |
25 | 19, 24 | sylan 281 |
. . . . . . . . . . 11
⊢ ((𝐴<P
𝐵 ∧ 𝑧 ∈ (1st ‘𝐴)) → 𝑧 ∈ Q) |
26 | 25 | ad2ant2r 501 |
. . . . . . . . . 10
⊢ (((𝐴<P
𝐵 ∧ 𝑞 ∈ Q) ∧ (𝑧 ∈ (1st
‘𝐴) ∧ (𝑧 +Q
𝑞) ∈ (2nd
‘𝐵))) → 𝑧 ∈
Q) |
27 | 26 | adantrl 470 |
. . . . . . . . 9
⊢ (((𝐴<P
𝐵 ∧ 𝑞 ∈ Q) ∧ ((𝑦 ∈ (2nd
‘𝐴) ∧ (𝑦 +Q
𝑞) ∈ (1st
‘𝐵)) ∧ (𝑧 ∈ (1st
‘𝐴) ∧ (𝑧 +Q
𝑞) ∈ (2nd
‘𝐵)))) → 𝑧 ∈
Q) |
28 | | simplr 520 |
. . . . . . . . 9
⊢ (((𝐴<P
𝐵 ∧ 𝑞 ∈ Q) ∧ ((𝑦 ∈ (2nd
‘𝐴) ∧ (𝑦 +Q
𝑞) ∈ (1st
‘𝐵)) ∧ (𝑧 ∈ (1st
‘𝐴) ∧ (𝑧 +Q
𝑞) ∈ (2nd
‘𝐵)))) → 𝑞 ∈
Q) |
29 | | addcomnqg 7322 |
. . . . . . . . . 10
⊢ ((𝑓 ∈ Q ∧
𝑔 ∈ Q)
→ (𝑓
+Q 𝑔) = (𝑔 +Q 𝑓)) |
30 | 29 | adantl 275 |
. . . . . . . . 9
⊢ ((((𝐴<P
𝐵 ∧ 𝑞 ∈ Q) ∧ ((𝑦 ∈ (2nd
‘𝐴) ∧ (𝑦 +Q
𝑞) ∈ (1st
‘𝐵)) ∧ (𝑧 ∈ (1st
‘𝐴) ∧ (𝑧 +Q
𝑞) ∈ (2nd
‘𝐵)))) ∧ (𝑓 ∈ Q ∧
𝑔 ∈ Q))
→ (𝑓
+Q 𝑔) = (𝑔 +Q 𝑓)) |
31 | 16, 23, 27, 28, 30 | caovord2d 6011 |
. . . . . . . 8
⊢ (((𝐴<P
𝐵 ∧ 𝑞 ∈ Q) ∧ ((𝑦 ∈ (2nd
‘𝐴) ∧ (𝑦 +Q
𝑞) ∈ (1st
‘𝐵)) ∧ (𝑧 ∈ (1st
‘𝐴) ∧ (𝑧 +Q
𝑞) ∈ (2nd
‘𝐵)))) → (𝑦 <Q
𝑧 ↔ (𝑦 +Q
𝑞)
<Q (𝑧 +Q 𝑞))) |
32 | 14, 31 | mpbird 166 |
. . . . . . 7
⊢ (((𝐴<P
𝐵 ∧ 𝑞 ∈ Q) ∧ ((𝑦 ∈ (2nd
‘𝐴) ∧ (𝑦 +Q
𝑞) ∈ (1st
‘𝐵)) ∧ (𝑧 ∈ (1st
‘𝐴) ∧ (𝑧 +Q
𝑞) ∈ (2nd
‘𝐵)))) → 𝑦 <Q
𝑧) |
33 | | prltlu 7428 |
. . . . . . . . . . . . 13
⊢
((〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈ P ∧ 𝑧 ∈ (1st
‘𝐴) ∧ 𝑦 ∈ (2nd
‘𝐴)) → 𝑧 <Q
𝑦) |
34 | 19, 33 | syl3an1 1261 |
. . . . . . . . . . . 12
⊢ ((𝐴<P
𝐵 ∧ 𝑧 ∈ (1st ‘𝐴) ∧ 𝑦 ∈ (2nd ‘𝐴)) → 𝑧 <Q 𝑦) |
35 | 34 | 3com23 1199 |
. . . . . . . . . . 11
⊢ ((𝐴<P
𝐵 ∧ 𝑦 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (1st ‘𝐴)) → 𝑧 <Q 𝑦) |
36 | 35 | 3expb 1194 |
. . . . . . . . . 10
⊢ ((𝐴<P
𝐵 ∧ (𝑦 ∈ (2nd ‘𝐴) ∧ 𝑧 ∈ (1st ‘𝐴))) → 𝑧 <Q 𝑦) |
37 | 36 | adantlr 469 |
. . . . . . . . 9
⊢ (((𝐴<P
𝐵 ∧ 𝑞 ∈ Q) ∧ (𝑦 ∈ (2nd
‘𝐴) ∧ 𝑧 ∈ (1st
‘𝐴))) → 𝑧 <Q
𝑦) |
38 | 37 | adantrlr 477 |
. . . . . . . 8
⊢ (((𝐴<P
𝐵 ∧ 𝑞 ∈ Q) ∧ ((𝑦 ∈ (2nd
‘𝐴) ∧ (𝑦 +Q
𝑞) ∈ (1st
‘𝐵)) ∧ 𝑧 ∈ (1st
‘𝐴))) → 𝑧 <Q
𝑦) |
39 | 38 | adantrrr 479 |
. . . . . . 7
⊢ (((𝐴<P
𝐵 ∧ 𝑞 ∈ Q) ∧ ((𝑦 ∈ (2nd
‘𝐴) ∧ (𝑦 +Q
𝑞) ∈ (1st
‘𝐵)) ∧ (𝑧 ∈ (1st
‘𝐴) ∧ (𝑧 +Q
𝑞) ∈ (2nd
‘𝐵)))) → 𝑧 <Q
𝑦) |
40 | 32, 39 | jca 304 |
. . . . . 6
⊢ (((𝐴<P
𝐵 ∧ 𝑞 ∈ Q) ∧ ((𝑦 ∈ (2nd
‘𝐴) ∧ (𝑦 +Q
𝑞) ∈ (1st
‘𝐵)) ∧ (𝑧 ∈ (1st
‘𝐴) ∧ (𝑧 +Q
𝑞) ∈ (2nd
‘𝐵)))) → (𝑦 <Q
𝑧 ∧ 𝑧 <Q 𝑦)) |
41 | 40 | ex 114 |
. . . . 5
⊢ ((𝐴<P
𝐵 ∧ 𝑞 ∈ Q) → (((𝑦 ∈ (2nd
‘𝐴) ∧ (𝑦 +Q
𝑞) ∈ (1st
‘𝐵)) ∧ (𝑧 ∈ (1st
‘𝐴) ∧ (𝑧 +Q
𝑞) ∈ (2nd
‘𝐵))) → (𝑦 <Q
𝑧 ∧ 𝑧 <Q 𝑦))) |
42 | 3, 41 | mtoi 654 |
. . . 4
⊢ ((𝐴<P
𝐵 ∧ 𝑞 ∈ Q) → ¬ ((𝑦 ∈ (2nd
‘𝐴) ∧ (𝑦 +Q
𝑞) ∈ (1st
‘𝐵)) ∧ (𝑧 ∈ (1st
‘𝐴) ∧ (𝑧 +Q
𝑞) ∈ (2nd
‘𝐵)))) |
43 | 42 | alrimivv 1863 |
. . 3
⊢ ((𝐴<P
𝐵 ∧ 𝑞 ∈ Q) → ∀𝑦∀𝑧 ¬ ((𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑞) ∈ (1st
‘𝐵)) ∧ (𝑧 ∈ (1st
‘𝐴) ∧ (𝑧 +Q
𝑞) ∈ (2nd
‘𝐵)))) |
44 | | ltexprlem.1 |
. . . . . . . . . . . 12
⊢ 𝐶 = 〈{𝑥 ∈ Q ∣ ∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (1st
‘𝐵))}, {𝑥 ∈ Q ∣
∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑥) ∈ (2nd
‘𝐵))}〉 |
45 | 44 | ltexprlemell 7539 |
. . . . . . . . . . 11
⊢ (𝑞 ∈ (1st
‘𝐶) ↔ (𝑞 ∈ Q ∧
∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑞) ∈ (1st
‘𝐵)))) |
46 | 44 | ltexprlemelu 7540 |
. . . . . . . . . . 11
⊢ (𝑞 ∈ (2nd
‘𝐶) ↔ (𝑞 ∈ Q ∧
∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑞) ∈ (2nd
‘𝐵)))) |
47 | 45, 46 | anbi12i 456 |
. . . . . . . . . 10
⊢ ((𝑞 ∈ (1st
‘𝐶) ∧ 𝑞 ∈ (2nd
‘𝐶)) ↔ ((𝑞 ∈ Q ∧
∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑞) ∈ (1st
‘𝐵))) ∧ (𝑞 ∈ Q ∧
∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑞) ∈ (2nd
‘𝐵))))) |
48 | | anandi 580 |
. . . . . . . . . 10
⊢ ((𝑞 ∈ Q ∧
(∃𝑦(𝑦 ∈ (2nd
‘𝐴) ∧ (𝑦 +Q
𝑞) ∈ (1st
‘𝐵)) ∧
∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑞) ∈ (2nd
‘𝐵)))) ↔ ((𝑞 ∈ Q ∧
∃𝑦(𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑞) ∈ (1st
‘𝐵))) ∧ (𝑞 ∈ Q ∧
∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑞) ∈ (2nd
‘𝐵))))) |
49 | 47, 48 | bitr4i 186 |
. . . . . . . . 9
⊢ ((𝑞 ∈ (1st
‘𝐶) ∧ 𝑞 ∈ (2nd
‘𝐶)) ↔ (𝑞 ∈ Q ∧
(∃𝑦(𝑦 ∈ (2nd
‘𝐴) ∧ (𝑦 +Q
𝑞) ∈ (1st
‘𝐵)) ∧
∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑞) ∈ (2nd
‘𝐵))))) |
50 | 49 | baib 909 |
. . . . . . . 8
⊢ (𝑞 ∈ Q →
((𝑞 ∈ (1st
‘𝐶) ∧ 𝑞 ∈ (2nd
‘𝐶)) ↔
(∃𝑦(𝑦 ∈ (2nd
‘𝐴) ∧ (𝑦 +Q
𝑞) ∈ (1st
‘𝐵)) ∧
∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑞) ∈ (2nd
‘𝐵))))) |
51 | | eleq1 2229 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑧 → (𝑦 ∈ (1st ‘𝐴) ↔ 𝑧 ∈ (1st ‘𝐴))) |
52 | | oveq1 5849 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑧 → (𝑦 +Q 𝑞) = (𝑧 +Q 𝑞)) |
53 | 52 | eleq1d 2235 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑧 → ((𝑦 +Q 𝑞) ∈ (2nd
‘𝐵) ↔ (𝑧 +Q
𝑞) ∈ (2nd
‘𝐵))) |
54 | 51, 53 | anbi12d 465 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑧 → ((𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑞) ∈ (2nd
‘𝐵)) ↔ (𝑧 ∈ (1st
‘𝐴) ∧ (𝑧 +Q
𝑞) ∈ (2nd
‘𝐵)))) |
55 | 54 | cbvexv 1906 |
. . . . . . . . 9
⊢
(∃𝑦(𝑦 ∈ (1st
‘𝐴) ∧ (𝑦 +Q
𝑞) ∈ (2nd
‘𝐵)) ↔
∃𝑧(𝑧 ∈ (1st ‘𝐴) ∧ (𝑧 +Q 𝑞) ∈ (2nd
‘𝐵))) |
56 | 55 | anbi2i 453 |
. . . . . . . 8
⊢
((∃𝑦(𝑦 ∈ (2nd
‘𝐴) ∧ (𝑦 +Q
𝑞) ∈ (1st
‘𝐵)) ∧
∃𝑦(𝑦 ∈ (1st ‘𝐴) ∧ (𝑦 +Q 𝑞) ∈ (2nd
‘𝐵))) ↔
(∃𝑦(𝑦 ∈ (2nd
‘𝐴) ∧ (𝑦 +Q
𝑞) ∈ (1st
‘𝐵)) ∧
∃𝑧(𝑧 ∈ (1st ‘𝐴) ∧ (𝑧 +Q 𝑞) ∈ (2nd
‘𝐵)))) |
57 | 50, 56 | bitrdi 195 |
. . . . . . 7
⊢ (𝑞 ∈ Q →
((𝑞 ∈ (1st
‘𝐶) ∧ 𝑞 ∈ (2nd
‘𝐶)) ↔
(∃𝑦(𝑦 ∈ (2nd
‘𝐴) ∧ (𝑦 +Q
𝑞) ∈ (1st
‘𝐵)) ∧
∃𝑧(𝑧 ∈ (1st ‘𝐴) ∧ (𝑧 +Q 𝑞) ∈ (2nd
‘𝐵))))) |
58 | | eeanv 1920 |
. . . . . . 7
⊢
(∃𝑦∃𝑧((𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑞) ∈ (1st
‘𝐵)) ∧ (𝑧 ∈ (1st
‘𝐴) ∧ (𝑧 +Q
𝑞) ∈ (2nd
‘𝐵))) ↔
(∃𝑦(𝑦 ∈ (2nd
‘𝐴) ∧ (𝑦 +Q
𝑞) ∈ (1st
‘𝐵)) ∧
∃𝑧(𝑧 ∈ (1st ‘𝐴) ∧ (𝑧 +Q 𝑞) ∈ (2nd
‘𝐵)))) |
59 | 57, 58 | bitr4di 197 |
. . . . . 6
⊢ (𝑞 ∈ Q →
((𝑞 ∈ (1st
‘𝐶) ∧ 𝑞 ∈ (2nd
‘𝐶)) ↔
∃𝑦∃𝑧((𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑞) ∈ (1st
‘𝐵)) ∧ (𝑧 ∈ (1st
‘𝐴) ∧ (𝑧 +Q
𝑞) ∈ (2nd
‘𝐵))))) |
60 | 59 | notbid 657 |
. . . . 5
⊢ (𝑞 ∈ Q →
(¬ (𝑞 ∈
(1st ‘𝐶)
∧ 𝑞 ∈
(2nd ‘𝐶))
↔ ¬ ∃𝑦∃𝑧((𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑞) ∈ (1st
‘𝐵)) ∧ (𝑧 ∈ (1st
‘𝐴) ∧ (𝑧 +Q
𝑞) ∈ (2nd
‘𝐵))))) |
61 | | alnex 1487 |
. . . . . . 7
⊢
(∀𝑧 ¬
((𝑦 ∈ (2nd
‘𝐴) ∧ (𝑦 +Q
𝑞) ∈ (1st
‘𝐵)) ∧ (𝑧 ∈ (1st
‘𝐴) ∧ (𝑧 +Q
𝑞) ∈ (2nd
‘𝐵))) ↔ ¬
∃𝑧((𝑦 ∈ (2nd
‘𝐴) ∧ (𝑦 +Q
𝑞) ∈ (1st
‘𝐵)) ∧ (𝑧 ∈ (1st
‘𝐴) ∧ (𝑧 +Q
𝑞) ∈ (2nd
‘𝐵)))) |
62 | 61 | albii 1458 |
. . . . . 6
⊢
(∀𝑦∀𝑧 ¬ ((𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑞) ∈ (1st
‘𝐵)) ∧ (𝑧 ∈ (1st
‘𝐴) ∧ (𝑧 +Q
𝑞) ∈ (2nd
‘𝐵))) ↔
∀𝑦 ¬
∃𝑧((𝑦 ∈ (2nd
‘𝐴) ∧ (𝑦 +Q
𝑞) ∈ (1st
‘𝐵)) ∧ (𝑧 ∈ (1st
‘𝐴) ∧ (𝑧 +Q
𝑞) ∈ (2nd
‘𝐵)))) |
63 | | alnex 1487 |
. . . . . 6
⊢
(∀𝑦 ¬
∃𝑧((𝑦 ∈ (2nd
‘𝐴) ∧ (𝑦 +Q
𝑞) ∈ (1st
‘𝐵)) ∧ (𝑧 ∈ (1st
‘𝐴) ∧ (𝑧 +Q
𝑞) ∈ (2nd
‘𝐵))) ↔ ¬
∃𝑦∃𝑧((𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑞) ∈ (1st
‘𝐵)) ∧ (𝑧 ∈ (1st
‘𝐴) ∧ (𝑧 +Q
𝑞) ∈ (2nd
‘𝐵)))) |
64 | 62, 63 | bitri 183 |
. . . . 5
⊢
(∀𝑦∀𝑧 ¬ ((𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑞) ∈ (1st
‘𝐵)) ∧ (𝑧 ∈ (1st
‘𝐴) ∧ (𝑧 +Q
𝑞) ∈ (2nd
‘𝐵))) ↔ ¬
∃𝑦∃𝑧((𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑞) ∈ (1st
‘𝐵)) ∧ (𝑧 ∈ (1st
‘𝐴) ∧ (𝑧 +Q
𝑞) ∈ (2nd
‘𝐵)))) |
65 | 60, 64 | bitr4di 197 |
. . . 4
⊢ (𝑞 ∈ Q →
(¬ (𝑞 ∈
(1st ‘𝐶)
∧ 𝑞 ∈
(2nd ‘𝐶))
↔ ∀𝑦∀𝑧 ¬ ((𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑞) ∈ (1st
‘𝐵)) ∧ (𝑧 ∈ (1st
‘𝐴) ∧ (𝑧 +Q
𝑞) ∈ (2nd
‘𝐵))))) |
66 | 65 | adantl 275 |
. . 3
⊢ ((𝐴<P
𝐵 ∧ 𝑞 ∈ Q) → (¬ (𝑞 ∈ (1st
‘𝐶) ∧ 𝑞 ∈ (2nd
‘𝐶)) ↔
∀𝑦∀𝑧 ¬ ((𝑦 ∈ (2nd ‘𝐴) ∧ (𝑦 +Q 𝑞) ∈ (1st
‘𝐵)) ∧ (𝑧 ∈ (1st
‘𝐴) ∧ (𝑧 +Q
𝑞) ∈ (2nd
‘𝐵))))) |
67 | 43, 66 | mpbird 166 |
. 2
⊢ ((𝐴<P
𝐵 ∧ 𝑞 ∈ Q) → ¬ (𝑞 ∈ (1st
‘𝐶) ∧ 𝑞 ∈ (2nd
‘𝐶))) |
68 | 67 | ralrimiva 2539 |
1
⊢ (𝐴<P
𝐵 → ∀𝑞 ∈ Q ¬
(𝑞 ∈ (1st
‘𝐶) ∧ 𝑞 ∈ (2nd
‘𝐶))) |