Step | Hyp | Ref
| Expression |
1 | | suplocexpr.ub |
. . . 4
⊢ (𝜑 → ∃𝑥 ∈ P ∀𝑦 ∈ 𝐴 𝑦<P 𝑥) |
2 | | prop 7437 |
. . . . . . 7
⊢ (𝑥 ∈ P →
〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∈
P) |
3 | | prmu 7440 |
. . . . . . 7
⊢
(〈(1st ‘𝑥), (2nd ‘𝑥)〉 ∈ P →
∃𝑠 ∈
Q 𝑠 ∈
(2nd ‘𝑥)) |
4 | 2, 3 | syl 14 |
. . . . . 6
⊢ (𝑥 ∈ P →
∃𝑠 ∈
Q 𝑠 ∈
(2nd ‘𝑥)) |
5 | 4 | ad2antrl 487 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ P ∧ ∀𝑦 ∈ 𝐴 𝑦<P 𝑥)) → ∃𝑠 ∈ Q 𝑠 ∈ (2nd
‘𝑥)) |
6 | | fo2nd 6137 |
. . . . . . . . . . . . 13
⊢
2nd :V–onto→V |
7 | | fofun 5421 |
. . . . . . . . . . . . 13
⊢
(2nd :V–onto→V → Fun 2nd ) |
8 | 6, 7 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ Fun
2nd |
9 | | fvelima 5548 |
. . . . . . . . . . . 12
⊢ ((Fun
2nd ∧ 𝑡
∈ (2nd “ 𝐴)) → ∃𝑢 ∈ 𝐴 (2nd ‘𝑢) = 𝑡) |
10 | 8, 9 | mpan 422 |
. . . . . . . . . . 11
⊢ (𝑡 ∈ (2nd “
𝐴) → ∃𝑢 ∈ 𝐴 (2nd ‘𝑢) = 𝑡) |
11 | 10 | adantl 275 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ (𝑥 ∈ P ∧
∀𝑦 ∈ 𝐴 𝑦<P 𝑥)) ∧ 𝑠 ∈ Q) ∧ 𝑠 ∈ (2nd
‘𝑥)) ∧ 𝑡 ∈ (2nd “
𝐴)) → ∃𝑢 ∈ 𝐴 (2nd ‘𝑢) = 𝑡) |
12 | | suplocexpr.m |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴) |
13 | | suplocexpr.loc |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∀𝑥 ∈ P ∀𝑦 ∈ P (𝑥<P
𝑦 → (∃𝑧 ∈ 𝐴 𝑥<P 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧<P 𝑦))) |
14 | 12, 1, 13 | suplocexprlemss 7677 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ⊆ P) |
15 | 14 | ad5antr 493 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑥 ∈ P ∧
∀𝑦 ∈ 𝐴 𝑦<P 𝑥)) ∧ 𝑠 ∈ Q) ∧ 𝑠 ∈ (2nd
‘𝑥)) ∧ 𝑡 ∈ (2nd “
𝐴)) ∧ (𝑢 ∈ 𝐴 ∧ (2nd ‘𝑢) = 𝑡)) → 𝐴 ⊆ P) |
16 | | simprl 526 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑥 ∈ P ∧
∀𝑦 ∈ 𝐴 𝑦<P 𝑥)) ∧ 𝑠 ∈ Q) ∧ 𝑠 ∈ (2nd
‘𝑥)) ∧ 𝑡 ∈ (2nd “
𝐴)) ∧ (𝑢 ∈ 𝐴 ∧ (2nd ‘𝑢) = 𝑡)) → 𝑢 ∈ 𝐴) |
17 | 15, 16 | sseldd 3148 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ (𝑥 ∈ P ∧
∀𝑦 ∈ 𝐴 𝑦<P 𝑥)) ∧ 𝑠 ∈ Q) ∧ 𝑠 ∈ (2nd
‘𝑥)) ∧ 𝑡 ∈ (2nd “
𝐴)) ∧ (𝑢 ∈ 𝐴 ∧ (2nd ‘𝑢) = 𝑡)) → 𝑢 ∈ P) |
18 | | simprl 526 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ P ∧ ∀𝑦 ∈ 𝐴 𝑦<P 𝑥)) → 𝑥 ∈ P) |
19 | 18 | ad4antr 491 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ (𝑥 ∈ P ∧
∀𝑦 ∈ 𝐴 𝑦<P 𝑥)) ∧ 𝑠 ∈ Q) ∧ 𝑠 ∈ (2nd
‘𝑥)) ∧ 𝑡 ∈ (2nd “
𝐴)) ∧ (𝑢 ∈ 𝐴 ∧ (2nd ‘𝑢) = 𝑡)) → 𝑥 ∈ P) |
20 | | breq1 3992 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 𝑢 → (𝑦<P 𝑥 ↔ 𝑢<P 𝑥)) |
21 | | simprr 527 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑥 ∈ P ∧ ∀𝑦 ∈ 𝐴 𝑦<P 𝑥)) → ∀𝑦 ∈ 𝐴 𝑦<P 𝑥) |
22 | 21 | ad4antr 491 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ (𝑥 ∈ P ∧
∀𝑦 ∈ 𝐴 𝑦<P 𝑥)) ∧ 𝑠 ∈ Q) ∧ 𝑠 ∈ (2nd
‘𝑥)) ∧ 𝑡 ∈ (2nd “
𝐴)) ∧ (𝑢 ∈ 𝐴 ∧ (2nd ‘𝑢) = 𝑡)) → ∀𝑦 ∈ 𝐴 𝑦<P 𝑥) |
23 | 20, 22, 16 | rspcdva 2839 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑥 ∈ P ∧
∀𝑦 ∈ 𝐴 𝑦<P 𝑥)) ∧ 𝑠 ∈ Q) ∧ 𝑠 ∈ (2nd
‘𝑥)) ∧ 𝑡 ∈ (2nd “
𝐴)) ∧ (𝑢 ∈ 𝐴 ∧ (2nd ‘𝑢) = 𝑡)) → 𝑢<P 𝑥) |
24 | | ltsopr 7558 |
. . . . . . . . . . . . . . . . 17
⊢
<P Or P |
25 | | so2nr 4306 |
. . . . . . . . . . . . . . . . 17
⊢
((<P Or P ∧ (𝑢 ∈ P ∧
𝑥 ∈ P))
→ ¬ (𝑢<P 𝑥 ∧ 𝑥<P 𝑢)) |
26 | 24, 25 | mpan 422 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 ∈ P ∧
𝑥 ∈ P)
→ ¬ (𝑢<P 𝑥 ∧ 𝑥<P 𝑢)) |
27 | 17, 19, 26 | syl2anc 409 |
. . . . . . . . . . . . . . 15
⊢
((((((𝜑 ∧ (𝑥 ∈ P ∧
∀𝑦 ∈ 𝐴 𝑦<P 𝑥)) ∧ 𝑠 ∈ Q) ∧ 𝑠 ∈ (2nd
‘𝑥)) ∧ 𝑡 ∈ (2nd “
𝐴)) ∧ (𝑢 ∈ 𝐴 ∧ (2nd ‘𝑢) = 𝑡)) → ¬ (𝑢<P 𝑥 ∧ 𝑥<P 𝑢)) |
28 | | imnan 685 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢<P
𝑥 → ¬ 𝑥<P
𝑢) ↔ ¬ (𝑢<P
𝑥 ∧ 𝑥<P 𝑢)) |
29 | 27, 28 | sylibr 133 |
. . . . . . . . . . . . . 14
⊢
((((((𝜑 ∧ (𝑥 ∈ P ∧
∀𝑦 ∈ 𝐴 𝑦<P 𝑥)) ∧ 𝑠 ∈ Q) ∧ 𝑠 ∈ (2nd
‘𝑥)) ∧ 𝑡 ∈ (2nd “
𝐴)) ∧ (𝑢 ∈ 𝐴 ∧ (2nd ‘𝑢) = 𝑡)) → (𝑢<P 𝑥 → ¬ 𝑥<P 𝑢)) |
30 | 23, 29 | mpd 13 |
. . . . . . . . . . . . 13
⊢
((((((𝜑 ∧ (𝑥 ∈ P ∧
∀𝑦 ∈ 𝐴 𝑦<P 𝑥)) ∧ 𝑠 ∈ Q) ∧ 𝑠 ∈ (2nd
‘𝑥)) ∧ 𝑡 ∈ (2nd “
𝐴)) ∧ (𝑢 ∈ 𝐴 ∧ (2nd ‘𝑢) = 𝑡)) → ¬ 𝑥<P 𝑢) |
31 | | aptiprlemu 7602 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ P ∧
𝑥 ∈ P
∧ ¬ 𝑥<P 𝑢) → (2nd
‘𝑥) ⊆
(2nd ‘𝑢)) |
32 | 17, 19, 30, 31 | syl3anc 1233 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ (𝑥 ∈ P ∧
∀𝑦 ∈ 𝐴 𝑦<P 𝑥)) ∧ 𝑠 ∈ Q) ∧ 𝑠 ∈ (2nd
‘𝑥)) ∧ 𝑡 ∈ (2nd “
𝐴)) ∧ (𝑢 ∈ 𝐴 ∧ (2nd ‘𝑢) = 𝑡)) → (2nd ‘𝑥) ⊆ (2nd
‘𝑢)) |
33 | | simpllr 529 |
. . . . . . . . . . . 12
⊢
((((((𝜑 ∧ (𝑥 ∈ P ∧
∀𝑦 ∈ 𝐴 𝑦<P 𝑥)) ∧ 𝑠 ∈ Q) ∧ 𝑠 ∈ (2nd
‘𝑥)) ∧ 𝑡 ∈ (2nd “
𝐴)) ∧ (𝑢 ∈ 𝐴 ∧ (2nd ‘𝑢) = 𝑡)) → 𝑠 ∈ (2nd ‘𝑥)) |
34 | 32, 33 | sseldd 3148 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ (𝑥 ∈ P ∧
∀𝑦 ∈ 𝐴 𝑦<P 𝑥)) ∧ 𝑠 ∈ Q) ∧ 𝑠 ∈ (2nd
‘𝑥)) ∧ 𝑡 ∈ (2nd “
𝐴)) ∧ (𝑢 ∈ 𝐴 ∧ (2nd ‘𝑢) = 𝑡)) → 𝑠 ∈ (2nd ‘𝑢)) |
35 | | simprr 527 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ (𝑥 ∈ P ∧
∀𝑦 ∈ 𝐴 𝑦<P 𝑥)) ∧ 𝑠 ∈ Q) ∧ 𝑠 ∈ (2nd
‘𝑥)) ∧ 𝑡 ∈ (2nd “
𝐴)) ∧ (𝑢 ∈ 𝐴 ∧ (2nd ‘𝑢) = 𝑡)) → (2nd ‘𝑢) = 𝑡) |
36 | 34, 35 | eleqtrd 2249 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ (𝑥 ∈ P ∧
∀𝑦 ∈ 𝐴 𝑦<P 𝑥)) ∧ 𝑠 ∈ Q) ∧ 𝑠 ∈ (2nd
‘𝑥)) ∧ 𝑡 ∈ (2nd “
𝐴)) ∧ (𝑢 ∈ 𝐴 ∧ (2nd ‘𝑢) = 𝑡)) → 𝑠 ∈ 𝑡) |
37 | 11, 36 | rexlimddv 2592 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ (𝑥 ∈ P ∧
∀𝑦 ∈ 𝐴 𝑦<P 𝑥)) ∧ 𝑠 ∈ Q) ∧ 𝑠 ∈ (2nd
‘𝑥)) ∧ 𝑡 ∈ (2nd “
𝐴)) → 𝑠 ∈ 𝑡) |
38 | 37 | ralrimiva 2543 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 ∈ P ∧ ∀𝑦 ∈ 𝐴 𝑦<P 𝑥)) ∧ 𝑠 ∈ Q) ∧ 𝑠 ∈ (2nd
‘𝑥)) →
∀𝑡 ∈
(2nd “ 𝐴)𝑠 ∈ 𝑡) |
39 | | vex 2733 |
. . . . . . . . 9
⊢ 𝑠 ∈ V |
40 | 39 | elint2 3838 |
. . . . . . . 8
⊢ (𝑠 ∈ ∩ (2nd “ 𝐴) ↔ ∀𝑡 ∈ (2nd “ 𝐴)𝑠 ∈ 𝑡) |
41 | 38, 40 | sylibr 133 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 ∈ P ∧ ∀𝑦 ∈ 𝐴 𝑦<P 𝑥)) ∧ 𝑠 ∈ Q) ∧ 𝑠 ∈ (2nd
‘𝑥)) → 𝑠 ∈ ∩ (2nd “ 𝐴)) |
42 | 41 | ex 114 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ P ∧ ∀𝑦 ∈ 𝐴 𝑦<P 𝑥)) ∧ 𝑠 ∈ Q) → (𝑠 ∈ (2nd
‘𝑥) → 𝑠 ∈ ∩ (2nd “ 𝐴))) |
43 | 42 | reximdva 2572 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ P ∧ ∀𝑦 ∈ 𝐴 𝑦<P 𝑥)) → (∃𝑠 ∈ Q 𝑠 ∈ (2nd
‘𝑥) →
∃𝑠 ∈
Q 𝑠 ∈
∩ (2nd “ 𝐴))) |
44 | 5, 43 | mpd 13 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ P ∧ ∀𝑦 ∈ 𝐴 𝑦<P 𝑥)) → ∃𝑠 ∈ Q 𝑠 ∈ ∩ (2nd “ 𝐴)) |
45 | 1, 44 | rexlimddv 2592 |
. . 3
⊢ (𝜑 → ∃𝑠 ∈ Q 𝑠 ∈ ∩
(2nd “ 𝐴)) |
46 | | simprr 527 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑠 ∈ ∩ (2nd “ 𝐴))) → 𝑠 ∈ ∩
(2nd “ 𝐴)) |
47 | | simprl 526 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑠 ∈ ∩ (2nd “ 𝐴))) → 𝑠 ∈ Q) |
48 | | 1nq 7328 |
. . . . . . . . 9
⊢
1Q ∈ Q |
49 | | addclnq 7337 |
. . . . . . . . 9
⊢ ((𝑠 ∈ Q ∧
1Q ∈ Q) → (𝑠 +Q
1Q) ∈ Q) |
50 | 47, 48, 49 | sylancl 411 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑠 ∈ ∩ (2nd “ 𝐴))) → (𝑠 +Q
1Q) ∈ Q) |
51 | | ltaddnq 7369 |
. . . . . . . . 9
⊢ ((𝑠 ∈ Q ∧
1Q ∈ Q) → 𝑠 <Q (𝑠 +Q
1Q)) |
52 | 47, 48, 51 | sylancl 411 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑠 ∈ ∩ (2nd “ 𝐴))) → 𝑠 <Q (𝑠 +Q
1Q)) |
53 | | breq2 3993 |
. . . . . . . . 9
⊢ (𝑗 = (𝑠 +Q
1Q) → (𝑠 <Q 𝑗 ↔ 𝑠 <Q (𝑠 +Q
1Q))) |
54 | 53 | rspcev 2834 |
. . . . . . . 8
⊢ (((𝑠 +Q
1Q) ∈ Q ∧ 𝑠 <Q (𝑠 +Q
1Q)) → ∃𝑗 ∈ Q 𝑠 <Q 𝑗) |
55 | 50, 52, 54 | syl2anc 409 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑠 ∈ ∩ (2nd “ 𝐴))) → ∃𝑗 ∈ Q 𝑠 <Q 𝑗) |
56 | | breq1 3992 |
. . . . . . . . 9
⊢ (𝑤 = 𝑠 → (𝑤 <Q 𝑗 ↔ 𝑠 <Q 𝑗)) |
57 | 56 | rexbidv 2471 |
. . . . . . . 8
⊢ (𝑤 = 𝑠 → (∃𝑗 ∈ Q 𝑤 <Q 𝑗 ↔ ∃𝑗 ∈ Q 𝑠 <Q
𝑗)) |
58 | 57 | rspcev 2834 |
. . . . . . 7
⊢ ((𝑠 ∈ ∩ (2nd “ 𝐴) ∧ ∃𝑗 ∈ Q 𝑠 <Q 𝑗) → ∃𝑤 ∈ ∩ (2nd “ 𝐴)∃𝑗 ∈ Q 𝑤 <Q 𝑗) |
59 | 46, 55, 58 | syl2anc 409 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑠 ∈ ∩ (2nd “ 𝐴))) → ∃𝑤 ∈ ∩
(2nd “ 𝐴)∃𝑗 ∈ Q 𝑤 <Q 𝑗) |
60 | | rexcom 2634 |
. . . . . 6
⊢
(∃𝑤 ∈
∩ (2nd “ 𝐴)∃𝑗 ∈ Q 𝑤 <Q 𝑗 ↔ ∃𝑗 ∈ Q
∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑗) |
61 | 59, 60 | sylib 121 |
. . . . 5
⊢ ((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑠 ∈ ∩ (2nd “ 𝐴))) → ∃𝑗 ∈ Q ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑗) |
62 | | ssid 3167 |
. . . . . 6
⊢
Q ⊆ Q |
63 | | rexss 3214 |
. . . . . 6
⊢
(Q ⊆ Q → (∃𝑗 ∈ Q
∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑗 ↔ ∃𝑗 ∈ Q (𝑗 ∈ Q ∧
∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑗))) |
64 | 62, 63 | ax-mp 5 |
. . . . 5
⊢
(∃𝑗 ∈
Q ∃𝑤
∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑗 ↔ ∃𝑗 ∈ Q (𝑗 ∈ Q ∧
∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑗)) |
65 | 61, 64 | sylib 121 |
. . . 4
⊢ ((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑠 ∈ ∩ (2nd “ 𝐴))) → ∃𝑗 ∈ Q (𝑗 ∈ Q ∧ ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑗)) |
66 | | suplocexpr.b |
. . . . . . . . . 10
⊢ 𝐵 = 〈∪ (1st “ 𝐴), {𝑢 ∈ Q ∣ ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑢}〉 |
67 | 66 | suplocexprlem2b 7676 |
. . . . . . . . 9
⊢ (𝐴 ⊆ P →
(2nd ‘𝐵) =
{𝑢 ∈ Q
∣ ∃𝑤 ∈
∩ (2nd “ 𝐴)𝑤 <Q 𝑢}) |
68 | 14, 67 | syl 14 |
. . . . . . . 8
⊢ (𝜑 → (2nd
‘𝐵) = {𝑢 ∈ Q ∣
∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑢}) |
69 | 68 | eleq2d 2240 |
. . . . . . 7
⊢ (𝜑 → (𝑗 ∈ (2nd ‘𝐵) ↔ 𝑗 ∈ {𝑢 ∈ Q ∣ ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑢})) |
70 | | breq2 3993 |
. . . . . . . . 9
⊢ (𝑢 = 𝑗 → (𝑤 <Q 𝑢 ↔ 𝑤 <Q 𝑗)) |
71 | 70 | rexbidv 2471 |
. . . . . . . 8
⊢ (𝑢 = 𝑗 → (∃𝑤 ∈ ∩
(2nd “ 𝐴)𝑤 <Q 𝑢 ↔ ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑗)) |
72 | 71 | elrab 2886 |
. . . . . . 7
⊢ (𝑗 ∈ {𝑢 ∈ Q ∣ ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑢} ↔ (𝑗 ∈ Q ∧ ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑗)) |
73 | 69, 72 | bitrdi 195 |
. . . . . 6
⊢ (𝜑 → (𝑗 ∈ (2nd ‘𝐵) ↔ (𝑗 ∈ Q ∧ ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑗))) |
74 | 73 | rexbidv 2471 |
. . . . 5
⊢ (𝜑 → (∃𝑗 ∈ Q 𝑗 ∈ (2nd ‘𝐵) ↔ ∃𝑗 ∈ Q (𝑗 ∈ Q ∧
∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑗))) |
75 | 74 | adantr 274 |
. . . 4
⊢ ((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑠 ∈ ∩ (2nd “ 𝐴))) → (∃𝑗 ∈ Q 𝑗 ∈ (2nd ‘𝐵) ↔ ∃𝑗 ∈ Q (𝑗 ∈ Q ∧
∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑗))) |
76 | 65, 75 | mpbird 166 |
. . 3
⊢ ((𝜑 ∧ (𝑠 ∈ Q ∧ 𝑠 ∈ ∩ (2nd “ 𝐴))) → ∃𝑗 ∈ Q 𝑗 ∈ (2nd ‘𝐵)) |
77 | 45, 76 | rexlimddv 2592 |
. 2
⊢ (𝜑 → ∃𝑗 ∈ Q 𝑗 ∈ (2nd ‘𝐵)) |
78 | | eleq1w 2231 |
. . 3
⊢ (𝑗 = 𝑠 → (𝑗 ∈ (2nd ‘𝐵) ↔ 𝑠 ∈ (2nd ‘𝐵))) |
79 | 78 | cbvrexv 2697 |
. 2
⊢
(∃𝑗 ∈
Q 𝑗 ∈
(2nd ‘𝐵)
↔ ∃𝑠 ∈
Q 𝑠 ∈
(2nd ‘𝐵)) |
80 | 77, 79 | sylib 121 |
1
⊢ (𝜑 → ∃𝑠 ∈ Q 𝑠 ∈ (2nd ‘𝐵)) |