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) |