Step |
Hyp |
Ref |
Expression |
1 |
|
ackbij.f |
⊢ 𝐹 = ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑦 ∈ 𝑥 ( { 𝑦 } × 𝒫 𝑦 ) ) ) |
2 |
|
ssexg |
⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ) → 𝐵 ∈ V ) |
3 |
|
elinel1 |
⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → 𝐴 ∈ 𝒫 ω ) |
4 |
3
|
elpwid |
⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → 𝐴 ⊆ ω ) |
5 |
|
sstr |
⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐴 ⊆ ω ) → 𝐵 ⊆ ω ) |
6 |
4 5
|
sylan2 |
⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ) → 𝐵 ⊆ ω ) |
7 |
2 6
|
elpwd |
⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ) → 𝐵 ∈ 𝒫 ω ) |
8 |
7
|
ancoms |
⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ∈ 𝒫 ω ) |
9 |
|
elinel2 |
⊢ ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) → 𝐴 ∈ Fin ) |
10 |
|
ssfi |
⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ∈ Fin ) |
11 |
9 10
|
sylan |
⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ∈ Fin ) |
12 |
8 11
|
elind |
⊢ ( ( 𝐴 ∈ ( 𝒫 ω ∩ Fin ) ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ∈ ( 𝒫 ω ∩ Fin ) ) |