Step | Hyp | Ref
| Expression |
1 | | iftrue 4497 |
. . . 4
⊢ (𝑂 ≺ 𝐵 → if(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵) = {sup(𝐵, 𝐴, 𝑅)}) |
2 | 1 | adantl 483 |
. . 3
⊢ ((𝜑 ∧ 𝑂 ≺ 𝐵) → if(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵) = {sup(𝐵, 𝐴, 𝑅)}) |
3 | | ensn1g 8970 |
. . . . 5
⊢
(sup(𝐵, 𝐴, 𝑅) ∈ V → {sup(𝐵, 𝐴, 𝑅)} ≈ 1o) |
4 | | 1on 8429 |
. . . . . 6
⊢
1o ∈ On |
5 | | domrefg 8934 |
. . . . . 6
⊢
(1o ∈ On → 1o ≼
1o) |
6 | 4, 5 | ax-mp 5 |
. . . . 5
⊢
1o ≼ 1o |
7 | | endomtr 8959 |
. . . . 5
⊢
(({sup(𝐵, 𝐴, 𝑅)} ≈ 1o ∧ 1o
≼ 1o) → {sup(𝐵, 𝐴, 𝑅)} ≼ 1o) |
8 | 3, 6, 7 | sylancl 587 |
. . . 4
⊢
(sup(𝐵, 𝐴, 𝑅) ∈ V → {sup(𝐵, 𝐴, 𝑅)} ≼ 1o) |
9 | | snprc 4683 |
. . . . . 6
⊢ (¬
sup(𝐵, 𝐴, 𝑅) ∈ V ↔ {sup(𝐵, 𝐴, 𝑅)} = ∅) |
10 | | snex 5393 |
. . . . . . 7
⊢
{sup(𝐵, 𝐴, 𝑅)} ∈ V |
11 | | eqeng 8933 |
. . . . . . 7
⊢
({sup(𝐵, 𝐴, 𝑅)} ∈ V → ({sup(𝐵, 𝐴, 𝑅)} = ∅ → {sup(𝐵, 𝐴, 𝑅)} ≈ ∅)) |
12 | 10, 11 | ax-mp 5 |
. . . . . 6
⊢
({sup(𝐵, 𝐴, 𝑅)} = ∅ → {sup(𝐵, 𝐴, 𝑅)} ≈ ∅) |
13 | 9, 12 | sylbi 216 |
. . . . 5
⊢ (¬
sup(𝐵, 𝐴, 𝑅) ∈ V → {sup(𝐵, 𝐴, 𝑅)} ≈ ∅) |
14 | | 0domg 9051 |
. . . . . 6
⊢
(1o ∈ On → ∅ ≼
1o) |
15 | 4, 14 | ax-mp 5 |
. . . . 5
⊢ ∅
≼ 1o |
16 | | endomtr 8959 |
. . . . 5
⊢
(({sup(𝐵, 𝐴, 𝑅)} ≈ ∅ ∧ ∅ ≼
1o) → {sup(𝐵, 𝐴, 𝑅)} ≼ 1o) |
17 | 13, 15, 16 | sylancl 587 |
. . . 4
⊢ (¬
sup(𝐵, 𝐴, 𝑅) ∈ V → {sup(𝐵, 𝐴, 𝑅)} ≼ 1o) |
18 | 8, 17 | pm2.61i 182 |
. . 3
⊢
{sup(𝐵, 𝐴, 𝑅)} ≼ 1o |
19 | 2, 18 | eqbrtrdi 5149 |
. 2
⊢ ((𝜑 ∧ 𝑂 ≺ 𝐵) → if(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵) ≼ 1o) |
20 | | iffalse 4500 |
. . . 4
⊢ (¬
𝑂 ≺ 𝐵 → if(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵) = 𝐵) |
21 | 20 | adantl 483 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑂 ≺ 𝐵) → if(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵) = 𝐵) |
22 | | safesnsupfidom1o.finite |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ Fin) |
23 | | safesnsupfidom1o.small |
. . . . 5
⊢ (𝜑 → (𝑂 = ∅ ∨ 𝑂 = 1o)) |
24 | | 0elon 6376 |
. . . . . . . . 9
⊢ ∅
∈ On |
25 | | eleq1 2826 |
. . . . . . . . 9
⊢ (𝑂 = ∅ → (𝑂 ∈ On ↔ ∅ ∈
On)) |
26 | 24, 25 | mpbiri 258 |
. . . . . . . 8
⊢ (𝑂 = ∅ → 𝑂 ∈ On) |
27 | | eleq1 2826 |
. . . . . . . . 9
⊢ (𝑂 = 1o → (𝑂 ∈ On ↔ 1o
∈ On)) |
28 | 4, 27 | mpbiri 258 |
. . . . . . . 8
⊢ (𝑂 = 1o → 𝑂 ∈ On) |
29 | 26, 28 | jaoi 856 |
. . . . . . 7
⊢ ((𝑂 = ∅ ∨ 𝑂 = 1o) → 𝑂 ∈ On) |
30 | | fidomtri 9936 |
. . . . . . 7
⊢ ((𝐵 ∈ Fin ∧ 𝑂 ∈ On) → (𝐵 ≼ 𝑂 ↔ ¬ 𝑂 ≺ 𝐵)) |
31 | 29, 30 | sylan2 594 |
. . . . . 6
⊢ ((𝐵 ∈ Fin ∧ (𝑂 = ∅ ∨ 𝑂 = 1o)) → (𝐵 ≼ 𝑂 ↔ ¬ 𝑂 ≺ 𝐵)) |
32 | | breq2 5114 |
. . . . . . . . 9
⊢ (𝑂 = ∅ → (𝐵 ≼ 𝑂 ↔ 𝐵 ≼ ∅)) |
33 | | domtr 8954 |
. . . . . . . . . 10
⊢ ((𝐵 ≼ ∅ ∧ ∅
≼ 1o) → 𝐵 ≼ 1o) |
34 | 15, 33 | mpan2 690 |
. . . . . . . . 9
⊢ (𝐵 ≼ ∅ → 𝐵 ≼
1o) |
35 | 32, 34 | syl6bi 253 |
. . . . . . . 8
⊢ (𝑂 = ∅ → (𝐵 ≼ 𝑂 → 𝐵 ≼ 1o)) |
36 | | breq2 5114 |
. . . . . . . . 9
⊢ (𝑂 = 1o → (𝐵 ≼ 𝑂 ↔ 𝐵 ≼ 1o)) |
37 | 36 | biimpd 228 |
. . . . . . . 8
⊢ (𝑂 = 1o → (𝐵 ≼ 𝑂 → 𝐵 ≼ 1o)) |
38 | 35, 37 | jaoi 856 |
. . . . . . 7
⊢ ((𝑂 = ∅ ∨ 𝑂 = 1o) → (𝐵 ≼ 𝑂 → 𝐵 ≼ 1o)) |
39 | 38 | adantl 483 |
. . . . . 6
⊢ ((𝐵 ∈ Fin ∧ (𝑂 = ∅ ∨ 𝑂 = 1o)) → (𝐵 ≼ 𝑂 → 𝐵 ≼ 1o)) |
40 | 31, 39 | sylbird 260 |
. . . . 5
⊢ ((𝐵 ∈ Fin ∧ (𝑂 = ∅ ∨ 𝑂 = 1o)) → (¬
𝑂 ≺ 𝐵 → 𝐵 ≼ 1o)) |
41 | 22, 23, 40 | syl2anc 585 |
. . . 4
⊢ (𝜑 → (¬ 𝑂 ≺ 𝐵 → 𝐵 ≼ 1o)) |
42 | 41 | imp 408 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝑂 ≺ 𝐵) → 𝐵 ≼ 1o) |
43 | 21, 42 | eqbrtrd 5132 |
. 2
⊢ ((𝜑 ∧ ¬ 𝑂 ≺ 𝐵) → if(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵) ≼ 1o) |
44 | 19, 43 | pm2.61dan 812 |
1
⊢ (𝜑 → if(𝑂 ≺ 𝐵, {sup(𝐵, 𝐴, 𝑅)}, 𝐵) ≼ 1o) |