Metamath Proof Explorer

Theorem dfacfin7

Description: Axiom of Choice equivalent: the VII-finite sets are the same as I-finite sets. (Contributed by Mario Carneiro, 18-May-2015)

Ref Expression
Assertion dfacfin7 ⊢ CHOICE ↔ FinVII = Fin

Proof

Step Hyp Ref Expression
1 ssequn2 ⊢ V ∖ dom ⁡ card ⊆ Fin ↔ Fin ∪ V ∖ dom ⁡ card = Fin
2 dfac10 ⊢ CHOICE ↔ dom ⁡ card = V
3 finnum ⊢ x ∈ Fin → x ∈ dom ⁡ card
4 3 ssriv ⊢ Fin ⊆ dom ⁡ card
5 ssequn2 ⊢ Fin ⊆ dom ⁡ card ↔ dom ⁡ card ∪ Fin = dom ⁡ card
6 4 5 mpbi ⊢ dom ⁡ card ∪ Fin = dom ⁡ card
7 6 eqeq1i ⊢ dom ⁡ card ∪ Fin = V ↔ dom ⁡ card = V
8 2 7 bitr4i ⊢ CHOICE ↔ dom ⁡ card ∪ Fin = V
9 ssv ⊢ dom ⁡ card ∪ Fin ⊆ V
10 eqss ⊢ dom ⁡ card ∪ Fin = V ↔ dom ⁡ card ∪ Fin ⊆ V ∧ V ⊆ dom ⁡ card ∪ Fin
11 9 10 mpbiran ⊢ dom ⁡ card ∪ Fin = V ↔ V ⊆ dom ⁡ card ∪ Fin
12 ssundif ⊢ V ⊆ dom ⁡ card ∪ Fin ↔ V ∖ dom ⁡ card ⊆ Fin
13 8 11 12 3bitri ⊢ CHOICE ↔ V ∖ dom ⁡ card ⊆ Fin
14 dffin7-2 ⊢ FinVII = Fin ∪ V ∖ dom ⁡ card
15 14 eqeq1i ⊢ FinVII = Fin ↔ Fin ∪ V ∖ dom ⁡ card = Fin
16 1 13 15 3bitr4i ⊢ CHOICE ↔ FinVII = Fin