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

Metamath Proof Explorer

Theorem fineqv

Description: If the Axiom of Infinity is denied, then all sets are finite (which implies the Axiom of Choice). (Contributed by Mario Carneiro, 20-Jan-2013) (Revised by Mario Carneiro, 3-Jan-2015)

Ref Expression
Assertion fineqv 
|- ( -. _om e. _V <-> Fin = _V )

Proof

Step Hyp Ref Expression
1 ssv 
 |-  Fin C_ _V
2 1 a1i 
 |-  ( -. _om e. _V -> Fin C_ _V )
3 vex 
 |-  a e. _V
4 fineqvlem 
 |-  ( ( a e. _V /\ -. a e. Fin ) -> _om ~<_ ~P ~P a )
5 3 4 mpan 
 |-  ( -. a e. Fin -> _om ~<_ ~P ~P a )
6 reldom 
 |-  Rel ~<_
7 6 brrelex1i 
 |-  ( _om ~<_ ~P ~P a -> _om e. _V )
8 5 7 syl 
 |-  ( -. a e. Fin -> _om e. _V )
9 8 con1i 
 |-  ( -. _om e. _V -> a e. Fin )
10 9 a1d 
 |-  ( -. _om e. _V -> ( a e. _V -> a e. Fin ) )
11 10 ssrdv 
 |-  ( -. _om e. _V -> _V C_ Fin )
12 2 11 eqssd 
 |-  ( -. _om e. _V -> Fin = _V )
13 ominf 
 |-  -. _om e. Fin
14 eleq2 
 |-  ( Fin = _V -> ( _om e. Fin <-> _om e. _V ) )
15 13 14 mtbii 
 |-  ( Fin = _V -> -. _om e. _V )
16 12 15 impbii 
 |-  ( -. _om e. _V <-> Fin = _V )