Step |
Hyp |
Ref |
Expression |
1 |
|
elex |
⊢ ( 𝐴 ∈ Fin → 𝐴 ∈ V ) |
2 |
|
elex |
⊢ ( 𝒫 𝒫 𝐴 ∈ FinIV → 𝒫 𝒫 𝐴 ∈ V ) |
3 |
|
pwexb |
⊢ ( 𝐴 ∈ V ↔ 𝒫 𝐴 ∈ V ) |
4 |
|
pwexb |
⊢ ( 𝒫 𝐴 ∈ V ↔ 𝒫 𝒫 𝐴 ∈ V ) |
5 |
3 4
|
bitri |
⊢ ( 𝐴 ∈ V ↔ 𝒫 𝒫 𝐴 ∈ V ) |
6 |
2 5
|
sylibr |
⊢ ( 𝒫 𝒫 𝐴 ∈ FinIV → 𝐴 ∈ V ) |
7 |
|
ominf |
⊢ ¬ ω ∈ Fin |
8 |
|
pwfi |
⊢ ( 𝐴 ∈ Fin ↔ 𝒫 𝐴 ∈ Fin ) |
9 |
|
pwfi |
⊢ ( 𝒫 𝐴 ∈ Fin ↔ 𝒫 𝒫 𝐴 ∈ Fin ) |
10 |
8 9
|
bitri |
⊢ ( 𝐴 ∈ Fin ↔ 𝒫 𝒫 𝐴 ∈ Fin ) |
11 |
|
domfi |
⊢ ( ( 𝒫 𝒫 𝐴 ∈ Fin ∧ ω ≼ 𝒫 𝒫 𝐴 ) → ω ∈ Fin ) |
12 |
11
|
expcom |
⊢ ( ω ≼ 𝒫 𝒫 𝐴 → ( 𝒫 𝒫 𝐴 ∈ Fin → ω ∈ Fin ) ) |
13 |
10 12
|
syl5bi |
⊢ ( ω ≼ 𝒫 𝒫 𝐴 → ( 𝐴 ∈ Fin → ω ∈ Fin ) ) |
14 |
7 13
|
mtoi |
⊢ ( ω ≼ 𝒫 𝒫 𝐴 → ¬ 𝐴 ∈ Fin ) |
15 |
|
fineqvlem |
⊢ ( ( 𝐴 ∈ V ∧ ¬ 𝐴 ∈ Fin ) → ω ≼ 𝒫 𝒫 𝐴 ) |
16 |
15
|
ex |
⊢ ( 𝐴 ∈ V → ( ¬ 𝐴 ∈ Fin → ω ≼ 𝒫 𝒫 𝐴 ) ) |
17 |
14 16
|
impbid2 |
⊢ ( 𝐴 ∈ V → ( ω ≼ 𝒫 𝒫 𝐴 ↔ ¬ 𝐴 ∈ Fin ) ) |
18 |
17
|
con2bid |
⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ Fin ↔ ¬ ω ≼ 𝒫 𝒫 𝐴 ) ) |
19 |
|
isfin4-2 |
⊢ ( 𝒫 𝒫 𝐴 ∈ V → ( 𝒫 𝒫 𝐴 ∈ FinIV ↔ ¬ ω ≼ 𝒫 𝒫 𝐴 ) ) |
20 |
5 19
|
sylbi |
⊢ ( 𝐴 ∈ V → ( 𝒫 𝒫 𝐴 ∈ FinIV ↔ ¬ ω ≼ 𝒫 𝒫 𝐴 ) ) |
21 |
18 20
|
bitr4d |
⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ Fin ↔ 𝒫 𝒫 𝐴 ∈ FinIV ) ) |
22 |
1 6 21
|
pm5.21nii |
⊢ ( 𝐴 ∈ Fin ↔ 𝒫 𝒫 𝐴 ∈ FinIV ) |