| Step | Hyp | Ref
| Expression |
| 1 | | isfin7 10341 |
. . . 4
⊢ (𝐴 ∈ FinVII →
(𝐴 ∈ FinVII
↔ ¬ ∃𝑥
∈ (On ∖ ω)𝐴 ≈ 𝑥)) |
| 2 | 1 | ibi 267 |
. . 3
⊢ (𝐴 ∈ FinVII →
¬ ∃𝑥 ∈ (On
∖ ω)𝐴 ≈
𝑥) |
| 3 | | isnum2 9985 |
. . . . 5
⊢ (𝐴 ∈ dom card ↔
∃𝑥 ∈ On 𝑥 ≈ 𝐴) |
| 4 | | ensym 9043 |
. . . . . . . . 9
⊢ (𝑥 ≈ 𝐴 → 𝐴 ≈ 𝑥) |
| 5 | | simprl 771 |
. . . . . . . . . . 11
⊢ ((¬
𝐴 ∈ Fin ∧ (𝑥 ∈ On ∧ 𝐴 ≈ 𝑥)) → 𝑥 ∈ On) |
| 6 | | enfi 9227 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ≈ 𝑥 → (𝐴 ∈ Fin ↔ 𝑥 ∈ Fin)) |
| 7 | | onfin 9267 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ On → (𝑥 ∈ Fin ↔ 𝑥 ∈
ω)) |
| 8 | 6, 7 | sylan9bbr 510 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ On ∧ 𝐴 ≈ 𝑥) → (𝐴 ∈ Fin ↔ 𝑥 ∈ ω)) |
| 9 | 8 | biimprd 248 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ On ∧ 𝐴 ≈ 𝑥) → (𝑥 ∈ ω → 𝐴 ∈ Fin)) |
| 10 | 9 | con3d 152 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ On ∧ 𝐴 ≈ 𝑥) → (¬ 𝐴 ∈ Fin → ¬ 𝑥 ∈ ω)) |
| 11 | 10 | impcom 407 |
. . . . . . . . . . 11
⊢ ((¬
𝐴 ∈ Fin ∧ (𝑥 ∈ On ∧ 𝐴 ≈ 𝑥)) → ¬ 𝑥 ∈ ω) |
| 12 | 5, 11 | eldifd 3962 |
. . . . . . . . . 10
⊢ ((¬
𝐴 ∈ Fin ∧ (𝑥 ∈ On ∧ 𝐴 ≈ 𝑥)) → 𝑥 ∈ (On ∖
ω)) |
| 13 | | simprr 773 |
. . . . . . . . . 10
⊢ ((¬
𝐴 ∈ Fin ∧ (𝑥 ∈ On ∧ 𝐴 ≈ 𝑥)) → 𝐴 ≈ 𝑥) |
| 14 | 12, 13 | jca 511 |
. . . . . . . . 9
⊢ ((¬
𝐴 ∈ Fin ∧ (𝑥 ∈ On ∧ 𝐴 ≈ 𝑥)) → (𝑥 ∈ (On ∖ ω) ∧ 𝐴 ≈ 𝑥)) |
| 15 | 4, 14 | sylanr2 683 |
. . . . . . . 8
⊢ ((¬
𝐴 ∈ Fin ∧ (𝑥 ∈ On ∧ 𝑥 ≈ 𝐴)) → (𝑥 ∈ (On ∖ ω) ∧ 𝐴 ≈ 𝑥)) |
| 16 | 15 | ex 412 |
. . . . . . 7
⊢ (¬
𝐴 ∈ Fin → ((𝑥 ∈ On ∧ 𝑥 ≈ 𝐴) → (𝑥 ∈ (On ∖ ω) ∧ 𝐴 ≈ 𝑥))) |
| 17 | 16 | reximdv2 3164 |
. . . . . 6
⊢ (¬
𝐴 ∈ Fin →
(∃𝑥 ∈ On 𝑥 ≈ 𝐴 → ∃𝑥 ∈ (On ∖ ω)𝐴 ≈ 𝑥)) |
| 18 | 17 | com12 32 |
. . . . 5
⊢
(∃𝑥 ∈ On
𝑥 ≈ 𝐴 → (¬ 𝐴 ∈ Fin → ∃𝑥 ∈ (On ∖ ω)𝐴 ≈ 𝑥)) |
| 19 | 3, 18 | sylbi 217 |
. . . 4
⊢ (𝐴 ∈ dom card → (¬
𝐴 ∈ Fin →
∃𝑥 ∈ (On ∖
ω)𝐴 ≈ 𝑥)) |
| 20 | 19 | con1d 145 |
. . 3
⊢ (𝐴 ∈ dom card → (¬
∃𝑥 ∈ (On ∖
ω)𝐴 ≈ 𝑥 → 𝐴 ∈ Fin)) |
| 21 | 2, 20 | syl5com 31 |
. 2
⊢ (𝐴 ∈ FinVII →
(𝐴 ∈ dom card →
𝐴 ∈
Fin)) |
| 22 | | eldifi 4131 |
. . . . . . 7
⊢ (𝑥 ∈ (On ∖ ω)
→ 𝑥 ∈
On) |
| 23 | | ensym 9043 |
. . . . . . 7
⊢ (𝐴 ≈ 𝑥 → 𝑥 ≈ 𝐴) |
| 24 | | isnumi 9986 |
. . . . . . 7
⊢ ((𝑥 ∈ On ∧ 𝑥 ≈ 𝐴) → 𝐴 ∈ dom card) |
| 25 | 22, 23, 24 | syl2an 596 |
. . . . . 6
⊢ ((𝑥 ∈ (On ∖ ω)
∧ 𝐴 ≈ 𝑥) → 𝐴 ∈ dom card) |
| 26 | 25 | rexlimiva 3147 |
. . . . 5
⊢
(∃𝑥 ∈ (On
∖ ω)𝐴 ≈
𝑥 → 𝐴 ∈ dom card) |
| 27 | 26 | con3i 154 |
. . . 4
⊢ (¬
𝐴 ∈ dom card →
¬ ∃𝑥 ∈ (On
∖ ω)𝐴 ≈
𝑥) |
| 28 | | isfin7 10341 |
. . . 4
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ FinVII ↔ ¬
∃𝑥 ∈ (On ∖
ω)𝐴 ≈ 𝑥)) |
| 29 | 27, 28 | imbitrrid 246 |
. . 3
⊢ (𝐴 ∈ 𝑉 → (¬ 𝐴 ∈ dom card → 𝐴 ∈ FinVII)) |
| 30 | | fin17 10434 |
. . . 4
⊢ (𝐴 ∈ Fin → 𝐴 ∈
FinVII) |
| 31 | 30 | a1i 11 |
. . 3
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ Fin → 𝐴 ∈ FinVII)) |
| 32 | 29, 31 | jad 187 |
. 2
⊢ (𝐴 ∈ 𝑉 → ((𝐴 ∈ dom card → 𝐴 ∈ Fin) → 𝐴 ∈ FinVII)) |
| 33 | 21, 32 | impbid2 226 |
1
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ FinVII ↔ (𝐴 ∈ dom card → 𝐴 ∈ Fin))) |