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 ( ( 𝐴𝐹𝐵𝐴 ) → 𝐵𝐹 )