Step |
Hyp |
Ref |
Expression |
1 |
|
isfin7 |
⊢ ( 𝐴 ∈ FinVII → ( 𝐴 ∈ FinVII ↔ ¬ ∃ 𝑥 ∈ ( On ∖ ω ) 𝐴 ≈ 𝑥 ) ) |
2 |
1
|
ibi |
⊢ ( 𝐴 ∈ FinVII → ¬ ∃ 𝑥 ∈ ( On ∖ ω ) 𝐴 ≈ 𝑥 ) |
3 |
|
isnum2 |
⊢ ( 𝐴 ∈ dom card ↔ ∃ 𝑥 ∈ On 𝑥 ≈ 𝐴 ) |
4 |
|
ensym |
⊢ ( 𝑥 ≈ 𝐴 → 𝐴 ≈ 𝑥 ) |
5 |
|
simprl |
⊢ ( ( ¬ 𝐴 ∈ Fin ∧ ( 𝑥 ∈ On ∧ 𝐴 ≈ 𝑥 ) ) → 𝑥 ∈ On ) |
6 |
|
enfi |
⊢ ( 𝐴 ≈ 𝑥 → ( 𝐴 ∈ Fin ↔ 𝑥 ∈ Fin ) ) |
7 |
|
onfin |
⊢ ( 𝑥 ∈ On → ( 𝑥 ∈ Fin ↔ 𝑥 ∈ ω ) ) |
8 |
6 7
|
sylan9bbr |
⊢ ( ( 𝑥 ∈ On ∧ 𝐴 ≈ 𝑥 ) → ( 𝐴 ∈ Fin ↔ 𝑥 ∈ ω ) ) |
9 |
8
|
biimprd |
⊢ ( ( 𝑥 ∈ On ∧ 𝐴 ≈ 𝑥 ) → ( 𝑥 ∈ ω → 𝐴 ∈ Fin ) ) |
10 |
9
|
con3d |
⊢ ( ( 𝑥 ∈ On ∧ 𝐴 ≈ 𝑥 ) → ( ¬ 𝐴 ∈ Fin → ¬ 𝑥 ∈ ω ) ) |
11 |
10
|
impcom |
⊢ ( ( ¬ 𝐴 ∈ Fin ∧ ( 𝑥 ∈ On ∧ 𝐴 ≈ 𝑥 ) ) → ¬ 𝑥 ∈ ω ) |
12 |
5 11
|
eldifd |
⊢ ( ( ¬ 𝐴 ∈ Fin ∧ ( 𝑥 ∈ On ∧ 𝐴 ≈ 𝑥 ) ) → 𝑥 ∈ ( On ∖ ω ) ) |
13 |
|
simprr |
⊢ ( ( ¬ 𝐴 ∈ Fin ∧ ( 𝑥 ∈ On ∧ 𝐴 ≈ 𝑥 ) ) → 𝐴 ≈ 𝑥 ) |
14 |
12 13
|
jca |
⊢ ( ( ¬ 𝐴 ∈ Fin ∧ ( 𝑥 ∈ On ∧ 𝐴 ≈ 𝑥 ) ) → ( 𝑥 ∈ ( On ∖ ω ) ∧ 𝐴 ≈ 𝑥 ) ) |
15 |
4 14
|
sylanr2 |
⊢ ( ( ¬ 𝐴 ∈ Fin ∧ ( 𝑥 ∈ On ∧ 𝑥 ≈ 𝐴 ) ) → ( 𝑥 ∈ ( On ∖ ω ) ∧ 𝐴 ≈ 𝑥 ) ) |
16 |
15
|
ex |
⊢ ( ¬ 𝐴 ∈ Fin → ( ( 𝑥 ∈ On ∧ 𝑥 ≈ 𝐴 ) → ( 𝑥 ∈ ( On ∖ ω ) ∧ 𝐴 ≈ 𝑥 ) ) ) |
17 |
16
|
reximdv2 |
⊢ ( ¬ 𝐴 ∈ Fin → ( ∃ 𝑥 ∈ On 𝑥 ≈ 𝐴 → ∃ 𝑥 ∈ ( On ∖ ω ) 𝐴 ≈ 𝑥 ) ) |
18 |
17
|
com12 |
⊢ ( ∃ 𝑥 ∈ On 𝑥 ≈ 𝐴 → ( ¬ 𝐴 ∈ Fin → ∃ 𝑥 ∈ ( On ∖ ω ) 𝐴 ≈ 𝑥 ) ) |
19 |
3 18
|
sylbi |
⊢ ( 𝐴 ∈ dom card → ( ¬ 𝐴 ∈ Fin → ∃ 𝑥 ∈ ( On ∖ ω ) 𝐴 ≈ 𝑥 ) ) |
20 |
19
|
con1d |
⊢ ( 𝐴 ∈ dom card → ( ¬ ∃ 𝑥 ∈ ( On ∖ ω ) 𝐴 ≈ 𝑥 → 𝐴 ∈ Fin ) ) |
21 |
2 20
|
syl5com |
⊢ ( 𝐴 ∈ FinVII → ( 𝐴 ∈ dom card → 𝐴 ∈ Fin ) ) |
22 |
|
eldifi |
⊢ ( 𝑥 ∈ ( On ∖ ω ) → 𝑥 ∈ On ) |
23 |
|
ensym |
⊢ ( 𝐴 ≈ 𝑥 → 𝑥 ≈ 𝐴 ) |
24 |
|
isnumi |
⊢ ( ( 𝑥 ∈ On ∧ 𝑥 ≈ 𝐴 ) → 𝐴 ∈ dom card ) |
25 |
22 23 24
|
syl2an |
⊢ ( ( 𝑥 ∈ ( On ∖ ω ) ∧ 𝐴 ≈ 𝑥 ) → 𝐴 ∈ dom card ) |
26 |
25
|
rexlimiva |
⊢ ( ∃ 𝑥 ∈ ( On ∖ ω ) 𝐴 ≈ 𝑥 → 𝐴 ∈ dom card ) |
27 |
26
|
con3i |
⊢ ( ¬ 𝐴 ∈ dom card → ¬ ∃ 𝑥 ∈ ( On ∖ ω ) 𝐴 ≈ 𝑥 ) |
28 |
|
isfin7 |
⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ FinVII ↔ ¬ ∃ 𝑥 ∈ ( On ∖ ω ) 𝐴 ≈ 𝑥 ) ) |
29 |
27 28
|
syl5ibr |
⊢ ( 𝐴 ∈ 𝑉 → ( ¬ 𝐴 ∈ dom card → 𝐴 ∈ FinVII ) ) |
30 |
|
fin17 |
⊢ ( 𝐴 ∈ Fin → 𝐴 ∈ FinVII ) |
31 |
30
|
a1i |
⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ Fin → 𝐴 ∈ FinVII ) ) |
32 |
29 31
|
jad |
⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝐴 ∈ dom card → 𝐴 ∈ Fin ) → 𝐴 ∈ FinVII ) ) |
33 |
21 32
|
impbid2 |
⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ FinVII ↔ ( 𝐴 ∈ dom card → 𝐴 ∈ Fin ) ) ) |