Step | Hyp | Ref
| Expression |
1 | | isfin7 9880 |
. . . 4
⊢ (𝐴 ∈ FinVII →
(𝐴 ∈ FinVII
↔ ¬ ∃𝑥
∈ (On ∖ ω)𝐴 ≈ 𝑥)) |
2 | 1 | ibi 270 |
. . 3
⊢ (𝐴 ∈ FinVII →
¬ ∃𝑥 ∈ (On
∖ ω)𝐴 ≈
𝑥) |
3 | | isnum2 9526 |
. . . . 5
⊢ (𝐴 ∈ dom card ↔
∃𝑥 ∈ On 𝑥 ≈ 𝐴) |
4 | | ensym 8655 |
. . . . . . . . 9
⊢ (𝑥 ≈ 𝐴 → 𝐴 ≈ 𝑥) |
5 | | simprl 771 |
. . . . . . . . . . 11
⊢ ((¬
𝐴 ∈ Fin ∧ (𝑥 ∈ On ∧ 𝐴 ≈ 𝑥)) → 𝑥 ∈ On) |
6 | | enfi 8842 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ≈ 𝑥 → (𝐴 ∈ Fin ↔ 𝑥 ∈ Fin)) |
7 | | onfin 8846 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ On → (𝑥 ∈ Fin ↔ 𝑥 ∈
ω)) |
8 | 6, 7 | sylan9bbr 514 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ On ∧ 𝐴 ≈ 𝑥) → (𝐴 ∈ Fin ↔ 𝑥 ∈ ω)) |
9 | 8 | biimprd 251 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ On ∧ 𝐴 ≈ 𝑥) → (𝑥 ∈ ω → 𝐴 ∈ Fin)) |
10 | 9 | con3d 155 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ On ∧ 𝐴 ≈ 𝑥) → (¬ 𝐴 ∈ Fin → ¬ 𝑥 ∈ ω)) |
11 | 10 | impcom 411 |
. . . . . . . . . . 11
⊢ ((¬
𝐴 ∈ Fin ∧ (𝑥 ∈ On ∧ 𝐴 ≈ 𝑥)) → ¬ 𝑥 ∈ ω) |
12 | 5, 11 | eldifd 3864 |
. . . . . . . . . 10
⊢ ((¬
𝐴 ∈ Fin ∧ (𝑥 ∈ On ∧ 𝐴 ≈ 𝑥)) → 𝑥 ∈ (On ∖
ω)) |
13 | | simprr 773 |
. . . . . . . . . 10
⊢ ((¬
𝐴 ∈ Fin ∧ (𝑥 ∈ On ∧ 𝐴 ≈ 𝑥)) → 𝐴 ≈ 𝑥) |
14 | 12, 13 | jca 515 |
. . . . . . . . 9
⊢ ((¬
𝐴 ∈ Fin ∧ (𝑥 ∈ On ∧ 𝐴 ≈ 𝑥)) → (𝑥 ∈ (On ∖ ω) ∧ 𝐴 ≈ 𝑥)) |
15 | 4, 14 | sylanr2 683 |
. . . . . . . 8
⊢ ((¬
𝐴 ∈ Fin ∧ (𝑥 ∈ On ∧ 𝑥 ≈ 𝐴)) → (𝑥 ∈ (On ∖ ω) ∧ 𝐴 ≈ 𝑥)) |
16 | 15 | ex 416 |
. . . . . . 7
⊢ (¬
𝐴 ∈ Fin → ((𝑥 ∈ On ∧ 𝑥 ≈ 𝐴) → (𝑥 ∈ (On ∖ ω) ∧ 𝐴 ≈ 𝑥))) |
17 | 16 | reximdv2 3180 |
. . . . . 6
⊢ (¬
𝐴 ∈ Fin →
(∃𝑥 ∈ On 𝑥 ≈ 𝐴 → ∃𝑥 ∈ (On ∖ ω)𝐴 ≈ 𝑥)) |
18 | 17 | com12 32 |
. . . . 5
⊢
(∃𝑥 ∈ On
𝑥 ≈ 𝐴 → (¬ 𝐴 ∈ Fin → ∃𝑥 ∈ (On ∖ ω)𝐴 ≈ 𝑥)) |
19 | 3, 18 | sylbi 220 |
. . . 4
⊢ (𝐴 ∈ dom card → (¬
𝐴 ∈ Fin →
∃𝑥 ∈ (On ∖
ω)𝐴 ≈ 𝑥)) |
20 | 19 | con1d 147 |
. . 3
⊢ (𝐴 ∈ dom card → (¬
∃𝑥 ∈ (On ∖
ω)𝐴 ≈ 𝑥 → 𝐴 ∈ Fin)) |
21 | 2, 20 | syl5com 31 |
. 2
⊢ (𝐴 ∈ FinVII →
(𝐴 ∈ dom card →
𝐴 ∈
Fin)) |
22 | | eldifi 4027 |
. . . . . . 7
⊢ (𝑥 ∈ (On ∖ ω)
→ 𝑥 ∈
On) |
23 | | ensym 8655 |
. . . . . . 7
⊢ (𝐴 ≈ 𝑥 → 𝑥 ≈ 𝐴) |
24 | | isnumi 9527 |
. . . . . . 7
⊢ ((𝑥 ∈ On ∧ 𝑥 ≈ 𝐴) → 𝐴 ∈ dom card) |
25 | 22, 23, 24 | syl2an 599 |
. . . . . 6
⊢ ((𝑥 ∈ (On ∖ ω)
∧ 𝐴 ≈ 𝑥) → 𝐴 ∈ dom card) |
26 | 25 | rexlimiva 3190 |
. . . . 5
⊢
(∃𝑥 ∈ (On
∖ ω)𝐴 ≈
𝑥 → 𝐴 ∈ dom card) |
27 | 26 | con3i 157 |
. . . 4
⊢ (¬
𝐴 ∈ dom card →
¬ ∃𝑥 ∈ (On
∖ ω)𝐴 ≈
𝑥) |
28 | | isfin7 9880 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ FinVII ↔ ¬
∃𝑥 ∈ (On ∖
ω)𝐴 ≈ 𝑥)) |
29 | 27, 28 | syl5ibr 249 |
. . 3
⊢ (𝐴 ∈ 𝑉 → (¬ 𝐴 ∈ dom card → 𝐴 ∈ FinVII)) |
30 | | fin17 9973 |
. . . 4
⊢ (𝐴 ∈ Fin → 𝐴 ∈
FinVII) |
31 | 30 | a1i 11 |
. . 3
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Fin → 𝐴 ∈ FinVII)) |
32 | 29, 31 | jad 190 |
. 2
⊢ (𝐴 ∈ 𝑉 → ((𝐴 ∈ dom card → 𝐴 ∈ Fin) → 𝐴 ∈ FinVII)) |
33 | 21, 32 | impbid2 229 |
1
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ FinVII ↔ (𝐴 ∈ dom card → 𝐴 ∈ Fin))) |