Proof of Theorem isfin4-3
Step | Hyp | Ref
| Expression |
1 | | 1on 7567 |
. . . 4
⊢
1𝑜 ∈ On |
2 | | cdadom3 9010 |
. . . 4
⊢ ((𝐴 ∈ FinIV ∧
1𝑜 ∈ On) → 𝐴 ≼ (𝐴 +𝑐
1𝑜)) |
3 | 1, 2 | mpan2 707 |
. . 3
⊢ (𝐴 ∈ FinIV →
𝐴 ≼ (𝐴 +𝑐
1𝑜)) |
4 | | ssun1 3776 |
. . . . . . . 8
⊢ (𝐴 × {∅}) ⊆
((𝐴 × {∅})
∪ (1𝑜 × {1𝑜})) |
5 | | relen 7960 |
. . . . . . . . . 10
⊢ Rel
≈ |
6 | 5 | brrelexi 5158 |
. . . . . . . . 9
⊢ (𝐴 ≈ (𝐴 +𝑐
1𝑜) → 𝐴 ∈ V) |
7 | | cdaval 8992 |
. . . . . . . . 9
⊢ ((𝐴 ∈ V ∧
1𝑜 ∈ On) → (𝐴 +𝑐
1𝑜) = ((𝐴 × {∅}) ∪
(1𝑜 × {1𝑜}))) |
8 | 6, 1, 7 | sylancl 694 |
. . . . . . . 8
⊢ (𝐴 ≈ (𝐴 +𝑐
1𝑜) → (𝐴 +𝑐
1𝑜) = ((𝐴 × {∅}) ∪
(1𝑜 × {1𝑜}))) |
9 | 4, 8 | syl5sseqr 3654 |
. . . . . . 7
⊢ (𝐴 ≈ (𝐴 +𝑐
1𝑜) → (𝐴 × {∅}) ⊆ (𝐴 +𝑐
1𝑜)) |
10 | | 0lt1o 7584 |
. . . . . . . . . 10
⊢ ∅
∈ 1𝑜 |
11 | 1 | elexi 3213 |
. . . . . . . . . . 11
⊢
1𝑜 ∈ V |
12 | 11 | snid 4208 |
. . . . . . . . . 10
⊢
1𝑜 ∈ {1𝑜} |
13 | | opelxpi 5148 |
. . . . . . . . . 10
⊢ ((∅
∈ 1𝑜 ∧ 1𝑜 ∈
{1𝑜}) → 〈∅, 1𝑜〉
∈ (1𝑜 ×
{1𝑜})) |
14 | 10, 12, 13 | mp2an 708 |
. . . . . . . . 9
⊢
〈∅, 1𝑜〉 ∈ (1𝑜
× {1𝑜}) |
15 | | elun2 3781 |
. . . . . . . . 9
⊢
(〈∅, 1𝑜〉 ∈
(1𝑜 × {1𝑜}) → 〈∅,
1𝑜〉 ∈ ((𝐴 × {∅}) ∪
(1𝑜 × {1𝑜}))) |
16 | 14, 15 | mp1i 13 |
. . . . . . . 8
⊢ (𝐴 ≈ (𝐴 +𝑐
1𝑜) → 〈∅, 1𝑜〉 ∈
((𝐴 × {∅})
∪ (1𝑜 ×
{1𝑜}))) |
17 | 16, 8 | eleqtrrd 2704 |
. . . . . . 7
⊢ (𝐴 ≈ (𝐴 +𝑐
1𝑜) → 〈∅, 1𝑜〉 ∈
(𝐴 +𝑐
1𝑜)) |
18 | | 1n0 7575 |
. . . . . . . 8
⊢
1𝑜 ≠ ∅ |
19 | | opelxp2 5151 |
. . . . . . . . . 10
⊢
(〈∅, 1𝑜〉 ∈ (𝐴 × {∅}) →
1𝑜 ∈ {∅}) |
20 | | elsni 4194 |
. . . . . . . . . 10
⊢
(1𝑜 ∈ {∅} → 1𝑜 =
∅) |
21 | 19, 20 | syl 17 |
. . . . . . . . 9
⊢
(〈∅, 1𝑜〉 ∈ (𝐴 × {∅}) →
1𝑜 = ∅) |
22 | 21 | necon3ai 2819 |
. . . . . . . 8
⊢
(1𝑜 ≠ ∅ → ¬ 〈∅,
1𝑜〉 ∈ (𝐴 × {∅})) |
23 | 18, 22 | mp1i 13 |
. . . . . . 7
⊢ (𝐴 ≈ (𝐴 +𝑐
1𝑜) → ¬ 〈∅, 1𝑜〉
∈ (𝐴 ×
{∅})) |
24 | 9, 17, 23 | ssnelpssd 3719 |
. . . . . 6
⊢ (𝐴 ≈ (𝐴 +𝑐
1𝑜) → (𝐴 × {∅}) ⊊ (𝐴 +𝑐
1𝑜)) |
25 | | 0ex 4790 |
. . . . . . . 8
⊢ ∅
∈ V |
26 | | xpsneng 8045 |
. . . . . . . 8
⊢ ((𝐴 ∈ V ∧ ∅ ∈
V) → (𝐴 ×
{∅}) ≈ 𝐴) |
27 | 6, 25, 26 | sylancl 694 |
. . . . . . 7
⊢ (𝐴 ≈ (𝐴 +𝑐
1𝑜) → (𝐴 × {∅}) ≈ 𝐴) |
28 | | entr 8008 |
. . . . . . 7
⊢ (((𝐴 × {∅}) ≈
𝐴 ∧ 𝐴 ≈ (𝐴 +𝑐
1𝑜)) → (𝐴 × {∅}) ≈ (𝐴 +𝑐
1𝑜)) |
29 | 27, 28 | mpancom 703 |
. . . . . 6
⊢ (𝐴 ≈ (𝐴 +𝑐
1𝑜) → (𝐴 × {∅}) ≈ (𝐴 +𝑐
1𝑜)) |
30 | | fin4i 9120 |
. . . . . 6
⊢ (((𝐴 × {∅}) ⊊
(𝐴 +𝑐
1𝑜) ∧ (𝐴 × {∅}) ≈ (𝐴 +𝑐
1𝑜)) → ¬ (𝐴 +𝑐
1𝑜) ∈ FinIV) |
31 | 24, 29, 30 | syl2anc 693 |
. . . . 5
⊢ (𝐴 ≈ (𝐴 +𝑐
1𝑜) → ¬ (𝐴 +𝑐
1𝑜) ∈ FinIV) |
32 | | fin4en1 9131 |
. . . . 5
⊢ (𝐴 ≈ (𝐴 +𝑐
1𝑜) → (𝐴 ∈ FinIV → (𝐴 +𝑐
1𝑜) ∈ FinIV)) |
33 | 31, 32 | mtod 189 |
. . . 4
⊢ (𝐴 ≈ (𝐴 +𝑐
1𝑜) → ¬ 𝐴 ∈ FinIV) |
34 | 33 | con2i 134 |
. . 3
⊢ (𝐴 ∈ FinIV →
¬ 𝐴 ≈ (𝐴 +𝑐
1𝑜)) |
35 | | brsdom 7978 |
. . 3
⊢ (𝐴 ≺ (𝐴 +𝑐
1𝑜) ↔ (𝐴 ≼ (𝐴 +𝑐
1𝑜) ∧ ¬ 𝐴 ≈ (𝐴 +𝑐
1𝑜))) |
36 | 3, 34, 35 | sylanbrc 698 |
. 2
⊢ (𝐴 ∈ FinIV →
𝐴 ≺ (𝐴 +𝑐
1𝑜)) |
37 | | sdomnen 7984 |
. . . 4
⊢ (𝐴 ≺ (𝐴 +𝑐
1𝑜) → ¬ 𝐴 ≈ (𝐴 +𝑐
1𝑜)) |
38 | | infcda1 9015 |
. . . . 5
⊢ (ω
≼ 𝐴 → (𝐴 +𝑐
1𝑜) ≈ 𝐴) |
39 | 38 | ensymd 8007 |
. . . 4
⊢ (ω
≼ 𝐴 → 𝐴 ≈ (𝐴 +𝑐
1𝑜)) |
40 | 37, 39 | nsyl 135 |
. . 3
⊢ (𝐴 ≺ (𝐴 +𝑐
1𝑜) → ¬ ω ≼ 𝐴) |
41 | | relsdom 7962 |
. . . . 5
⊢ Rel
≺ |
42 | 41 | brrelexi 5158 |
. . . 4
⊢ (𝐴 ≺ (𝐴 +𝑐
1𝑜) → 𝐴 ∈ V) |
43 | | isfin4-2 9136 |
. . . 4
⊢ (𝐴 ∈ V → (𝐴 ∈ FinIV ↔
¬ ω ≼ 𝐴)) |
44 | 42, 43 | syl 17 |
. . 3
⊢ (𝐴 ≺ (𝐴 +𝑐
1𝑜) → (𝐴 ∈ FinIV ↔ ¬
ω ≼ 𝐴)) |
45 | 40, 44 | mpbird 247 |
. 2
⊢ (𝐴 ≺ (𝐴 +𝑐
1𝑜) → 𝐴 ∈ FinIV) |
46 | 36, 45 | impbii 199 |
1
⊢ (𝐴 ∈ FinIV ↔
𝐴 ≺ (𝐴 +𝑐
1𝑜)) |