This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ssfin3ds

Description: A subset of a III-finite set is III-finite. (Contributed by Stefan O'Rear, 4-Nov-2014)

Ref Expression
Hypothesis isfin3ds.f ⊢ 𝐹 = { 𝑔 ∣ ∀ 𝑎 ∈ ( 𝒫 𝑔 ↑m ω ) ( ∀ 𝑏 ∈ ω ( 𝑎 ‘ suc 𝑏 ) ⊆ ( 𝑎 ‘ 𝑏 ) → ∩ ran 𝑎 ∈ ran 𝑎 ) }
Assertion ssfin3ds ( ( 𝐴 ∈ 𝐹 ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ∈ 𝐹 )

Proof

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 ⊢ ( ( 𝐴 ∈ 𝐹 ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ∈ 𝐹 )