Proof of Theorem ord2eln012
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ne0i 4340 | . . 3
⊢
(2o ∈ 𝐴 → 𝐴 ≠ ∅) | 
| 2 |  | 2on0 8523 | . . . . . 6
⊢
2o ≠ ∅ | 
| 3 |  | el1o 8534 | . . . . . 6
⊢
(2o ∈ 1o ↔ 2o =
∅) | 
| 4 | 2, 3 | nemtbir 3037 | . . . . 5
⊢  ¬
2o ∈ 1o | 
| 5 |  | eleq2 2829 | . . . . 5
⊢ (𝐴 = 1o →
(2o ∈ 𝐴
↔ 2o ∈ 1o)) | 
| 6 | 4, 5 | mtbiri 327 | . . . 4
⊢ (𝐴 = 1o → ¬
2o ∈ 𝐴) | 
| 7 | 6 | necon2ai 2969 | . . 3
⊢
(2o ∈ 𝐴 → 𝐴 ≠ 1o) | 
| 8 |  | 2on 8521 | . . . . . 6
⊢
2o ∈ On | 
| 9 | 8 | onirri 6496 | . . . . 5
⊢  ¬
2o ∈ 2o | 
| 10 |  | eleq2 2829 | . . . . 5
⊢ (𝐴 = 2o →
(2o ∈ 𝐴
↔ 2o ∈ 2o)) | 
| 11 | 9, 10 | mtbiri 327 | . . . 4
⊢ (𝐴 = 2o → ¬
2o ∈ 𝐴) | 
| 12 | 11 | necon2ai 2969 | . . 3
⊢
(2o ∈ 𝐴 → 𝐴 ≠ 2o) | 
| 13 | 1, 7, 12 | 3jca 1128 | . 2
⊢
(2o ∈ 𝐴 → (𝐴 ≠ ∅ ∧ 𝐴 ≠ 1o ∧ 𝐴 ≠ 2o)) | 
| 14 |  | nesym 2996 | . . . . . . 7
⊢ (𝐴 ≠ 2o ↔ ¬
2o = 𝐴) | 
| 15 | 14 | biimpi 216 | . . . . . 6
⊢ (𝐴 ≠ 2o → ¬
2o = 𝐴) | 
| 16 | 15 | 3ad2ant3 1135 | . . . . 5
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ≠ 1o ∧ 𝐴 ≠ 2o) →
¬ 2o = 𝐴) | 
| 17 |  | simp1 1136 | . . . . . . 7
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ≠ 1o ∧ 𝐴 ≠ 2o) →
𝐴 ≠
∅) | 
| 18 |  | simp2 1137 | . . . . . . 7
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ≠ 1o ∧ 𝐴 ≠ 2o) →
𝐴 ≠
1o) | 
| 19 | 17, 18 | nelprd 4656 | . . . . . 6
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ≠ 1o ∧ 𝐴 ≠ 2o) →
¬ 𝐴 ∈ {∅,
1o}) | 
| 20 |  | df2o3 8515 | . . . . . . 7
⊢
2o = {∅, 1o} | 
| 21 | 20 | eleq2i 2832 | . . . . . 6
⊢ (𝐴 ∈ 2o ↔
𝐴 ∈ {∅,
1o}) | 
| 22 | 19, 21 | sylnibr 329 | . . . . 5
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ≠ 1o ∧ 𝐴 ≠ 2o) →
¬ 𝐴 ∈
2o) | 
| 23 | 16, 22 | jca 511 | . . . 4
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ≠ 1o ∧ 𝐴 ≠ 2o) →
(¬ 2o = 𝐴
∧ ¬ 𝐴 ∈
2o)) | 
| 24 |  | pm4.56 990 | . . . 4
⊢ ((¬
2o = 𝐴 ∧
¬ 𝐴 ∈
2o) ↔ ¬ (2o = 𝐴 ∨ 𝐴 ∈ 2o)) | 
| 25 | 23, 24 | sylib 218 | . . 3
⊢ ((𝐴 ≠ ∅ ∧ 𝐴 ≠ 1o ∧ 𝐴 ≠ 2o) →
¬ (2o = 𝐴
∨ 𝐴 ∈
2o)) | 
| 26 | 8 | onordi 6494 | . . . 4
⊢ Ord
2o | 
| 27 |  | ordtri2 6418 | . . . 4
⊢ ((Ord
2o ∧ Ord 𝐴)
→ (2o ∈ 𝐴 ↔ ¬ (2o = 𝐴 ∨ 𝐴 ∈ 2o))) | 
| 28 | 26, 27 | mpan 690 | . . 3
⊢ (Ord
𝐴 → (2o
∈ 𝐴 ↔ ¬
(2o = 𝐴 ∨
𝐴 ∈
2o))) | 
| 29 | 25, 28 | imbitrrid 246 | . 2
⊢ (Ord
𝐴 → ((𝐴 ≠ ∅ ∧ 𝐴 ≠ 1o ∧ 𝐴 ≠ 2o) →
2o ∈ 𝐴)) | 
| 30 | 13, 29 | impbid2 226 | 1
⊢ (Ord
𝐴 → (2o
∈ 𝐴 ↔ (𝐴 ≠ ∅ ∧ 𝐴 ≠ 1o ∧ 𝐴 ≠
2o))) |