Proof of Theorem safesnsupfidom1o
| Step | Hyp | Ref
| Expression |
| 1 | | iftrue 4531 |
. . . 4
⊢ (𝑂 ≺ 𝐵 → if(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵) = {sup(𝐵, 𝐴, 𝑅)}) |
| 2 | 1 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ 𝑂 ≺ 𝐵) → if(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵) = {sup(𝐵, 𝐴, 𝑅)}) |
| 3 | | ensn1g 9062 |
. . . . 5
⊢
(sup(𝐵, 𝐴, 𝑅) ∈ V → {sup(𝐵, 𝐴, 𝑅)} ≈ 1o) |
| 4 | | 1on 8518 |
. . . . . 6
⊢
1o ∈ On |
| 5 | | domrefg 9027 |
. . . . . 6
⊢
(1o ∈ On → 1o ≼
1o) |
| 6 | 4, 5 | ax-mp 5 |
. . . . 5
⊢
1o ≼ 1o |
| 7 | | endomtr 9052 |
. . . . 5
⊢
(({sup(𝐵, 𝐴, 𝑅)} ≈ 1o ∧ 1o
≼ 1o) → {sup(𝐵, 𝐴, 𝑅)} ≼ 1o) |
| 8 | 3, 6, 7 | sylancl 586 |
. . . 4
⊢
(sup(𝐵, 𝐴, 𝑅) ∈ V → {sup(𝐵, 𝐴, 𝑅)} ≼ 1o) |
| 9 | | snprc 4717 |
. . . . . 6
⊢ (¬
sup(𝐵, 𝐴, 𝑅) ∈ V ↔ {sup(𝐵, 𝐴, 𝑅)} = ∅) |
| 10 | | snex 5436 |
. . . . . . 7
⊢
{sup(𝐵, 𝐴, 𝑅)} ∈ V |
| 11 | | eqeng 9026 |
. . . . . . 7
⊢
({sup(𝐵, 𝐴, 𝑅)} ∈ V → ({sup(𝐵, 𝐴, 𝑅)} = ∅ → {sup(𝐵, 𝐴, 𝑅)} ≈ ∅)) |
| 12 | 10, 11 | ax-mp 5 |
. . . . . 6
⊢
({sup(𝐵, 𝐴, 𝑅)} = ∅ → {sup(𝐵, 𝐴, 𝑅)} ≈ ∅) |
| 13 | 9, 12 | sylbi 217 |
. . . . 5
⊢ (¬
sup(𝐵, 𝐴, 𝑅) ∈ V → {sup(𝐵, 𝐴, 𝑅)} ≈ ∅) |
| 14 | | 0domg 9140 |
. . . . . 6
⊢
(1o ∈ On → ∅ ≼
1o) |
| 15 | 4, 14 | ax-mp 5 |
. . . . 5
⊢ ∅
≼ 1o |
| 16 | | endomtr 9052 |
. . . . 5
⊢
(({sup(𝐵, 𝐴, 𝑅)} ≈ ∅ ∧ ∅ ≼
1o) → {sup(𝐵, 𝐴, 𝑅)} ≼ 1o) |
| 17 | 13, 15, 16 | sylancl 586 |
. . . 4
⊢ (¬
sup(𝐵, 𝐴, 𝑅) ∈ V → {sup(𝐵, 𝐴, 𝑅)} ≼ 1o) |
| 18 | 8, 17 | pm2.61i 182 |
. . 3
⊢
{sup(𝐵, 𝐴, 𝑅)} ≼ 1o |
| 19 | 2, 18 | eqbrtrdi 5182 |
. 2
⊢ ((𝜑 ∧ 𝑂 ≺ 𝐵) → if(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵) ≼ 1o) |
| 20 | | iffalse 4534 |
. . . 4
⊢ (¬
𝑂 ≺ 𝐵 → if(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵) = 𝐵) |
| 21 | 20 | adantl 481 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑂 ≺ 𝐵) → if(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵) = 𝐵) |
| 22 | | safesnsupfidom1o.finite |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ Fin) |
| 23 | | safesnsupfidom1o.small |
. . . . 5
⊢ (𝜑 → (𝑂 = ∅ ∨ 𝑂 = 1o)) |
| 24 | | 0elon 6438 |
. . . . . . . . 9
⊢ ∅
∈ On |
| 25 | | eleq1 2829 |
. . . . . . . . 9
⊢ (𝑂 = ∅ → (𝑂 ∈ On ↔ ∅ ∈
On)) |
| 26 | 24, 25 | mpbiri 258 |
. . . . . . . 8
⊢ (𝑂 = ∅ → 𝑂 ∈ On) |
| 27 | | eleq1 2829 |
. . . . . . . . 9
⊢ (𝑂 = 1o → (𝑂 ∈ On ↔ 1o
∈ On)) |
| 28 | 4, 27 | mpbiri 258 |
. . . . . . . 8
⊢ (𝑂 = 1o → 𝑂 ∈ On) |
| 29 | 26, 28 | jaoi 858 |
. . . . . . 7
⊢ ((𝑂 = ∅ ∨ 𝑂 = 1o) → 𝑂 ∈ On) |
| 30 | | fidomtri 10033 |
. . . . . . 7
⊢ ((𝐵 ∈ Fin ∧ 𝑂 ∈ On) → (𝐵 ≼ 𝑂 ↔ ¬ 𝑂 ≺ 𝐵)) |
| 31 | 29, 30 | sylan2 593 |
. . . . . 6
⊢ ((𝐵 ∈ Fin ∧ (𝑂 = ∅ ∨ 𝑂 = 1o)) → (𝐵 ≼ 𝑂 ↔ ¬ 𝑂 ≺ 𝐵)) |
| 32 | | breq2 5147 |
. . . . . . . . 9
⊢ (𝑂 = ∅ → (𝐵 ≼ 𝑂 ↔ 𝐵 ≼ ∅)) |
| 33 | | domtr 9047 |
. . . . . . . . . 10
⊢ ((𝐵 ≼ ∅ ∧ ∅
≼ 1o) → 𝐵 ≼ 1o) |
| 34 | 15, 33 | mpan2 691 |
. . . . . . . . 9
⊢ (𝐵 ≼ ∅ → 𝐵 ≼
1o) |
| 35 | 32, 34 | biimtrdi 253 |
. . . . . . . 8
⊢ (𝑂 = ∅ → (𝐵 ≼ 𝑂 → 𝐵 ≼ 1o)) |
| 36 | | breq2 5147 |
. . . . . . . . 9
⊢ (𝑂 = 1o → (𝐵 ≼ 𝑂 ↔ 𝐵 ≼ 1o)) |
| 37 | 36 | biimpd 229 |
. . . . . . . 8
⊢ (𝑂 = 1o → (𝐵 ≼ 𝑂 → 𝐵 ≼ 1o)) |
| 38 | 35, 37 | jaoi 858 |
. . . . . . 7
⊢ ((𝑂 = ∅ ∨ 𝑂 = 1o) → (𝐵 ≼ 𝑂 → 𝐵 ≼ 1o)) |
| 39 | 38 | adantl 481 |
. . . . . 6
⊢ ((𝐵 ∈ Fin ∧ (𝑂 = ∅ ∨ 𝑂 = 1o)) → (𝐵 ≼ 𝑂 → 𝐵 ≼ 1o)) |
| 40 | 31, 39 | sylbird 260 |
. . . . 5
⊢ ((𝐵 ∈ Fin ∧ (𝑂 = ∅ ∨ 𝑂 = 1o)) → (¬
𝑂 ≺ 𝐵 → 𝐵 ≼ 1o)) |
| 41 | 22, 23, 40 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (¬ 𝑂 ≺ 𝐵 → 𝐵 ≼ 1o)) |
| 42 | 41 | imp 406 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑂 ≺ 𝐵) → 𝐵 ≼ 1o) |
| 43 | 21, 42 | eqbrtrd 5165 |
. 2
⊢ ((𝜑 ∧ ¬ 𝑂 ≺ 𝐵) → if(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵) ≼ 1o) |
| 44 | 19, 43 | pm2.61dan 813 |
1
⊢ (𝜑 → if(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵) ≼ 1o) |