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	⊢ ( ¬ ω ∈ V ↔ Fin = V )

Proof

Step	Hyp	Ref	Expression
1		ssv	⊢ Fin ⊆ V
2	1	a1i	⊢ ( ¬ ω ∈ V → Fin ⊆ V )
3		vex	⊢ 𝑎 ∈ V
4		fineqvlem	⊢ ( ( 𝑎 ∈ V ∧ ¬ 𝑎 ∈ Fin ) → ω ≼ 𝒫 𝒫 𝑎 )
5	3 4	mpan	⊢ ( ¬ 𝑎 ∈ Fin → ω ≼ 𝒫 𝒫 𝑎 )
6		reldom	⊢ Rel ≼
7	6	brrelex1i	⊢ ( ω ≼ 𝒫 𝒫 𝑎 → ω ∈ V )
8	5 7	syl	⊢ ( ¬ 𝑎 ∈ Fin → ω ∈ V )
9	8	con1i	⊢ ( ¬ ω ∈ V → 𝑎 ∈ Fin )
10	9	a1d	⊢ ( ¬ ω ∈ V → ( 𝑎 ∈ V → 𝑎 ∈ Fin ) )
11	10	ssrdv	⊢ ( ¬ ω ∈ V → V ⊆ Fin )
12	2 11	eqssd	⊢ ( ¬ ω ∈ V → Fin = V )
13		ominf	⊢ ¬ ω ∈ Fin
14		eleq2	⊢ ( Fin = V → ( ω ∈ Fin ↔ ω ∈ V ) )
15	13 14	mtbii	⊢ ( Fin = V → ¬ ω ∈ V )
16	12 15	impbii	⊢ ( ¬ ω ∈ V ↔ Fin = V )