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 )