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 )