Theorem ssfin2

Description: A subset of a II-finite set is II-finite. (Contributed by Stefan O'Rear, 2-Nov-2014) (Revised by Mario Carneiro, 16-May-2015)

	Ref	Expression
Assertion	ssfin2	⊢ ( ( 𝐴 ∈ FinII ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ∈ FinII )

Proof

Step	Hyp	Ref	Expression
1		simpll	⊢ ( ( ( 𝐴 ∈ FinII ∧ 𝐵 ⊆ 𝐴 ) ∧ 𝑥 ∈ 𝒫 𝒫 𝐵 ) → 𝐴 ∈ FinII )
2		elpwi	⊢ ( 𝑥 ∈ 𝒫 𝒫 𝐵 → 𝑥 ⊆ 𝒫 𝐵 )
3	2	adantl	⊢ ( ( ( 𝐴 ∈ FinII ∧ 𝐵 ⊆ 𝐴 ) ∧ 𝑥 ∈ 𝒫 𝒫 𝐵 ) → 𝑥 ⊆ 𝒫 𝐵 )
4		simplr	⊢ ( ( ( 𝐴 ∈ FinII ∧ 𝐵 ⊆ 𝐴 ) ∧ 𝑥 ∈ 𝒫 𝒫 𝐵 ) → 𝐵 ⊆ 𝐴 )
5		sspwb	⊢ ( 𝐵 ⊆ 𝐴 ↔ 𝒫 𝐵 ⊆ 𝒫 𝐴 )
6	4 5	sylib	⊢ ( ( ( 𝐴 ∈ FinII ∧ 𝐵 ⊆ 𝐴 ) ∧ 𝑥 ∈ 𝒫 𝒫 𝐵 ) → 𝒫 𝐵 ⊆ 𝒫 𝐴 )
7	3 6	sstrd	⊢ ( ( ( 𝐴 ∈ FinII ∧ 𝐵 ⊆ 𝐴 ) ∧ 𝑥 ∈ 𝒫 𝒫 𝐵 ) → 𝑥 ⊆ 𝒫 𝐴 )
8		fin2i	⊢ ( ( ( 𝐴 ∈ FinII ∧ 𝑥 ⊆ 𝒫 𝐴 ) ∧ ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) → ∪ 𝑥 ∈ 𝑥 )
9	8	ex	⊢ ( ( 𝐴 ∈ FinII ∧ 𝑥 ⊆ 𝒫 𝐴 ) → ( ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) → ∪ 𝑥 ∈ 𝑥 ) )
10	1 7 9	syl2anc	⊢ ( ( ( 𝐴 ∈ FinII ∧ 𝐵 ⊆ 𝐴 ) ∧ 𝑥 ∈ 𝒫 𝒫 𝐵 ) → ( ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) → ∪ 𝑥 ∈ 𝑥 ) )
11	10	ralrimiva	⊢ ( ( 𝐴 ∈ FinII ∧ 𝐵 ⊆ 𝐴 ) → ∀ 𝑥 ∈ 𝒫 𝒫 𝐵 ( ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) → ∪ 𝑥 ∈ 𝑥 ) )
12		ssexg	⊢ ( ( 𝐵 ⊆ 𝐴 ∧ 𝐴 ∈ FinII ) → 𝐵 ∈ V )
13	12	ancoms	⊢ ( ( 𝐴 ∈ FinII ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ∈ V )
14		isfin2	⊢ ( 𝐵 ∈ V → ( 𝐵 ∈ FinII ↔ ∀ 𝑥 ∈ 𝒫 𝒫 𝐵 ( ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) → ∪ 𝑥 ∈ 𝑥 ) ) )
15	13 14	syl	⊢ ( ( 𝐴 ∈ FinII ∧ 𝐵 ⊆ 𝐴 ) → ( 𝐵 ∈ FinII ↔ ∀ 𝑥 ∈ 𝒫 𝒫 𝐵 ( ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) → ∪ 𝑥 ∈ 𝑥 ) ) )
16	11 15	mpbird	⊢ ( ( 𝐴 ∈ FinII ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ∈ FinII )