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

Metamath Proof Explorer

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

Proof

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