Metamath Proof Explorer


Theorem fin17

Description: Every I-finite set is VII-finite. (Contributed by Mario Carneiro, 17-May-2015)

Ref Expression
Assertion fin17 AFinAFinVII

Proof

Step Hyp Ref Expression
1 eldif bOnωbOn¬bω
2 enfi AbAFinbFin
3 onfin bOnbFinbω
4 2 3 sylan9bbr bOnAbAFinbω
5 4 biimpd bOnAbAFinbω
6 5 con3d bOnAb¬bω¬AFin
7 6 impancom bOn¬bωAb¬AFin
8 1 7 sylbi bOnωAb¬AFin
9 8 rexlimiv bOnωAb¬AFin
10 9 con2i AFin¬bOnωAb
11 isfin7 AFinAFinVII¬bOnωAb
12 10 11 mpbird AFinAFinVII