Step | Hyp | Ref
| Expression |
1 | | prop 7395 |
. . . . . 6
⊢ (𝐵 ∈ P →
〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈
P) |
2 | | prnminu 7409 |
. . . . . 6
⊢
((〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈ P ∧ 𝐴 ∈ (2nd
‘𝐵)) →
∃𝑥 ∈
(2nd ‘𝐵)𝑥 <Q 𝐴) |
3 | 1, 2 | sylan 281 |
. . . . 5
⊢ ((𝐵 ∈ P ∧
𝐴 ∈ (2nd
‘𝐵)) →
∃𝑥 ∈
(2nd ‘𝐵)𝑥 <Q 𝐴) |
4 | | elprnqu 7402 |
. . . . . . . . . 10
⊢
((〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈ P ∧ 𝑥 ∈ (2nd
‘𝐵)) → 𝑥 ∈
Q) |
5 | 1, 4 | sylan 281 |
. . . . . . . . 9
⊢ ((𝐵 ∈ P ∧
𝑥 ∈ (2nd
‘𝐵)) → 𝑥 ∈
Q) |
6 | 5 | ad2ant2r 501 |
. . . . . . . 8
⊢ (((𝐵 ∈ P ∧
𝐴 ∈ (2nd
‘𝐵)) ∧ (𝑥 ∈ (2nd
‘𝐵) ∧ 𝑥 <Q
𝐴)) → 𝑥 ∈
Q) |
7 | | simprl 521 |
. . . . . . . 8
⊢ (((𝐵 ∈ P ∧
𝐴 ∈ (2nd
‘𝐵)) ∧ (𝑥 ∈ (2nd
‘𝐵) ∧ 𝑥 <Q
𝐴)) → 𝑥 ∈ (2nd
‘𝐵)) |
8 | | vex 2715 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
9 | | breq1 3968 |
. . . . . . . . . . . 12
⊢ (𝑙 = 𝑥 → (𝑙 <Q 𝐴 ↔ 𝑥 <Q 𝐴)) |
10 | 8, 9 | elab 2856 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ {𝑙 ∣ 𝑙 <Q 𝐴} ↔ 𝑥 <Q 𝐴) |
11 | 10 | biimpri 132 |
. . . . . . . . . 10
⊢ (𝑥 <Q
𝐴 → 𝑥 ∈ {𝑙 ∣ 𝑙 <Q 𝐴}) |
12 | | ltnqex 7469 |
. . . . . . . . . . . 12
⊢ {𝑙 ∣ 𝑙 <Q 𝐴} ∈ V |
13 | | gtnqex 7470 |
. . . . . . . . . . . 12
⊢ {𝑢 ∣ 𝐴 <Q 𝑢} ∈ V |
14 | 12, 13 | op1st 6094 |
. . . . . . . . . . 11
⊢
(1st ‘〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉) = {𝑙 ∣ 𝑙 <Q 𝐴} |
15 | 14 | eleq2i 2224 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉) ↔ 𝑥 ∈ {𝑙 ∣ 𝑙 <Q 𝐴}) |
16 | 11, 15 | sylibr 133 |
. . . . . . . . 9
⊢ (𝑥 <Q
𝐴 → 𝑥 ∈ (1st ‘〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉)) |
17 | 16 | ad2antll 483 |
. . . . . . . 8
⊢ (((𝐵 ∈ P ∧
𝐴 ∈ (2nd
‘𝐵)) ∧ (𝑥 ∈ (2nd
‘𝐵) ∧ 𝑥 <Q
𝐴)) → 𝑥 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉)) |
18 | | 19.8a 1570 |
. . . . . . . 8
⊢ ((𝑥 ∈ Q ∧
(𝑥 ∈ (2nd
‘𝐵) ∧ 𝑥 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉))) → ∃𝑥(𝑥 ∈ Q ∧ (𝑥 ∈ (2nd
‘𝐵) ∧ 𝑥 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉)))) |
19 | 6, 7, 17, 18 | syl12anc 1218 |
. . . . . . 7
⊢ (((𝐵 ∈ P ∧
𝐴 ∈ (2nd
‘𝐵)) ∧ (𝑥 ∈ (2nd
‘𝐵) ∧ 𝑥 <Q
𝐴)) → ∃𝑥(𝑥 ∈ Q ∧ (𝑥 ∈ (2nd
‘𝐵) ∧ 𝑥 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉)))) |
20 | | df-rex 2441 |
. . . . . . 7
⊢
(∃𝑥 ∈
Q (𝑥 ∈
(2nd ‘𝐵)
∧ 𝑥 ∈
(1st ‘〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉)) ↔ ∃𝑥(𝑥 ∈ Q ∧ (𝑥 ∈ (2nd
‘𝐵) ∧ 𝑥 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉)))) |
21 | 19, 20 | sylibr 133 |
. . . . . 6
⊢ (((𝐵 ∈ P ∧
𝐴 ∈ (2nd
‘𝐵)) ∧ (𝑥 ∈ (2nd
‘𝐵) ∧ 𝑥 <Q
𝐴)) → ∃𝑥 ∈ Q (𝑥 ∈ (2nd
‘𝐵) ∧ 𝑥 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉))) |
22 | | elprnqu 7402 |
. . . . . . . . 9
⊢
((〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈ P ∧ 𝐴 ∈ (2nd
‘𝐵)) → 𝐴 ∈
Q) |
23 | 1, 22 | sylan 281 |
. . . . . . . 8
⊢ ((𝐵 ∈ P ∧
𝐴 ∈ (2nd
‘𝐵)) → 𝐴 ∈
Q) |
24 | | nqprlu 7467 |
. . . . . . . . 9
⊢ (𝐴 ∈ Q →
〈{𝑙 ∣ 𝑙 <Q
𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉 ∈
P) |
25 | | ltdfpr 7426 |
. . . . . . . . 9
⊢ ((𝐵 ∈ P ∧
〈{𝑙 ∣ 𝑙 <Q
𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉 ∈ P)
→ (𝐵<P 〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉 ↔ ∃𝑥 ∈ Q (𝑥 ∈ (2nd
‘𝐵) ∧ 𝑥 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉)))) |
26 | 24, 25 | sylan2 284 |
. . . . . . . 8
⊢ ((𝐵 ∈ P ∧
𝐴 ∈ Q)
→ (𝐵<P 〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉 ↔ ∃𝑥 ∈ Q (𝑥 ∈ (2nd
‘𝐵) ∧ 𝑥 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉)))) |
27 | 23, 26 | syldan 280 |
. . . . . . 7
⊢ ((𝐵 ∈ P ∧
𝐴 ∈ (2nd
‘𝐵)) → (𝐵<P
〈{𝑙 ∣ 𝑙 <Q
𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉 ↔ ∃𝑥 ∈ Q (𝑥 ∈ (2nd
‘𝐵) ∧ 𝑥 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉)))) |
28 | 27 | adantr 274 |
. . . . . 6
⊢ (((𝐵 ∈ P ∧
𝐴 ∈ (2nd
‘𝐵)) ∧ (𝑥 ∈ (2nd
‘𝐵) ∧ 𝑥 <Q
𝐴)) → (𝐵<P
〈{𝑙 ∣ 𝑙 <Q
𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉 ↔ ∃𝑥 ∈ Q (𝑥 ∈ (2nd
‘𝐵) ∧ 𝑥 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉)))) |
29 | 21, 28 | mpbird 166 |
. . . . 5
⊢ (((𝐵 ∈ P ∧
𝐴 ∈ (2nd
‘𝐵)) ∧ (𝑥 ∈ (2nd
‘𝐵) ∧ 𝑥 <Q
𝐴)) → 𝐵<P
〈{𝑙 ∣ 𝑙 <Q
𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉) |
30 | 3, 29 | rexlimddv 2579 |
. . . 4
⊢ ((𝐵 ∈ P ∧
𝐴 ∈ (2nd
‘𝐵)) → 𝐵<P
〈{𝑙 ∣ 𝑙 <Q
𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉) |
31 | 30 | ex 114 |
. . 3
⊢ (𝐵 ∈ P →
(𝐴 ∈ (2nd
‘𝐵) → 𝐵<P
〈{𝑙 ∣ 𝑙 <Q
𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉)) |
32 | 31 | adantl 275 |
. 2
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ P)
→ (𝐴 ∈
(2nd ‘𝐵)
→ 𝐵<P 〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉)) |
33 | 26 | ancoms 266 |
. . . . 5
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ P)
→ (𝐵<P 〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉 ↔ ∃𝑥 ∈ Q (𝑥 ∈ (2nd
‘𝐵) ∧ 𝑥 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉)))) |
34 | 33 | biimpa 294 |
. . . 4
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ P)
∧ 𝐵<P 〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉) → ∃𝑥 ∈ Q (𝑥 ∈ (2nd
‘𝐵) ∧ 𝑥 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉))) |
35 | 15, 10 | bitri 183 |
. . . . . . . 8
⊢ (𝑥 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉) ↔ 𝑥 <Q
𝐴) |
36 | 35 | biimpi 119 |
. . . . . . 7
⊢ (𝑥 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉) → 𝑥 <Q
𝐴) |
37 | 36 | ad2antll 483 |
. . . . . 6
⊢ ((𝑥 ∈ Q ∧
(𝑥 ∈ (2nd
‘𝐵) ∧ 𝑥 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉))) → 𝑥 <Q
𝐴) |
38 | 37 | adantl 275 |
. . . . 5
⊢ ((((𝐴 ∈ Q ∧
𝐵 ∈ P)
∧ 𝐵<P 〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉) ∧ (𝑥 ∈ Q ∧
(𝑥 ∈ (2nd
‘𝐵) ∧ 𝑥 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉)))) → 𝑥 <Q
𝐴) |
39 | | simpllr 524 |
. . . . . 6
⊢ ((((𝐴 ∈ Q ∧
𝐵 ∈ P)
∧ 𝐵<P 〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉) ∧ (𝑥 ∈ Q ∧
(𝑥 ∈ (2nd
‘𝐵) ∧ 𝑥 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉)))) → 𝐵 ∈
P) |
40 | | simprrl 529 |
. . . . . 6
⊢ ((((𝐴 ∈ Q ∧
𝐵 ∈ P)
∧ 𝐵<P 〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉) ∧ (𝑥 ∈ Q ∧
(𝑥 ∈ (2nd
‘𝐵) ∧ 𝑥 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉)))) → 𝑥 ∈ (2nd
‘𝐵)) |
41 | | prcunqu 7405 |
. . . . . . 7
⊢
((〈(1st ‘𝐵), (2nd ‘𝐵)〉 ∈ P ∧ 𝑥 ∈ (2nd
‘𝐵)) → (𝑥 <Q
𝐴 → 𝐴 ∈ (2nd ‘𝐵))) |
42 | 1, 41 | sylan 281 |
. . . . . 6
⊢ ((𝐵 ∈ P ∧
𝑥 ∈ (2nd
‘𝐵)) → (𝑥 <Q
𝐴 → 𝐴 ∈ (2nd ‘𝐵))) |
43 | 39, 40, 42 | syl2anc 409 |
. . . . 5
⊢ ((((𝐴 ∈ Q ∧
𝐵 ∈ P)
∧ 𝐵<P 〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉) ∧ (𝑥 ∈ Q ∧
(𝑥 ∈ (2nd
‘𝐵) ∧ 𝑥 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉)))) → (𝑥 <Q
𝐴 → 𝐴 ∈ (2nd ‘𝐵))) |
44 | 38, 43 | mpd 13 |
. . . 4
⊢ ((((𝐴 ∈ Q ∧
𝐵 ∈ P)
∧ 𝐵<P 〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉) ∧ (𝑥 ∈ Q ∧
(𝑥 ∈ (2nd
‘𝐵) ∧ 𝑥 ∈ (1st
‘〈{𝑙 ∣
𝑙
<Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉)))) → 𝐴 ∈ (2nd
‘𝐵)) |
45 | 34, 44 | rexlimddv 2579 |
. . 3
⊢ (((𝐴 ∈ Q ∧
𝐵 ∈ P)
∧ 𝐵<P 〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉) → 𝐴 ∈ (2nd
‘𝐵)) |
46 | 45 | ex 114 |
. 2
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ P)
→ (𝐵<P 〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉 → 𝐴 ∈ (2nd ‘𝐵))) |
47 | 32, 46 | impbid 128 |
1
⊢ ((𝐴 ∈ Q ∧
𝐵 ∈ P)
→ (𝐴 ∈
(2nd ‘𝐵)
↔ 𝐵<P 〈{𝑙 ∣ 𝑙 <Q 𝐴}, {𝑢 ∣ 𝐴 <Q 𝑢}〉)) |