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	$⊢ \neg ω \in V \leftrightarrow Fin = V$

Proof

Step	Hyp	Ref	Expression
1		ssv	$⊢ Fin \subseteq V$
2	1	a1i	$⊢ \neg ω \in V \to Fin \subseteq V$
3		vex	$⊢ a \in V$
4		fineqvlem	$⊢ (a \in V \land \neg a \in Fin) \to ω ≼ 𝒫 𝒫 a$
5	3 4	mpan	$⊢ \neg a \in Fin \to ω ≼ 𝒫 𝒫 a$
6		reldom	$⊢ Rel ≼$
7	6	brrelex1i	$⊢ ω ≼ 𝒫 𝒫 a \to ω \in V$
8	5 7	syl	$⊢ \neg a \in Fin \to ω \in V$
9	8	con1i	$⊢ \neg ω \in V \to a \in Fin$
10	9	a1d	$⊢ \neg ω \in V \to (a \in V \to a \in Fin)$
11	10	ssrdv	$⊢ \neg ω \in V \to V \subseteq Fin$
12	2 11	eqssd	$⊢ \neg ω \in V \to Fin = V$
13		ominf	$⊢ \neg ω \in Fin$
14		eleq2	$⊢ Fin = V \to (ω \in Fin \leftrightarrow ω \in V)$
15	13 14	mtbii	$⊢ Fin = V \to \neg ω \in V$
16	12 15	impbii	$⊢ \neg ω \in V \leftrightarrow Fin = V$