Step | Hyp | Ref
| Expression |
1 | | ltrelpr 7467 |
. . . 4
⊢
<P ⊆ (P ×
P) |
2 | 1 | brel 4663 |
. . 3
⊢ (𝐴<P
𝐵 → (𝐴 ∈ P ∧ 𝐵 ∈
P)) |
3 | | ltdfpr 7468 |
. . . 4
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ (𝐴<P 𝐵 ↔ ∃𝑥 ∈ Q (𝑥 ∈ (2nd
‘𝐴) ∧ 𝑥 ∈ (1st
‘𝐵)))) |
4 | 3 | biimpd 143 |
. . 3
⊢ ((𝐴 ∈ P ∧
𝐵 ∈ P)
→ (𝐴<P 𝐵 → ∃𝑥 ∈ Q (𝑥 ∈ (2nd
‘𝐴) ∧ 𝑥 ∈ (1st
‘𝐵)))) |
5 | 2, 4 | mpcom 36 |
. 2
⊢ (𝐴<P
𝐵 → ∃𝑥 ∈ Q (𝑥 ∈ (2nd
‘𝐴) ∧ 𝑥 ∈ (1st
‘𝐵))) |
6 | | simpll 524 |
. . . . . 6
⊢ (((𝐴<P
𝐵 ∧ (𝑥 ∈ Q ∧ (𝑥 ∈ (2nd
‘𝐴) ∧ 𝑥 ∈ (1st
‘𝐵)))) ∧ 𝑦 ∈ (1st
‘𝐴)) → 𝐴<P
𝐵) |
7 | | simpr 109 |
. . . . . 6
⊢ (((𝐴<P
𝐵 ∧ (𝑥 ∈ Q ∧ (𝑥 ∈ (2nd
‘𝐴) ∧ 𝑥 ∈ (1st
‘𝐵)))) ∧ 𝑦 ∈ (1st
‘𝐴)) → 𝑦 ∈ (1st
‘𝐴)) |
8 | | simprrl 534 |
. . . . . . 7
⊢ ((𝐴<P
𝐵 ∧ (𝑥 ∈ Q ∧ (𝑥 ∈ (2nd
‘𝐴) ∧ 𝑥 ∈ (1st
‘𝐵)))) → 𝑥 ∈ (2nd
‘𝐴)) |
9 | 8 | adantr 274 |
. . . . . 6
⊢ (((𝐴<P
𝐵 ∧ (𝑥 ∈ Q ∧ (𝑥 ∈ (2nd
‘𝐴) ∧ 𝑥 ∈ (1st
‘𝐵)))) ∧ 𝑦 ∈ (1st
‘𝐴)) → 𝑥 ∈ (2nd
‘𝐴)) |
10 | 2 | simpld 111 |
. . . . . . . 8
⊢ (𝐴<P
𝐵 → 𝐴 ∈ P) |
11 | | prop 7437 |
. . . . . . . 8
⊢ (𝐴 ∈ P →
〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈
P) |
12 | 10, 11 | syl 14 |
. . . . . . 7
⊢ (𝐴<P
𝐵 →
〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈
P) |
13 | | prltlu 7449 |
. . . . . . 7
⊢
((〈(1st ‘𝐴), (2nd ‘𝐴)〉 ∈ P ∧ 𝑦 ∈ (1st
‘𝐴) ∧ 𝑥 ∈ (2nd
‘𝐴)) → 𝑦 <Q
𝑥) |
14 | 12, 13 | syl3an1 1266 |
. . . . . 6
⊢ ((𝐴<P
𝐵 ∧ 𝑦 ∈ (1st ‘𝐴) ∧ 𝑥 ∈ (2nd ‘𝐴)) → 𝑦 <Q 𝑥) |
15 | 6, 7, 9, 14 | syl3anc 1233 |
. . . . 5
⊢ (((𝐴<P
𝐵 ∧ (𝑥 ∈ Q ∧ (𝑥 ∈ (2nd
‘𝐴) ∧ 𝑥 ∈ (1st
‘𝐵)))) ∧ 𝑦 ∈ (1st
‘𝐴)) → 𝑦 <Q
𝑥) |
16 | | simprrr 535 |
. . . . . . 7
⊢ ((𝐴<P
𝐵 ∧ (𝑥 ∈ Q ∧ (𝑥 ∈ (2nd
‘𝐴) ∧ 𝑥 ∈ (1st
‘𝐵)))) → 𝑥 ∈ (1st
‘𝐵)) |
17 | 16 | adantr 274 |
. . . . . 6
⊢ (((𝐴<P
𝐵 ∧ (𝑥 ∈ Q ∧ (𝑥 ∈ (2nd
‘𝐴) ∧ 𝑥 ∈ (1st
‘𝐵)))) ∧ 𝑦 ∈ (1st
‘𝐴)) → 𝑥 ∈ (1st
‘𝐵)) |
18 | 2 | simprd 113 |
. . . . . . . 8
⊢ (𝐴<P
𝐵 → 𝐵 ∈ P) |
19 | | prop 7437 |
. . . . . . . 8
⊢ (𝐵 ∈ P →
〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈
P) |
20 | 18, 19 | syl 14 |
. . . . . . 7
⊢ (𝐴<P
𝐵 →
〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈
P) |
21 | | prcdnql 7446 |
. . . . . . 7
⊢
((〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈ P ∧ 𝑥 ∈ (1st
‘𝐵)) → (𝑦 <Q
𝑥 → 𝑦 ∈ (1st ‘𝐵))) |
22 | 20, 21 | sylan 281 |
. . . . . 6
⊢ ((𝐴<P
𝐵 ∧ 𝑥 ∈ (1st ‘𝐵)) → (𝑦 <Q 𝑥 → 𝑦 ∈ (1st ‘𝐵))) |
23 | 6, 17, 22 | syl2anc 409 |
. . . . 5
⊢ (((𝐴<P
𝐵 ∧ (𝑥 ∈ Q ∧ (𝑥 ∈ (2nd
‘𝐴) ∧ 𝑥 ∈ (1st
‘𝐵)))) ∧ 𝑦 ∈ (1st
‘𝐴)) → (𝑦 <Q
𝑥 → 𝑦 ∈ (1st ‘𝐵))) |
24 | 15, 23 | mpd 13 |
. . . 4
⊢ (((𝐴<P
𝐵 ∧ (𝑥 ∈ Q ∧ (𝑥 ∈ (2nd
‘𝐴) ∧ 𝑥 ∈ (1st
‘𝐵)))) ∧ 𝑦 ∈ (1st
‘𝐴)) → 𝑦 ∈ (1st
‘𝐵)) |
25 | 24 | ex 114 |
. . 3
⊢ ((𝐴<P
𝐵 ∧ (𝑥 ∈ Q ∧ (𝑥 ∈ (2nd
‘𝐴) ∧ 𝑥 ∈ (1st
‘𝐵)))) → (𝑦 ∈ (1st
‘𝐴) → 𝑦 ∈ (1st
‘𝐵))) |
26 | 25 | ssrdv 3153 |
. 2
⊢ ((𝐴<P
𝐵 ∧ (𝑥 ∈ Q ∧ (𝑥 ∈ (2nd
‘𝐴) ∧ 𝑥 ∈ (1st
‘𝐵)))) →
(1st ‘𝐴)
⊆ (1st ‘𝐵)) |
27 | 5, 26 | rexlimddv 2592 |
1
⊢ (𝐴<P
𝐵 → (1st
‘𝐴) ⊆
(1st ‘𝐵)) |