Step | Hyp | Ref
| Expression |
1 | | safesnsupfilb.ordered |
. . . . . . 7
⊢ (𝜑 → 𝑅 Or 𝐴) |
2 | 1 | ad2antrr 725 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑂 ≺ 𝐵) ∧ 𝑥 ∈ 𝐵) → 𝑅 Or 𝐴) |
3 | | safesnsupfilb.subset |
. . . . . . 7
⊢ (𝜑 → 𝐵 ⊆ 𝐴) |
4 | 3 | ad2antrr 725 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑂 ≺ 𝐵) ∧ 𝑥 ∈ 𝐵) → 𝐵 ⊆ 𝐴) |
5 | | safesnsupfilb.finite |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ Fin) |
6 | 5 | ad2antrr 725 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑂 ≺ 𝐵) ∧ 𝑥 ∈ 𝐵) → 𝐵 ∈ Fin) |
7 | | simpr 486 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑂 ≺ 𝐵) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐵) |
8 | | eqidd 2738 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑂 ≺ 𝐵) ∧ 𝑥 ∈ 𝐵) → sup(𝐵, 𝐴, 𝑅) = sup(𝐵, 𝐴, 𝑅)) |
9 | 2, 4, 6, 7, 8 | supgtoreq 9413 |
. . . . 5
⊢ (((𝜑 ∧ 𝑂 ≺ 𝐵) ∧ 𝑥 ∈ 𝐵) → (𝑥𝑅sup(𝐵, 𝐴, 𝑅) ∨ 𝑥 = sup(𝐵, 𝐴, 𝑅))) |
10 | | df-or 847 |
. . . . . 6
⊢ ((𝑥 = sup(𝐵, 𝐴, 𝑅) ∨ 𝑥𝑅sup(𝐵, 𝐴, 𝑅)) ↔ (¬ 𝑥 = sup(𝐵, 𝐴, 𝑅) → 𝑥𝑅sup(𝐵, 𝐴, 𝑅))) |
11 | | orcom 869 |
. . . . . 6
⊢ ((𝑥𝑅sup(𝐵, 𝐴, 𝑅) ∨ 𝑥 = sup(𝐵, 𝐴, 𝑅)) ↔ (𝑥 = sup(𝐵, 𝐴, 𝑅) ∨ 𝑥𝑅sup(𝐵, 𝐴, 𝑅))) |
12 | | df-ne 2945 |
. . . . . . 7
⊢ (𝑥 ≠ sup(𝐵, 𝐴, 𝑅) ↔ ¬ 𝑥 = sup(𝐵, 𝐴, 𝑅)) |
13 | 12 | imbi1i 350 |
. . . . . 6
⊢ ((𝑥 ≠ sup(𝐵, 𝐴, 𝑅) → 𝑥𝑅sup(𝐵, 𝐴, 𝑅)) ↔ (¬ 𝑥 = sup(𝐵, 𝐴, 𝑅) → 𝑥𝑅sup(𝐵, 𝐴, 𝑅))) |
14 | 10, 11, 13 | 3bitr4i 303 |
. . . . 5
⊢ ((𝑥𝑅sup(𝐵, 𝐴, 𝑅) ∨ 𝑥 = sup(𝐵, 𝐴, 𝑅)) ↔ (𝑥 ≠ sup(𝐵, 𝐴, 𝑅) → 𝑥𝑅sup(𝐵, 𝐴, 𝑅))) |
15 | 9, 14 | sylib 217 |
. . . 4
⊢ (((𝜑 ∧ 𝑂 ≺ 𝐵) ∧ 𝑥 ∈ 𝐵) → (𝑥 ≠ sup(𝐵, 𝐴, 𝑅) → 𝑥𝑅sup(𝐵, 𝐴, 𝑅))) |
16 | 15 | ralrimiva 3144 |
. . 3
⊢ ((𝜑 ∧ 𝑂 ≺ 𝐵) → ∀𝑥 ∈ 𝐵 (𝑥 ≠ sup(𝐵, 𝐴, 𝑅) → 𝑥𝑅sup(𝐵, 𝐴, 𝑅))) |
17 | | iftrue 4497 |
. . . . . . 7
⊢ (𝑂 ≺ 𝐵 → if(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵) = {sup(𝐵, 𝐴, 𝑅)}) |
18 | 17 | difeq2d 4087 |
. . . . . 6
⊢ (𝑂 ≺ 𝐵 → (𝐵 ∖ if(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵)) = (𝐵 ∖ {sup(𝐵, 𝐴, 𝑅)})) |
19 | 18 | adantl 483 |
. . . . 5
⊢ ((𝜑 ∧ 𝑂 ≺ 𝐵) → (𝐵 ∖ if(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵)) = (𝐵 ∖ {sup(𝐵, 𝐴, 𝑅)})) |
20 | 19 | raleqdv 3316 |
. . . 4
⊢ ((𝜑 ∧ 𝑂 ≺ 𝐵) → (∀𝑥 ∈ (𝐵 ∖ if(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵))∀𝑦 ∈ if (𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵)𝑥𝑅𝑦 ↔ ∀𝑥 ∈ (𝐵 ∖ {sup(𝐵, 𝐴, 𝑅)})∀𝑦 ∈ if (𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵)𝑥𝑅𝑦)) |
21 | | simpr 486 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑂 ≺ 𝐵) → 𝑂 ≺ 𝐵) |
22 | 21 | iftrued 4499 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑂 ≺ 𝐵) → if(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵) = {sup(𝐵, 𝐴, 𝑅)}) |
23 | 22 | raleqdv 3316 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑂 ≺ 𝐵) → (∀𝑦 ∈ if (𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵)𝑥𝑅𝑦 ↔ ∀𝑦 ∈ {sup(𝐵, 𝐴, 𝑅)}𝑥𝑅𝑦)) |
24 | 5 | adantr 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑂 ≺ 𝐵) → 𝐵 ∈ Fin) |
25 | | safesnsupfilb.small |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑂 = ∅ ∨ 𝑂 = 1o)) |
26 | 25 | adantr 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑂 ≺ 𝐵) → (𝑂 = ∅ ∨ 𝑂 = 1o)) |
27 | | 0elon 6376 |
. . . . . . . . . . . . . 14
⊢ ∅
∈ On |
28 | | eleq1 2826 |
. . . . . . . . . . . . . 14
⊢ (𝑂 = ∅ → (𝑂 ∈ On ↔ ∅ ∈
On)) |
29 | 27, 28 | mpbiri 258 |
. . . . . . . . . . . . 13
⊢ (𝑂 = ∅ → 𝑂 ∈ On) |
30 | | 1on 8429 |
. . . . . . . . . . . . . 14
⊢
1o ∈ On |
31 | | eleq1 2826 |
. . . . . . . . . . . . . 14
⊢ (𝑂 = 1o → (𝑂 ∈ On ↔ 1o
∈ On)) |
32 | 30, 31 | mpbiri 258 |
. . . . . . . . . . . . 13
⊢ (𝑂 = 1o → 𝑂 ∈ On) |
33 | 29, 32 | jaoi 856 |
. . . . . . . . . . . 12
⊢ ((𝑂 = ∅ ∨ 𝑂 = 1o) → 𝑂 ∈ On) |
34 | 26, 33 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑂 ≺ 𝐵) → 𝑂 ∈ On) |
35 | 21, 34 | sdomne0d 41760 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑂 ≺ 𝐵) → 𝐵 ≠ ∅) |
36 | 3 | adantr 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑂 ≺ 𝐵) → 𝐵 ⊆ 𝐴) |
37 | 24, 35, 36 | 3jca 1129 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑂 ≺ 𝐵) → (𝐵 ∈ Fin ∧ 𝐵 ≠ ∅ ∧ 𝐵 ⊆ 𝐴)) |
38 | | fisupcl 9412 |
. . . . . . . . 9
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ Fin ∧ 𝐵 ≠ ∅ ∧ 𝐵 ⊆ 𝐴)) → sup(𝐵, 𝐴, 𝑅) ∈ 𝐵) |
39 | 1, 37, 38 | syl2an2r 684 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑂 ≺ 𝐵) → sup(𝐵, 𝐴, 𝑅) ∈ 𝐵) |
40 | | breq2 5114 |
. . . . . . . . 9
⊢ (𝑦 = sup(𝐵, 𝐴, 𝑅) → (𝑥𝑅𝑦 ↔ 𝑥𝑅sup(𝐵, 𝐴, 𝑅))) |
41 | 40 | ralsng 4639 |
. . . . . . . 8
⊢
(sup(𝐵, 𝐴, 𝑅) ∈ 𝐵 → (∀𝑦 ∈ {sup(𝐵, 𝐴, 𝑅)}𝑥𝑅𝑦 ↔ 𝑥𝑅sup(𝐵, 𝐴, 𝑅))) |
42 | 39, 41 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑂 ≺ 𝐵) → (∀𝑦 ∈ {sup(𝐵, 𝐴, 𝑅)}𝑥𝑅𝑦 ↔ 𝑥𝑅sup(𝐵, 𝐴, 𝑅))) |
43 | 23, 42 | bitrd 279 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑂 ≺ 𝐵) → (∀𝑦 ∈ if (𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵)𝑥𝑅𝑦 ↔ 𝑥𝑅sup(𝐵, 𝐴, 𝑅))) |
44 | 43 | ralbidv 3175 |
. . . . 5
⊢ ((𝜑 ∧ 𝑂 ≺ 𝐵) → (∀𝑥 ∈ (𝐵 ∖ {sup(𝐵, 𝐴, 𝑅)})∀𝑦 ∈ if (𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵)𝑥𝑅𝑦 ↔ ∀𝑥 ∈ (𝐵 ∖ {sup(𝐵, 𝐴, 𝑅)})𝑥𝑅sup(𝐵, 𝐴, 𝑅))) |
45 | | raldifsnb 4761 |
. . . . 5
⊢
(∀𝑥 ∈
𝐵 (𝑥 ≠ sup(𝐵, 𝐴, 𝑅) → 𝑥𝑅sup(𝐵, 𝐴, 𝑅)) ↔ ∀𝑥 ∈ (𝐵 ∖ {sup(𝐵, 𝐴, 𝑅)})𝑥𝑅sup(𝐵, 𝐴, 𝑅)) |
46 | 44, 45 | bitr4di 289 |
. . . 4
⊢ ((𝜑 ∧ 𝑂 ≺ 𝐵) → (∀𝑥 ∈ (𝐵 ∖ {sup(𝐵, 𝐴, 𝑅)})∀𝑦 ∈ if (𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵)𝑥𝑅𝑦 ↔ ∀𝑥 ∈ 𝐵 (𝑥 ≠ sup(𝐵, 𝐴, 𝑅) → 𝑥𝑅sup(𝐵, 𝐴, 𝑅)))) |
47 | 20, 46 | bitrd 279 |
. . 3
⊢ ((𝜑 ∧ 𝑂 ≺ 𝐵) → (∀𝑥 ∈ (𝐵 ∖ if(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵))∀𝑦 ∈ if (𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵)𝑥𝑅𝑦 ↔ ∀𝑥 ∈ 𝐵 (𝑥 ≠ sup(𝐵, 𝐴, 𝑅) → 𝑥𝑅sup(𝐵, 𝐴, 𝑅)))) |
48 | 16, 47 | mpbird 257 |
. 2
⊢ ((𝜑 ∧ 𝑂 ≺ 𝐵) → ∀𝑥 ∈ (𝐵 ∖ if(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵))∀𝑦 ∈ if (𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵)𝑥𝑅𝑦) |
49 | | ral0 4475 |
. . 3
⊢
∀𝑥 ∈
∅ ∀𝑦 ∈ if
(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵)𝑥𝑅𝑦 |
50 | | iffalse 4500 |
. . . . . . 7
⊢ (¬
𝑂 ≺ 𝐵 → if(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵) = 𝐵) |
51 | 50 | adantl 483 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝑂 ≺ 𝐵) → if(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵) = 𝐵) |
52 | 51 | difeq2d 4087 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝑂 ≺ 𝐵) → (𝐵 ∖ if(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵)) = (𝐵 ∖ 𝐵)) |
53 | | difid 4335 |
. . . . 5
⊢ (𝐵 ∖ 𝐵) = ∅ |
54 | 52, 53 | eqtrdi 2793 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑂 ≺ 𝐵) → (𝐵 ∖ if(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵)) = ∅) |
55 | 54 | raleqdv 3316 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑂 ≺ 𝐵) → (∀𝑥 ∈ (𝐵 ∖ if(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵))∀𝑦 ∈ if (𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵)𝑥𝑅𝑦 ↔ ∀𝑥 ∈ ∅ ∀𝑦 ∈ if (𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵)𝑥𝑅𝑦)) |
56 | 49, 55 | mpbiri 258 |
. 2
⊢ ((𝜑 ∧ ¬ 𝑂 ≺ 𝐵) → ∀𝑥 ∈ (𝐵 ∖ if(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵))∀𝑦 ∈ if (𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵)𝑥𝑅𝑦) |
57 | 48, 56 | pm2.61dan 812 |
1
⊢ (𝜑 → ∀𝑥 ∈ (𝐵 ∖ if(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵))∀𝑦 ∈ if (𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵)𝑥𝑅𝑦) |