Proof of Theorem isfin4p1
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 1on 8519 | . . . 4
⊢
1o ∈ On | 
| 2 |  | djudoml 10226 | . . . 4
⊢ ((𝐴 ∈ FinIV ∧
1o ∈ On) → 𝐴 ≼ (𝐴 ⊔ 1o)) | 
| 3 | 1, 2 | mpan2 691 | . . 3
⊢ (𝐴 ∈ FinIV →
𝐴 ≼ (𝐴 ⊔
1o)) | 
| 4 |  | 1oex 8517 | . . . . . . . . . . 11
⊢
1o ∈ V | 
| 5 | 4 | snid 4661 | . . . . . . . . . 10
⊢
1o ∈ {1o} | 
| 6 |  | 0lt1o 8543 | . . . . . . . . . 10
⊢ ∅
∈ 1o | 
| 7 |  | opelxpi 5721 | . . . . . . . . . 10
⊢
((1o ∈ {1o} ∧ ∅ ∈
1o) → 〈1o, ∅〉 ∈
({1o} × 1o)) | 
| 8 | 5, 6, 7 | mp2an 692 | . . . . . . . . 9
⊢
〈1o, ∅〉 ∈ ({1o} ×
1o) | 
| 9 |  | elun2 4182 | . . . . . . . . 9
⊢
(〈1o, ∅〉 ∈ ({1o} ×
1o) → 〈1o, ∅〉 ∈ (({∅}
× 𝐴) ∪
({1o} × 1o))) | 
| 10 | 8, 9 | ax-mp 5 | . . . . . . . 8
⊢
〈1o, ∅〉 ∈ (({∅} × 𝐴) ∪ ({1o} ×
1o)) | 
| 11 |  | df-dju 9942 | . . . . . . . 8
⊢ (𝐴 ⊔ 1o) =
(({∅} × 𝐴)
∪ ({1o} × 1o)) | 
| 12 | 10, 11 | eleqtrri 2839 | . . . . . . 7
⊢
〈1o, ∅〉 ∈ (𝐴 ⊔ 1o) | 
| 13 |  | 1n0 8527 | . . . . . . . 8
⊢
1o ≠ ∅ | 
| 14 |  | opelxp1 5726 | . . . . . . . . . 10
⊢
(〈1o, ∅〉 ∈ ({∅} × 𝐴) → 1o ∈
{∅}) | 
| 15 |  | elsni 4642 | . . . . . . . . . 10
⊢
(1o ∈ {∅} → 1o =
∅) | 
| 16 | 14, 15 | syl 17 | . . . . . . . . 9
⊢
(〈1o, ∅〉 ∈ ({∅} × 𝐴) → 1o =
∅) | 
| 17 | 16 | necon3ai 2964 | . . . . . . . 8
⊢
(1o ≠ ∅ → ¬ 〈1o,
∅〉 ∈ ({∅} × 𝐴)) | 
| 18 | 13, 17 | ax-mp 5 | . . . . . . 7
⊢  ¬
〈1o, ∅〉 ∈ ({∅} × 𝐴) | 
| 19 |  | ssun1 4177 | . . . . . . . . 9
⊢
({∅} × 𝐴) ⊆ (({∅} × 𝐴) ∪ ({1o} ×
1o)) | 
| 20 | 19, 11 | sseqtrri 4032 | . . . . . . . 8
⊢
({∅} × 𝐴) ⊆ (𝐴 ⊔ 1o) | 
| 21 |  | ssnelpss 4113 | . . . . . . . 8
⊢
(({∅} × 𝐴) ⊆ (𝐴 ⊔ 1o) →
((〈1o, ∅〉 ∈ (𝐴 ⊔ 1o) ∧ ¬
〈1o, ∅〉 ∈ ({∅} × 𝐴)) → ({∅} × 𝐴) ⊊ (𝐴 ⊔ 1o))) | 
| 22 | 20, 21 | ax-mp 5 | . . . . . . 7
⊢
((〈1o, ∅〉 ∈ (𝐴 ⊔ 1o) ∧ ¬
〈1o, ∅〉 ∈ ({∅} × 𝐴)) → ({∅} × 𝐴) ⊊ (𝐴 ⊔ 1o)) | 
| 23 | 12, 18, 22 | mp2an 692 | . . . . . 6
⊢
({∅} × 𝐴) ⊊ (𝐴 ⊔ 1o) | 
| 24 |  | 0ex 5306 | . . . . . . . 8
⊢ ∅
∈ V | 
| 25 |  | relen 8991 | . . . . . . . . 9
⊢ Rel
≈ | 
| 26 | 25 | brrelex1i 5740 | . . . . . . . 8
⊢ (𝐴 ≈ (𝐴 ⊔ 1o) → 𝐴 ∈ V) | 
| 27 |  | xpsnen2g 9106 | . . . . . . . 8
⊢ ((∅
∈ V ∧ 𝐴 ∈ V)
→ ({∅} × 𝐴) ≈ 𝐴) | 
| 28 | 24, 26, 27 | sylancr 587 | . . . . . . 7
⊢ (𝐴 ≈ (𝐴 ⊔ 1o) → ({∅}
× 𝐴) ≈ 𝐴) | 
| 29 |  | entr 9047 | . . . . . . 7
⊢
((({∅} × 𝐴) ≈ 𝐴 ∧ 𝐴 ≈ (𝐴 ⊔ 1o)) → ({∅}
× 𝐴) ≈ (𝐴 ⊔
1o)) | 
| 30 | 28, 29 | mpancom 688 | . . . . . 6
⊢ (𝐴 ≈ (𝐴 ⊔ 1o) → ({∅}
× 𝐴) ≈ (𝐴 ⊔
1o)) | 
| 31 |  | fin4i 10339 | . . . . . 6
⊢
((({∅} × 𝐴) ⊊ (𝐴 ⊔ 1o) ∧ ({∅}
× 𝐴) ≈ (𝐴 ⊔ 1o)) →
¬ (𝐴 ⊔
1o) ∈ FinIV) | 
| 32 | 23, 30, 31 | sylancr 587 | . . . . 5
⊢ (𝐴 ≈ (𝐴 ⊔ 1o) → ¬ (𝐴 ⊔ 1o) ∈
FinIV) | 
| 33 |  | fin4en1 10350 | . . . . 5
⊢ (𝐴 ≈ (𝐴 ⊔ 1o) → (𝐴 ∈ FinIV →
(𝐴 ⊔ 1o)
∈ FinIV)) | 
| 34 | 32, 33 | mtod 198 | . . . 4
⊢ (𝐴 ≈ (𝐴 ⊔ 1o) → ¬ 𝐴 ∈
FinIV) | 
| 35 | 34 | con2i 139 | . . 3
⊢ (𝐴 ∈ FinIV →
¬ 𝐴 ≈ (𝐴 ⊔
1o)) | 
| 36 |  | brsdom 9016 | . . 3
⊢ (𝐴 ≺ (𝐴 ⊔ 1o) ↔ (𝐴 ≼ (𝐴 ⊔ 1o) ∧ ¬ 𝐴 ≈ (𝐴 ⊔ 1o))) | 
| 37 | 3, 35, 36 | sylanbrc 583 | . 2
⊢ (𝐴 ∈ FinIV →
𝐴 ≺ (𝐴 ⊔
1o)) | 
| 38 |  | sdomnen 9022 | . . . 4
⊢ (𝐴 ≺ (𝐴 ⊔ 1o) → ¬ 𝐴 ≈ (𝐴 ⊔ 1o)) | 
| 39 |  | infdju1 10231 | . . . . 5
⊢ (ω
≼ 𝐴 → (𝐴 ⊔ 1o) ≈
𝐴) | 
| 40 | 39 | ensymd 9046 | . . . 4
⊢ (ω
≼ 𝐴 → 𝐴 ≈ (𝐴 ⊔ 1o)) | 
| 41 | 38, 40 | nsyl 140 | . . 3
⊢ (𝐴 ≺ (𝐴 ⊔ 1o) → ¬
ω ≼ 𝐴) | 
| 42 |  | relsdom 8993 | . . . . 5
⊢ Rel
≺ | 
| 43 | 42 | brrelex1i 5740 | . . . 4
⊢ (𝐴 ≺ (𝐴 ⊔ 1o) → 𝐴 ∈ V) | 
| 44 |  | isfin4-2 10355 | . . . 4
⊢ (𝐴 ∈ V → (𝐴 ∈ FinIV ↔
¬ ω ≼ 𝐴)) | 
| 45 | 43, 44 | syl 17 | . . 3
⊢ (𝐴 ≺ (𝐴 ⊔ 1o) → (𝐴 ∈ FinIV ↔
¬ ω ≼ 𝐴)) | 
| 46 | 41, 45 | mpbird 257 | . 2
⊢ (𝐴 ≺ (𝐴 ⊔ 1o) → 𝐴 ∈
FinIV) | 
| 47 | 37, 46 | impbii 209 | 1
⊢ (𝐴 ∈ FinIV ↔
𝐴 ≺ (𝐴 ⊔
1o)) |