This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝑥 ∈ Fin → 𝑥 ∈ 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 )