Step | Hyp | Ref
| Expression |
1 | | prop 7424 |
. . . . . . . 8
⊢ (𝑠 ∈ P →
〈(1st ‘𝑠), (2nd ‘𝑠)〉 ∈
P) |
2 | | prdisj 7441 |
. . . . . . . 8
⊢
((〈(1st ‘𝑠), (2nd ‘𝑠)〉 ∈ P ∧ 𝑞 ∈ Q) →
¬ (𝑞 ∈
(1st ‘𝑠)
∧ 𝑞 ∈
(2nd ‘𝑠))) |
3 | 1, 2 | sylan 281 |
. . . . . . 7
⊢ ((𝑠 ∈ P ∧
𝑞 ∈ Q)
→ ¬ (𝑞 ∈
(1st ‘𝑠)
∧ 𝑞 ∈
(2nd ‘𝑠))) |
4 | | ancom 264 |
. . . . . . 7
⊢ ((𝑞 ∈ (1st
‘𝑠) ∧ 𝑞 ∈ (2nd
‘𝑠)) ↔ (𝑞 ∈ (2nd
‘𝑠) ∧ 𝑞 ∈ (1st
‘𝑠))) |
5 | 3, 4 | sylnib 671 |
. . . . . 6
⊢ ((𝑠 ∈ P ∧
𝑞 ∈ Q)
→ ¬ (𝑞 ∈
(2nd ‘𝑠)
∧ 𝑞 ∈
(1st ‘𝑠))) |
6 | 5 | nrexdv 2563 |
. . . . 5
⊢ (𝑠 ∈ P →
¬ ∃𝑞 ∈
Q (𝑞 ∈
(2nd ‘𝑠)
∧ 𝑞 ∈
(1st ‘𝑠))) |
7 | | ltdfpr 7455 |
. . . . . 6
⊢ ((𝑠 ∈ P ∧
𝑠 ∈ P)
→ (𝑠<P 𝑠 ↔ ∃𝑞 ∈ Q (𝑞 ∈ (2nd
‘𝑠) ∧ 𝑞 ∈ (1st
‘𝑠)))) |
8 | 7 | anidms 395 |
. . . . 5
⊢ (𝑠 ∈ P →
(𝑠<P 𝑠 ↔ ∃𝑞 ∈ Q (𝑞 ∈ (2nd
‘𝑠) ∧ 𝑞 ∈ (1st
‘𝑠)))) |
9 | 6, 8 | mtbird 668 |
. . . 4
⊢ (𝑠 ∈ P →
¬ 𝑠<P 𝑠) |
10 | 9 | adantl 275 |
. . 3
⊢
((⊤ ∧ 𝑠
∈ P) → ¬ 𝑠<P 𝑠) |
11 | | ltdfpr 7455 |
. . . . . . . . . . 11
⊢ ((𝑠 ∈ P ∧
𝑡 ∈ P)
→ (𝑠<P 𝑡 ↔ ∃𝑞 ∈ Q (𝑞 ∈ (2nd
‘𝑠) ∧ 𝑞 ∈ (1st
‘𝑡)))) |
12 | 11 | 3adant3 1012 |
. . . . . . . . . 10
⊢ ((𝑠 ∈ P ∧
𝑡 ∈ P
∧ 𝑢 ∈
P) → (𝑠<P 𝑡 ↔ ∃𝑞 ∈ Q (𝑞 ∈ (2nd
‘𝑠) ∧ 𝑞 ∈ (1st
‘𝑡)))) |
13 | | ltdfpr 7455 |
. . . . . . . . . . 11
⊢ ((𝑡 ∈ P ∧
𝑢 ∈ P)
→ (𝑡<P 𝑢 ↔ ∃𝑟 ∈ Q (𝑟 ∈ (2nd
‘𝑡) ∧ 𝑟 ∈ (1st
‘𝑢)))) |
14 | 13 | 3adant1 1010 |
. . . . . . . . . 10
⊢ ((𝑠 ∈ P ∧
𝑡 ∈ P
∧ 𝑢 ∈
P) → (𝑡<P 𝑢 ↔ ∃𝑟 ∈ Q (𝑟 ∈ (2nd
‘𝑡) ∧ 𝑟 ∈ (1st
‘𝑢)))) |
15 | 12, 14 | anbi12d 470 |
. . . . . . . . 9
⊢ ((𝑠 ∈ P ∧
𝑡 ∈ P
∧ 𝑢 ∈
P) → ((𝑠<P 𝑡 ∧ 𝑡<P 𝑢) ↔ (∃𝑞 ∈ Q (𝑞 ∈ (2nd
‘𝑠) ∧ 𝑞 ∈ (1st
‘𝑡)) ∧
∃𝑟 ∈
Q (𝑟 ∈
(2nd ‘𝑡)
∧ 𝑟 ∈
(1st ‘𝑢))))) |
16 | | reeanv 2639 |
. . . . . . . . 9
⊢
(∃𝑞 ∈
Q ∃𝑟
∈ Q ((𝑞
∈ (2nd ‘𝑠) ∧ 𝑞 ∈ (1st ‘𝑡)) ∧ (𝑟 ∈ (2nd ‘𝑡) ∧ 𝑟 ∈ (1st ‘𝑢))) ↔ (∃𝑞 ∈ Q (𝑞 ∈ (2nd
‘𝑠) ∧ 𝑞 ∈ (1st
‘𝑡)) ∧
∃𝑟 ∈
Q (𝑟 ∈
(2nd ‘𝑡)
∧ 𝑟 ∈
(1st ‘𝑢)))) |
17 | 15, 16 | bitr4di 197 |
. . . . . . . 8
⊢ ((𝑠 ∈ P ∧
𝑡 ∈ P
∧ 𝑢 ∈
P) → ((𝑠<P 𝑡 ∧ 𝑡<P 𝑢) ↔ ∃𝑞 ∈ Q
∃𝑟 ∈
Q ((𝑞 ∈
(2nd ‘𝑠)
∧ 𝑞 ∈
(1st ‘𝑡))
∧ (𝑟 ∈
(2nd ‘𝑡)
∧ 𝑟 ∈
(1st ‘𝑢))))) |
18 | 17 | biimpa 294 |
. . . . . . 7
⊢ (((𝑠 ∈ P ∧
𝑡 ∈ P
∧ 𝑢 ∈
P) ∧ (𝑠<P 𝑡 ∧ 𝑡<P 𝑢)) → ∃𝑞 ∈ Q
∃𝑟 ∈
Q ((𝑞 ∈
(2nd ‘𝑠)
∧ 𝑞 ∈
(1st ‘𝑡))
∧ (𝑟 ∈
(2nd ‘𝑡)
∧ 𝑟 ∈
(1st ‘𝑢)))) |
19 | | simprll 532 |
. . . . . . . . . . 11
⊢ ((((𝑠 ∈ P ∧
𝑡 ∈ P
∧ 𝑢 ∈
P) ∧ (𝑠<P 𝑡 ∧ 𝑡<P 𝑢)) ∧ ((𝑞 ∈ (2nd ‘𝑠) ∧ 𝑞 ∈ (1st ‘𝑡)) ∧ (𝑟 ∈ (2nd ‘𝑡) ∧ 𝑟 ∈ (1st ‘𝑢)))) → 𝑞 ∈ (2nd ‘𝑠)) |
20 | | prop 7424 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑡 ∈ P →
〈(1st ‘𝑡), (2nd ‘𝑡)〉 ∈
P) |
21 | | prltlu 7436 |
. . . . . . . . . . . . . . . . . 18
⊢
((〈(1st ‘𝑡), (2nd ‘𝑡)〉 ∈ P ∧ 𝑞 ∈ (1st
‘𝑡) ∧ 𝑟 ∈ (2nd
‘𝑡)) → 𝑞 <Q
𝑟) |
22 | 20, 21 | syl3an1 1266 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑡 ∈ P ∧
𝑞 ∈ (1st
‘𝑡) ∧ 𝑟 ∈ (2nd
‘𝑡)) → 𝑞 <Q
𝑟) |
23 | 22 | 3adant3r 1230 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑡 ∈ P ∧
𝑞 ∈ (1st
‘𝑡) ∧ (𝑟 ∈ (2nd
‘𝑡) ∧ 𝑟 ∈ (1st
‘𝑢))) → 𝑞 <Q
𝑟) |
24 | 23 | 3adant2l 1227 |
. . . . . . . . . . . . . . 15
⊢ ((𝑡 ∈ P ∧
(𝑞 ∈ (2nd
‘𝑠) ∧ 𝑞 ∈ (1st
‘𝑡)) ∧ (𝑟 ∈ (2nd
‘𝑡) ∧ 𝑟 ∈ (1st
‘𝑢))) → 𝑞 <Q
𝑟) |
25 | 24 | 3expb 1199 |
. . . . . . . . . . . . . 14
⊢ ((𝑡 ∈ P ∧
((𝑞 ∈ (2nd
‘𝑠) ∧ 𝑞 ∈ (1st
‘𝑡)) ∧ (𝑟 ∈ (2nd
‘𝑡) ∧ 𝑟 ∈ (1st
‘𝑢)))) → 𝑞 <Q
𝑟) |
26 | 25 | 3ad2antl2 1155 |
. . . . . . . . . . . . 13
⊢ (((𝑠 ∈ P ∧
𝑡 ∈ P
∧ 𝑢 ∈
P) ∧ ((𝑞
∈ (2nd ‘𝑠) ∧ 𝑞 ∈ (1st ‘𝑡)) ∧ (𝑟 ∈ (2nd ‘𝑡) ∧ 𝑟 ∈ (1st ‘𝑢)))) → 𝑞 <Q 𝑟) |
27 | 26 | adantlr 474 |
. . . . . . . . . . . 12
⊢ ((((𝑠 ∈ P ∧
𝑡 ∈ P
∧ 𝑢 ∈
P) ∧ (𝑠<P 𝑡 ∧ 𝑡<P 𝑢)) ∧ ((𝑞 ∈ (2nd ‘𝑠) ∧ 𝑞 ∈ (1st ‘𝑡)) ∧ (𝑟 ∈ (2nd ‘𝑡) ∧ 𝑟 ∈ (1st ‘𝑢)))) → 𝑞 <Q 𝑟) |
28 | | prop 7424 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 ∈ P →
〈(1st ‘𝑢), (2nd ‘𝑢)〉 ∈
P) |
29 | | prcdnql 7433 |
. . . . . . . . . . . . . . . . 17
⊢
((〈(1st ‘𝑢), (2nd ‘𝑢)〉 ∈ P ∧ 𝑟 ∈ (1st
‘𝑢)) → (𝑞 <Q
𝑟 → 𝑞 ∈ (1st ‘𝑢))) |
30 | 28, 29 | sylan 281 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 ∈ P ∧
𝑟 ∈ (1st
‘𝑢)) → (𝑞 <Q
𝑟 → 𝑞 ∈ (1st ‘𝑢))) |
31 | 30 | adantrl 475 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 ∈ P ∧
(𝑟 ∈ (2nd
‘𝑡) ∧ 𝑟 ∈ (1st
‘𝑢))) → (𝑞 <Q
𝑟 → 𝑞 ∈ (1st ‘𝑢))) |
32 | 31 | adantrl 475 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ P ∧
((𝑞 ∈ (2nd
‘𝑠) ∧ 𝑞 ∈ (1st
‘𝑡)) ∧ (𝑟 ∈ (2nd
‘𝑡) ∧ 𝑟 ∈ (1st
‘𝑢)))) → (𝑞 <Q
𝑟 → 𝑞 ∈ (1st ‘𝑢))) |
33 | 32 | 3ad2antl3 1156 |
. . . . . . . . . . . . 13
⊢ (((𝑠 ∈ P ∧
𝑡 ∈ P
∧ 𝑢 ∈
P) ∧ ((𝑞
∈ (2nd ‘𝑠) ∧ 𝑞 ∈ (1st ‘𝑡)) ∧ (𝑟 ∈ (2nd ‘𝑡) ∧ 𝑟 ∈ (1st ‘𝑢)))) → (𝑞 <Q 𝑟 → 𝑞 ∈ (1st ‘𝑢))) |
34 | 33 | adantlr 474 |
. . . . . . . . . . . 12
⊢ ((((𝑠 ∈ P ∧
𝑡 ∈ P
∧ 𝑢 ∈
P) ∧ (𝑠<P 𝑡 ∧ 𝑡<P 𝑢)) ∧ ((𝑞 ∈ (2nd ‘𝑠) ∧ 𝑞 ∈ (1st ‘𝑡)) ∧ (𝑟 ∈ (2nd ‘𝑡) ∧ 𝑟 ∈ (1st ‘𝑢)))) → (𝑞 <Q 𝑟 → 𝑞 ∈ (1st ‘𝑢))) |
35 | 27, 34 | mpd 13 |
. . . . . . . . . . 11
⊢ ((((𝑠 ∈ P ∧
𝑡 ∈ P
∧ 𝑢 ∈
P) ∧ (𝑠<P 𝑡 ∧ 𝑡<P 𝑢)) ∧ ((𝑞 ∈ (2nd ‘𝑠) ∧ 𝑞 ∈ (1st ‘𝑡)) ∧ (𝑟 ∈ (2nd ‘𝑡) ∧ 𝑟 ∈ (1st ‘𝑢)))) → 𝑞 ∈ (1st ‘𝑢)) |
36 | 19, 35 | jca 304 |
. . . . . . . . . 10
⊢ ((((𝑠 ∈ P ∧
𝑡 ∈ P
∧ 𝑢 ∈
P) ∧ (𝑠<P 𝑡 ∧ 𝑡<P 𝑢)) ∧ ((𝑞 ∈ (2nd ‘𝑠) ∧ 𝑞 ∈ (1st ‘𝑡)) ∧ (𝑟 ∈ (2nd ‘𝑡) ∧ 𝑟 ∈ (1st ‘𝑢)))) → (𝑞 ∈ (2nd ‘𝑠) ∧ 𝑞 ∈ (1st ‘𝑢))) |
37 | 36 | ex 114 |
. . . . . . . . 9
⊢ (((𝑠 ∈ P ∧
𝑡 ∈ P
∧ 𝑢 ∈
P) ∧ (𝑠<P 𝑡 ∧ 𝑡<P 𝑢)) → (((𝑞 ∈ (2nd ‘𝑠) ∧ 𝑞 ∈ (1st ‘𝑡)) ∧ (𝑟 ∈ (2nd ‘𝑡) ∧ 𝑟 ∈ (1st ‘𝑢))) → (𝑞 ∈ (2nd ‘𝑠) ∧ 𝑞 ∈ (1st ‘𝑢)))) |
38 | 37 | rexlimdvw 2591 |
. . . . . . . 8
⊢ (((𝑠 ∈ P ∧
𝑡 ∈ P
∧ 𝑢 ∈
P) ∧ (𝑠<P 𝑡 ∧ 𝑡<P 𝑢)) → (∃𝑟 ∈ Q ((𝑞 ∈ (2nd
‘𝑠) ∧ 𝑞 ∈ (1st
‘𝑡)) ∧ (𝑟 ∈ (2nd
‘𝑡) ∧ 𝑟 ∈ (1st
‘𝑢))) → (𝑞 ∈ (2nd
‘𝑠) ∧ 𝑞 ∈ (1st
‘𝑢)))) |
39 | 38 | reximdv 2571 |
. . . . . . 7
⊢ (((𝑠 ∈ P ∧
𝑡 ∈ P
∧ 𝑢 ∈
P) ∧ (𝑠<P 𝑡 ∧ 𝑡<P 𝑢)) → (∃𝑞 ∈ Q
∃𝑟 ∈
Q ((𝑞 ∈
(2nd ‘𝑠)
∧ 𝑞 ∈
(1st ‘𝑡))
∧ (𝑟 ∈
(2nd ‘𝑡)
∧ 𝑟 ∈
(1st ‘𝑢)))
→ ∃𝑞 ∈
Q (𝑞 ∈
(2nd ‘𝑠)
∧ 𝑞 ∈
(1st ‘𝑢)))) |
40 | 18, 39 | mpd 13 |
. . . . . 6
⊢ (((𝑠 ∈ P ∧
𝑡 ∈ P
∧ 𝑢 ∈
P) ∧ (𝑠<P 𝑡 ∧ 𝑡<P 𝑢)) → ∃𝑞 ∈ Q (𝑞 ∈ (2nd
‘𝑠) ∧ 𝑞 ∈ (1st
‘𝑢))) |
41 | | ltdfpr 7455 |
. . . . . . . . 9
⊢ ((𝑠 ∈ P ∧
𝑢 ∈ P)
→ (𝑠<P 𝑢 ↔ ∃𝑞 ∈ Q (𝑞 ∈ (2nd
‘𝑠) ∧ 𝑞 ∈ (1st
‘𝑢)))) |
42 | 41 | 3adant2 1011 |
. . . . . . . 8
⊢ ((𝑠 ∈ P ∧
𝑡 ∈ P
∧ 𝑢 ∈
P) → (𝑠<P 𝑢 ↔ ∃𝑞 ∈ Q (𝑞 ∈ (2nd
‘𝑠) ∧ 𝑞 ∈ (1st
‘𝑢)))) |
43 | 42 | biimprd 157 |
. . . . . . 7
⊢ ((𝑠 ∈ P ∧
𝑡 ∈ P
∧ 𝑢 ∈
P) → (∃𝑞 ∈ Q (𝑞 ∈ (2nd ‘𝑠) ∧ 𝑞 ∈ (1st ‘𝑢)) → 𝑠<P 𝑢)) |
44 | 43 | adantr 274 |
. . . . . 6
⊢ (((𝑠 ∈ P ∧
𝑡 ∈ P
∧ 𝑢 ∈
P) ∧ (𝑠<P 𝑡 ∧ 𝑡<P 𝑢)) → (∃𝑞 ∈ Q (𝑞 ∈ (2nd
‘𝑠) ∧ 𝑞 ∈ (1st
‘𝑢)) → 𝑠<P
𝑢)) |
45 | 40, 44 | mpd 13 |
. . . . 5
⊢ (((𝑠 ∈ P ∧
𝑡 ∈ P
∧ 𝑢 ∈
P) ∧ (𝑠<P 𝑡 ∧ 𝑡<P 𝑢)) → 𝑠<P 𝑢) |
46 | 45 | ex 114 |
. . . 4
⊢ ((𝑠 ∈ P ∧
𝑡 ∈ P
∧ 𝑢 ∈
P) → ((𝑠<P 𝑡 ∧ 𝑡<P 𝑢) → 𝑠<P 𝑢)) |
47 | 46 | adantl 275 |
. . 3
⊢
((⊤ ∧ (𝑠
∈ P ∧ 𝑡 ∈ P ∧ 𝑢 ∈ P)) →
((𝑠<P 𝑡 ∧ 𝑡<P 𝑢) → 𝑠<P 𝑢)) |
48 | 10, 47 | ispod 4287 |
. 2
⊢ (⊤
→ <P Po P) |
49 | 48 | mptru 1357 |
1
⊢
<P Po P |