Step |
Hyp |
Ref |
Expression |
1 |
|
isfin3ds.f |
⊢ 𝐹 = { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑏 ∈ ω ( 𝑎 ‘ suc 𝑏 ) ⊆ ( 𝑎 ‘ 𝑏 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) } |
2 |
|
pwexg |
⊢ ( 𝐴 ∈ 𝐹 → 𝒫 𝐴 ∈ V ) |
3 |
|
simpr |
⊢ ( ( 𝐴 ∈ 𝐹 ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ⊆ 𝐴 ) |
4 |
3
|
sspwd |
⊢ ( ( 𝐴 ∈ 𝐹 ∧ 𝐵 ⊆ 𝐴 ) → 𝒫 𝐵 ⊆ 𝒫 𝐴 ) |
5 |
|
mapss |
⊢ ( ( 𝒫 𝐴 ∈ V ∧ 𝒫 𝐵 ⊆ 𝒫 𝐴 ) → ( 𝒫 𝐵 ↑m ω ) ⊆ ( 𝒫 𝐴 ↑m ω ) ) |
6 |
2 4 5
|
syl2an2r |
⊢ ( ( 𝐴 ∈ 𝐹 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝒫 𝐵 ↑m ω ) ⊆ ( 𝒫 𝐴 ↑m ω ) ) |
7 |
1
|
isfin3ds |
⊢ ( 𝐴 ∈ 𝐹 → ( 𝐴 ∈ 𝐹 ↔ ∀ 𝑓 ∈ ( 𝒫 𝐴 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑓 ‘ suc 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) → ∩ ran 𝑓 ∈ ran 𝑓 ) ) ) |
8 |
7
|
ibi |
⊢ ( 𝐴 ∈ 𝐹 → ∀ 𝑓 ∈ ( 𝒫 𝐴 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑓 ‘ suc 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) → ∩ ran 𝑓 ∈ ran 𝑓 ) ) |
9 |
8
|
adantr |
⊢ ( ( 𝐴 ∈ 𝐹 ∧ 𝐵 ⊆ 𝐴 ) → ∀ 𝑓 ∈ ( 𝒫 𝐴 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑓 ‘ suc 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) → ∩ ran 𝑓 ∈ ran 𝑓 ) ) |
10 |
|
ssralv |
⊢ ( ( 𝒫 𝐵 ↑m ω ) ⊆ ( 𝒫 𝐴 ↑m ω ) → ( ∀ 𝑓 ∈ ( 𝒫 𝐴 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑓 ‘ suc 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) → ∩ ran 𝑓 ∈ ran 𝑓 ) → ∀ 𝑓 ∈ ( 𝒫 𝐵 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑓 ‘ suc 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) → ∩ ran 𝑓 ∈ ran 𝑓 ) ) ) |
11 |
6 9 10
|
sylc |
⊢ ( ( 𝐴 ∈ 𝐹 ∧ 𝐵 ⊆ 𝐴 ) → ∀ 𝑓 ∈ ( 𝒫 𝐵 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑓 ‘ suc 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) → ∩ ran 𝑓 ∈ ran 𝑓 ) ) |
12 |
|
ssexg |
⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐴 ∈ 𝐹 ) → 𝐵 ∈ V ) |
13 |
12
|
ancoms |
⊢ ( ( 𝐴 ∈ 𝐹 ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ∈ V ) |
14 |
1
|
isfin3ds |
⊢ ( 𝐵 ∈ V → ( 𝐵 ∈ 𝐹 ↔ ∀ 𝑓 ∈ ( 𝒫 𝐵 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑓 ‘ suc 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) → ∩ ran 𝑓 ∈ ran 𝑓 ) ) ) |
15 |
13 14
|
syl |
⊢ ( ( 𝐴 ∈ 𝐹 ∧ 𝐵 ⊆ 𝐴 ) → ( 𝐵 ∈ 𝐹 ↔ ∀ 𝑓 ∈ ( 𝒫 𝐵 ↑m ω ) ( ∀ 𝑥 ∈ ω ( 𝑓 ‘ suc 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) → ∩ ran 𝑓 ∈ ran 𝑓 ) ) ) |
16 |
11 15
|
mpbird |
⊢ ( ( 𝐴 ∈ 𝐹 ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ∈ 𝐹 ) |