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

Proof

Step Hyp Ref Expression
1 ssv ⊢ Fin ⊆ V
2 1 a1i ⊢ ¬ ω ∈ V → Fin ⊆ V
3 vex ⊢ a ∈ V
4 fineqvlem ⊢ a ∈ V ∧ ¬ a ∈ Fin → ω ≼ 𝒫 𝒫 a
5 3 4 mpan ⊢ ¬ a ∈ Fin → ω ≼ 𝒫 𝒫 a
6 reldom ⊢ Rel ⁡ ≼
7 6 brrelex1i ⊢ ω ≼ 𝒫 𝒫 a → ω ∈ V
8 5 7 syl ⊢ ¬ a ∈ Fin → ω ∈ V
9 8 con1i ⊢ ¬ ω ∈ V → a ∈ Fin
10 9 a1d ⊢ ¬ ω ∈ V → a ∈ V → a ∈ 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