Step | Hyp | Ref
| Expression |
1 | | suplocexpr.m |
. . 3
⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴) |
2 | | suplocexpr.ub |
. . 3
⊢ (𝜑 → ∃𝑥 ∈ P ∀𝑦 ∈ 𝐴 𝑦<P 𝑥) |
3 | | suplocexpr.loc |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ P ∀𝑦 ∈ P (𝑥<P
𝑦 → (∃𝑧 ∈ 𝐴 𝑥<P 𝑧 ∨ ∀𝑧 ∈ 𝐴 𝑧<P 𝑦))) |
4 | | breq1 3992 |
. . . . . 6
⊢ (𝑎 = 𝑤 → (𝑎 <Q 𝑢 ↔ 𝑤 <Q 𝑢)) |
5 | 4 | cbvrexv 2697 |
. . . . 5
⊢
(∃𝑎 ∈
∩ (2nd “ 𝐴)𝑎 <Q 𝑢 ↔ ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑢) |
6 | 5 | rabbii 2716 |
. . . 4
⊢ {𝑢 ∈ Q ∣
∃𝑎 ∈ ∩ (2nd “ 𝐴)𝑎 <Q 𝑢} = {𝑢 ∈ Q ∣ ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑢} |
7 | 6 | opeq2i 3769 |
. . 3
⊢
〈∪ (1st “ 𝐴), {𝑢 ∈ Q ∣ ∃𝑎 ∈ ∩ (2nd “ 𝐴)𝑎 <Q 𝑢}〉 = 〈∪ (1st “ 𝐴), {𝑢 ∈ Q ∣ ∃𝑤 ∈ ∩ (2nd “ 𝐴)𝑤 <Q 𝑢}〉 |
8 | 1, 2, 3, 7 | suplocexprlemex 7684 |
. 2
⊢ (𝜑 → 〈∪ (1st “ 𝐴), {𝑢 ∈ Q ∣ ∃𝑎 ∈ ∩ (2nd “ 𝐴)𝑎 <Q 𝑢}〉 ∈
P) |
9 | 1, 2, 3, 7 | suplocexprlemub 7685 |
. 2
⊢ (𝜑 → ∀𝑦 ∈ 𝐴 ¬ 〈∪
(1st “ 𝐴),
{𝑢 ∈ Q
∣ ∃𝑎 ∈
∩ (2nd “ 𝐴)𝑎 <Q 𝑢}〉<P 𝑦) |
10 | 1, 2, 3, 7 | suplocexprlemlub 7686 |
. . 3
⊢ (𝜑 → (𝑦<P 〈∪ (1st “ 𝐴), {𝑢 ∈ Q ∣ ∃𝑎 ∈ ∩ (2nd “ 𝐴)𝑎 <Q 𝑢}〉 → ∃𝑧 ∈ 𝐴 𝑦<P 𝑧)) |
11 | 10 | ralrimivw 2544 |
. 2
⊢ (𝜑 → ∀𝑦 ∈ P (𝑦<P 〈∪ (1st “ 𝐴), {𝑢 ∈ Q ∣ ∃𝑎 ∈ ∩ (2nd “ 𝐴)𝑎 <Q 𝑢}〉 → ∃𝑧 ∈ 𝐴 𝑦<P 𝑧)) |
12 | | breq1 3992 |
. . . . . 6
⊢ (𝑥 = 〈∪ (1st “ 𝐴), {𝑢 ∈ Q ∣ ∃𝑎 ∈ ∩ (2nd “ 𝐴)𝑎 <Q 𝑢}〉 → (𝑥<P
𝑦 ↔ 〈∪ (1st “ 𝐴), {𝑢 ∈ Q ∣ ∃𝑎 ∈ ∩ (2nd “ 𝐴)𝑎 <Q 𝑢}〉<P 𝑦)) |
13 | 12 | notbid 662 |
. . . . 5
⊢ (𝑥 = 〈∪ (1st “ 𝐴), {𝑢 ∈ Q ∣ ∃𝑎 ∈ ∩ (2nd “ 𝐴)𝑎 <Q 𝑢}〉 → (¬ 𝑥<P
𝑦 ↔ ¬ 〈∪ (1st “ 𝐴), {𝑢 ∈ Q ∣ ∃𝑎 ∈ ∩ (2nd “ 𝐴)𝑎 <Q 𝑢}〉<P 𝑦)) |
14 | 13 | ralbidv 2470 |
. . . 4
⊢ (𝑥 = 〈∪ (1st “ 𝐴), {𝑢 ∈ Q ∣ ∃𝑎 ∈ ∩ (2nd “ 𝐴)𝑎 <Q 𝑢}〉 → (∀𝑦 ∈ 𝐴 ¬ 𝑥<P 𝑦 ↔ ∀𝑦 ∈ 𝐴 ¬ 〈∪
(1st “ 𝐴),
{𝑢 ∈ Q
∣ ∃𝑎 ∈
∩ (2nd “ 𝐴)𝑎 <Q 𝑢}〉<P 𝑦)) |
15 | | breq2 3993 |
. . . . . 6
⊢ (𝑥 = 〈∪ (1st “ 𝐴), {𝑢 ∈ Q ∣ ∃𝑎 ∈ ∩ (2nd “ 𝐴)𝑎 <Q 𝑢}〉 → (𝑦<P
𝑥 ↔ 𝑦<P 〈∪ (1st “ 𝐴), {𝑢 ∈ Q ∣ ∃𝑎 ∈ ∩ (2nd “ 𝐴)𝑎 <Q 𝑢}〉)) |
16 | 15 | imbi1d 230 |
. . . . 5
⊢ (𝑥 = 〈∪ (1st “ 𝐴), {𝑢 ∈ Q ∣ ∃𝑎 ∈ ∩ (2nd “ 𝐴)𝑎 <Q 𝑢}〉 → ((𝑦<P
𝑥 → ∃𝑧 ∈ 𝐴 𝑦<P 𝑧) ↔ (𝑦<P 〈∪ (1st “ 𝐴), {𝑢 ∈ Q ∣ ∃𝑎 ∈ ∩ (2nd “ 𝐴)𝑎 <Q 𝑢}〉 → ∃𝑧 ∈ 𝐴 𝑦<P 𝑧))) |
17 | 16 | ralbidv 2470 |
. . . 4
⊢ (𝑥 = 〈∪ (1st “ 𝐴), {𝑢 ∈ Q ∣ ∃𝑎 ∈ ∩ (2nd “ 𝐴)𝑎 <Q 𝑢}〉 → (∀𝑦 ∈ P (𝑦<P
𝑥 → ∃𝑧 ∈ 𝐴 𝑦<P 𝑧) ↔ ∀𝑦 ∈ P (𝑦<P
〈∪ (1st “ 𝐴), {𝑢 ∈ Q ∣ ∃𝑎 ∈ ∩ (2nd “ 𝐴)𝑎 <Q 𝑢}〉 → ∃𝑧 ∈ 𝐴 𝑦<P 𝑧))) |
18 | 14, 17 | anbi12d 470 |
. . 3
⊢ (𝑥 = 〈∪ (1st “ 𝐴), {𝑢 ∈ Q ∣ ∃𝑎 ∈ ∩ (2nd “ 𝐴)𝑎 <Q 𝑢}〉 → ((∀𝑦 ∈ 𝐴 ¬ 𝑥<P 𝑦 ∧ ∀𝑦 ∈ P (𝑦<P
𝑥 → ∃𝑧 ∈ 𝐴 𝑦<P 𝑧)) ↔ (∀𝑦 ∈ 𝐴 ¬ 〈∪
(1st “ 𝐴),
{𝑢 ∈ Q
∣ ∃𝑎 ∈
∩ (2nd “ 𝐴)𝑎 <Q 𝑢}〉<P 𝑦 ∧ ∀𝑦 ∈ P (𝑦<P
〈∪ (1st “ 𝐴), {𝑢 ∈ Q ∣ ∃𝑎 ∈ ∩ (2nd “ 𝐴)𝑎 <Q 𝑢}〉 → ∃𝑧 ∈ 𝐴 𝑦<P 𝑧)))) |
19 | 18 | rspcev 2834 |
. 2
⊢
((〈∪ (1st “ 𝐴), {𝑢 ∈ Q ∣ ∃𝑎 ∈ ∩ (2nd “ 𝐴)𝑎 <Q 𝑢}〉 ∈ P
∧ (∀𝑦 ∈
𝐴 ¬ 〈∪ (1st “ 𝐴), {𝑢 ∈ Q ∣ ∃𝑎 ∈ ∩ (2nd “ 𝐴)𝑎 <Q 𝑢}〉<P 𝑦 ∧ ∀𝑦 ∈ P (𝑦<P
〈∪ (1st “ 𝐴), {𝑢 ∈ Q ∣ ∃𝑎 ∈ ∩ (2nd “ 𝐴)𝑎 <Q 𝑢}〉 → ∃𝑧 ∈ 𝐴 𝑦<P 𝑧))) → ∃𝑥 ∈ P
(∀𝑦 ∈ 𝐴 ¬ 𝑥<P 𝑦 ∧ ∀𝑦 ∈ P (𝑦<P
𝑥 → ∃𝑧 ∈ 𝐴 𝑦<P 𝑧))) |
20 | 8, 9, 11, 19 | syl12anc 1231 |
1
⊢ (𝜑 → ∃𝑥 ∈ P (∀𝑦 ∈ 𝐴 ¬ 𝑥<P 𝑦 ∧ ∀𝑦 ∈ P (𝑦<P
𝑥 → ∃𝑧 ∈ 𝐴 𝑦<P 𝑧))) |