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 
|- ( ( A e. Fin2 /\ B C_ A ) -> B e. Fin2 )

Proof

Step Hyp Ref Expression
1 simpll 
 |-  ( ( ( A e. Fin2 /\ B C_ A ) /\ x e. ~P ~P B ) -> A e. Fin2 )
2 elpwi 
 |-  ( x e. ~P ~P B -> x C_ ~P B )
3 2 adantl 
 |-  ( ( ( A e. Fin2 /\ B C_ A ) /\ x e. ~P ~P B ) -> x C_ ~P B )
4 simplr 
 |-  ( ( ( A e. Fin2 /\ B C_ A ) /\ x e. ~P ~P B ) -> B C_ A )
5 4 sspwd 
 |-  ( ( ( A e. Fin2 /\ B C_ A ) /\ x e. ~P ~P B ) -> ~P B C_ ~P A )
6 3 5 sstrd 
 |-  ( ( ( A e. Fin2 /\ B C_ A ) /\ x e. ~P ~P B ) -> x C_ ~P A )
7 fin2i 
 |-  ( ( ( A e. Fin2 /\ x C_ ~P A ) /\ ( x =/= (/) /\ [C.] Or x ) ) -> U. x e. x )
8 7 ex 
 |-  ( ( A e. Fin2 /\ x C_ ~P A ) -> ( ( x =/= (/) /\ [C.] Or x ) -> U. x e. x ) )
9 1 6 8 syl2anc 
 |-  ( ( ( A e. Fin2 /\ B C_ A ) /\ x e. ~P ~P B ) -> ( ( x =/= (/) /\ [C.] Or x ) -> U. x e. x ) )
10 9 ralrimiva 
 |-  ( ( A e. Fin2 /\ B C_ A ) -> A. x e. ~P ~P B ( ( x =/= (/) /\ [C.] Or x ) -> U. x e. x ) )
11 ssexg 
 |-  ( ( B C_ A /\ A e. Fin2 ) -> B e. _V )
12 11 ancoms 
 |-  ( ( A e. Fin2 /\ B C_ A ) -> B e. _V )
13 isfin2 
 |-  ( B e. _V -> ( B e. Fin2 <-> A. x e. ~P ~P B ( ( x =/= (/) /\ [C.] Or x ) -> U. x e. x ) ) )
14 12 13 syl 
 |-  ( ( A e. Fin2 /\ B C_ A ) -> ( B e. Fin2 <-> A. x e. ~P ~P B ( ( x =/= (/) /\ [C.] Or x ) -> U. x e. x ) ) )
15 10 14 mpbird 
 |-  ( ( A e. Fin2 /\ B C_ A ) -> B e. Fin2 )