Metamath Proof Explorer

Theorem ackbij1lem3

Description: Lemma for ackbij2 . (Contributed by Stefan O'Rear, 18-Nov-2014)

Ref Expression
Assertion ackbij1lem3 
|- ( A e. _om -> A e. ( ~P _om i^i Fin ) )

Proof

Step Hyp Ref Expression
1 ordom 
 |-  Ord _om
2 ordelss 
 |-  ( ( Ord _om /\ A e. _om ) -> A C_ _om )
3 1 2 mpan 
 |-  ( A e. _om -> A C_ _om )
4 elpwg 
 |-  ( A e. _om -> ( A e. ~P _om <-> A C_ _om ) )
5 3 4 mpbird 
 |-  ( A e. _om -> A e. ~P _om )
6 nnfi 
 |-  ( A e. _om -> A e. Fin )
7 5 6 elind 
 |-  ( A e. _om -> A e. ( ~P _om i^i Fin ) )