Proof of Theorem safesnsupfilb
| Step | Hyp | Ref
| Expression |
| 1 | | safesnsupfilb.ordered |
. . . . . . 7
⊢ (𝜑 → 𝑅 Or 𝐴) |
| 2 | 1 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑂 ≺ 𝐵) ∧ 𝑥 ∈ 𝐵) → 𝑅 Or 𝐴) |
| 3 | | safesnsupfilb.subset |
. . . . . . 7
⊢ (𝜑 → 𝐵 ⊆ 𝐴) |
| 4 | 3 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑂 ≺ 𝐵) ∧ 𝑥 ∈ 𝐵) → 𝐵 ⊆ 𝐴) |
| 5 | | safesnsupfilb.finite |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ Fin) |
| 6 | 5 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑂 ≺ 𝐵) ∧ 𝑥 ∈ 𝐵) → 𝐵 ∈ Fin) |
| 7 | | simpr 484 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑂 ≺ 𝐵) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐵) |
| 8 | | eqidd 2738 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑂 ≺ 𝐵) ∧ 𝑥 ∈ 𝐵) → sup(𝐵, 𝐴, 𝑅) = sup(𝐵, 𝐴, 𝑅)) |
| 9 | 2, 4, 6, 7, 8 | supgtoreq 9510 |
. . . . 5
⊢ (((𝜑 ∧ 𝑂 ≺ 𝐵) ∧ 𝑥 ∈ 𝐵) → (𝑥𝑅sup(𝐵, 𝐴, 𝑅) ∨ 𝑥 = sup(𝐵, 𝐴, 𝑅))) |
| 10 | | df-or 849 |
. . . . . 6
⊢ ((𝑥 = sup(𝐵, 𝐴, 𝑅) ∨ 𝑥𝑅sup(𝐵, 𝐴, 𝑅)) ↔ (¬ 𝑥 = sup(𝐵, 𝐴, 𝑅) → 𝑥𝑅sup(𝐵, 𝐴, 𝑅))) |
| 11 | | orcom 871 |
. . . . . 6
⊢ ((𝑥𝑅sup(𝐵, 𝐴, 𝑅) ∨ 𝑥 = sup(𝐵, 𝐴, 𝑅)) ↔ (𝑥 = sup(𝐵, 𝐴, 𝑅) ∨ 𝑥𝑅sup(𝐵, 𝐴, 𝑅))) |
| 12 | | df-ne 2941 |
. . . . . . 7
⊢ (𝑥 ≠ sup(𝐵, 𝐴, 𝑅) ↔ ¬ 𝑥 = sup(𝐵, 𝐴, 𝑅)) |
| 13 | 12 | imbi1i 349 |
. . . . . 6
⊢ ((𝑥 ≠ sup(𝐵, 𝐴, 𝑅) → 𝑥𝑅sup(𝐵, 𝐴, 𝑅)) ↔ (¬ 𝑥 = sup(𝐵, 𝐴, 𝑅) → 𝑥𝑅sup(𝐵, 𝐴, 𝑅))) |
| 14 | 10, 11, 13 | 3bitr4i 303 |
. . . . 5
⊢ ((𝑥𝑅sup(𝐵, 𝐴, 𝑅) ∨ 𝑥 = sup(𝐵, 𝐴, 𝑅)) ↔ (𝑥 ≠ sup(𝐵, 𝐴, 𝑅) → 𝑥𝑅sup(𝐵, 𝐴, 𝑅))) |
| 15 | 9, 14 | sylib 218 |
. . . 4
⊢ (((𝜑 ∧ 𝑂 ≺ 𝐵) ∧ 𝑥 ∈ 𝐵) → (𝑥 ≠ sup(𝐵, 𝐴, 𝑅) → 𝑥𝑅sup(𝐵, 𝐴, 𝑅))) |
| 16 | 15 | ralrimiva 3146 |
. . 3
⊢ ((𝜑 ∧ 𝑂 ≺ 𝐵) → ∀𝑥 ∈ 𝐵 (𝑥 ≠ sup(𝐵, 𝐴, 𝑅) → 𝑥𝑅sup(𝐵, 𝐴, 𝑅))) |
| 17 | | iftrue 4531 |
. . . . . . 7
⊢ (𝑂 ≺ 𝐵 → if(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵) = {sup(𝐵, 𝐴, 𝑅)}) |
| 18 | 17 | difeq2d 4126 |
. . . . . 6
⊢ (𝑂 ≺ 𝐵 → (𝐵 ∖ if(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵)) = (𝐵 ∖ {sup(𝐵, 𝐴, 𝑅)})) |
| 19 | 18 | adantl 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑂 ≺ 𝐵) → (𝐵 ∖ if(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵)) = (𝐵 ∖ {sup(𝐵, 𝐴, 𝑅)})) |
| 20 | 19 | raleqdv 3326 |
. . . 4
⊢ ((𝜑 ∧ 𝑂 ≺ 𝐵) → (∀𝑥 ∈ (𝐵 ∖ if(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵))∀𝑦 ∈ if (𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵)𝑥𝑅𝑦 ↔ ∀𝑥 ∈ (𝐵 ∖ {sup(𝐵, 𝐴, 𝑅)})∀𝑦 ∈ if (𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵)𝑥𝑅𝑦)) |
| 21 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑂 ≺ 𝐵) → 𝑂 ≺ 𝐵) |
| 22 | 21 | iftrued 4533 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑂 ≺ 𝐵) → if(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵) = {sup(𝐵, 𝐴, 𝑅)}) |
| 23 | 22 | raleqdv 3326 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑂 ≺ 𝐵) → (∀𝑦 ∈ if (𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵)𝑥𝑅𝑦 ↔ ∀𝑦 ∈ {sup(𝐵, 𝐴, 𝑅)}𝑥𝑅𝑦)) |
| 24 | 5 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑂 ≺ 𝐵) → 𝐵 ∈ Fin) |
| 25 | | safesnsupfilb.small |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑂 = ∅ ∨ 𝑂 = 1o)) |
| 26 | 25 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑂 ≺ 𝐵) → (𝑂 = ∅ ∨ 𝑂 = 1o)) |
| 27 | | 0elon 6438 |
. . . . . . . . . . . . . 14
⊢ ∅
∈ On |
| 28 | | eleq1 2829 |
. . . . . . . . . . . . . 14
⊢ (𝑂 = ∅ → (𝑂 ∈ On ↔ ∅ ∈
On)) |
| 29 | 27, 28 | mpbiri 258 |
. . . . . . . . . . . . 13
⊢ (𝑂 = ∅ → 𝑂 ∈ On) |
| 30 | | 1on 8518 |
. . . . . . . . . . . . . 14
⊢
1o ∈ On |
| 31 | | eleq1 2829 |
. . . . . . . . . . . . . 14
⊢ (𝑂 = 1o → (𝑂 ∈ On ↔ 1o
∈ On)) |
| 32 | 30, 31 | mpbiri 258 |
. . . . . . . . . . . . 13
⊢ (𝑂 = 1o → 𝑂 ∈ On) |
| 33 | 29, 32 | jaoi 858 |
. . . . . . . . . . . 12
⊢ ((𝑂 = ∅ ∨ 𝑂 = 1o) → 𝑂 ∈ On) |
| 34 | 26, 33 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑂 ≺ 𝐵) → 𝑂 ∈ On) |
| 35 | 21, 34 | sdomne0d 43427 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑂 ≺ 𝐵) → 𝐵 ≠ ∅) |
| 36 | 3 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑂 ≺ 𝐵) → 𝐵 ⊆ 𝐴) |
| 37 | 24, 35, 36 | 3jca 1129 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑂 ≺ 𝐵) → (𝐵 ∈ Fin ∧ 𝐵 ≠ ∅ ∧ 𝐵 ⊆ 𝐴)) |
| 38 | | fisupcl 9509 |
. . . . . . . . 9
⊢ ((𝑅 Or 𝐴 ∧ (𝐵 ∈ Fin ∧ 𝐵 ≠ ∅ ∧ 𝐵 ⊆ 𝐴)) → sup(𝐵, 𝐴, 𝑅) ∈ 𝐵) |
| 39 | 1, 37, 38 | syl2an2r 685 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑂 ≺ 𝐵) → sup(𝐵, 𝐴, 𝑅) ∈ 𝐵) |
| 40 | | breq2 5147 |
. . . . . . . . 9
⊢ (𝑦 = sup(𝐵, 𝐴, 𝑅) → (𝑥𝑅𝑦 ↔ 𝑥𝑅sup(𝐵, 𝐴, 𝑅))) |
| 41 | 40 | ralsng 4675 |
. . . . . . . 8
⊢
(sup(𝐵, 𝐴, 𝑅) ∈ 𝐵 → (∀𝑦 ∈ {sup(𝐵, 𝐴, 𝑅)}𝑥𝑅𝑦 ↔ 𝑥𝑅sup(𝐵, 𝐴, 𝑅))) |
| 42 | 39, 41 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑂 ≺ 𝐵) → (∀𝑦 ∈ {sup(𝐵, 𝐴, 𝑅)}𝑥𝑅𝑦 ↔ 𝑥𝑅sup(𝐵, 𝐴, 𝑅))) |
| 43 | 23, 42 | bitrd 279 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑂 ≺ 𝐵) → (∀𝑦 ∈ if (𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵)𝑥𝑅𝑦 ↔ 𝑥𝑅sup(𝐵, 𝐴, 𝑅))) |
| 44 | 43 | ralbidv 3178 |
. . . . 5
⊢ ((𝜑 ∧ 𝑂 ≺ 𝐵) → (∀𝑥 ∈ (𝐵 ∖ {sup(𝐵, 𝐴, 𝑅)})∀𝑦 ∈ if (𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵)𝑥𝑅𝑦 ↔ ∀𝑥 ∈ (𝐵 ∖ {sup(𝐵, 𝐴, 𝑅)})𝑥𝑅sup(𝐵, 𝐴, 𝑅))) |
| 45 | | raldifsnb 4796 |
. . . . 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 4513 |
. . 3
⊢
∀𝑥 ∈
∅ ∀𝑦 ∈ if
(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵)𝑥𝑅𝑦 |
| 50 | | iffalse 4534 |
. . . . . . 7
⊢ (¬
𝑂 ≺ 𝐵 → if(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵) = 𝐵) |
| 51 | 50 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ ¬ 𝑂 ≺ 𝐵) → if(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵) = 𝐵) |
| 52 | 51 | difeq2d 4126 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝑂 ≺ 𝐵) → (𝐵 ∖ if(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵)) = (𝐵 ∖ 𝐵)) |
| 53 | | difid 4376 |
. . . . 5
⊢ (𝐵 ∖ 𝐵) = ∅ |
| 54 | 52, 53 | eqtrdi 2793 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝑂 ≺ 𝐵) → (𝐵 ∖ if(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵)) = ∅) |
| 55 | 54 | raleqdv 3326 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑂 ≺ 𝐵) → (∀𝑥 ∈ (𝐵 ∖ if(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵))∀𝑦 ∈ if (𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵)𝑥𝑅𝑦 ↔ ∀𝑥 ∈ ∅ ∀𝑦 ∈ if (𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵)𝑥𝑅𝑦)) |
| 56 | 49, 55 | mpbiri 258 |
. 2
⊢ ((𝜑 ∧ ¬ 𝑂 ≺ 𝐵) → ∀𝑥 ∈ (𝐵 ∖ if(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵))∀𝑦 ∈ if (𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵)𝑥𝑅𝑦) |
| 57 | 48, 56 | pm2.61dan 813 |
1
⊢ (𝜑 → ∀𝑥 ∈ (𝐵 ∖ if(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵))∀𝑦 ∈ if (𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵)𝑥𝑅𝑦) |