Description: Every I-finite set is Ia-finite. (Contributed by Stefan O'Rear, 30-Oct-2014) (Revised by Mario Carneiro, 17-May-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | fin11a | |- ( A e. Fin -> A e. Fin1a ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elpwi | |- ( x e. ~P A -> x C_ A ) |
|
2 | ssfi | |- ( ( A e. Fin /\ x C_ A ) -> x e. Fin ) |
|
3 | 1 2 | sylan2 | |- ( ( A e. Fin /\ x e. ~P A ) -> x e. Fin ) |
4 | 3 | orcd | |- ( ( A e. Fin /\ x e. ~P A ) -> ( x e. Fin \/ ( A \ x ) e. Fin ) ) |
5 | 4 | ralrimiva | |- ( A e. Fin -> A. x e. ~P A ( x e. Fin \/ ( A \ x ) e. Fin ) ) |
6 | isfin1a | |- ( A e. Fin -> ( A e. Fin1a <-> A. x e. ~P A ( x e. Fin \/ ( A \ x ) e. Fin ) ) ) |
|
7 | 5 6 | mpbird | |- ( A e. Fin -> A e. Fin1a ) |