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