Theorem dfac13

Description: The axiom of choice holds iff every set has choice sequences as long as itself. (Contributed by Mario Carneiro, 3-Sep-2015)

	Ref	Expression
Assertion	dfac13	⊢ ( CHOICE ↔ ∀ 𝑥 𝑥 ∈ AC 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑥 ∈ V
2		acacni	⊢ ( ( CHOICE ∧ 𝑥 ∈ V ) → AC 𝑥 = V )
3	2	elvd	⊢ ( CHOICE → AC 𝑥 = V )
4	1 3	eleqtrrid	⊢ ( CHOICE → 𝑥 ∈ AC 𝑥 )
5	4	alrimiv	⊢ ( CHOICE → ∀ 𝑥 𝑥 ∈ AC 𝑥 )
6		vpwex	⊢ 𝒫 𝑧 ∈ V
7		id	⊢ ( 𝑥 = 𝒫 𝑧 → 𝑥 = 𝒫 𝑧 )
8		acneq	⊢ ( 𝑥 = 𝒫 𝑧 → AC 𝑥 = AC 𝒫 𝑧 )
9	7 8	eleq12d	⊢ ( 𝑥 = 𝒫 𝑧 → ( 𝑥 ∈ AC 𝑥 ↔ 𝒫 𝑧 ∈ AC 𝒫 𝑧 ) )
10	6 9	spcv	⊢ ( ∀ 𝑥 𝑥 ∈ AC 𝑥 → 𝒫 𝑧 ∈ AC 𝒫 𝑧 )
11		vex	⊢ 𝑦 ∈ V
12		vex	⊢ 𝑧 ∈ V
13	12	canth2	⊢ 𝑧 ≺ 𝒫 𝑧
14		sdomdom	⊢ ( 𝑧 ≺ 𝒫 𝑧 → 𝑧 ≼ 𝒫 𝑧 )
15		acndom2	⊢ ( 𝑧 ≼ 𝒫 𝑧 → ( 𝒫 𝑧 ∈ AC 𝒫 𝑧 → 𝑧 ∈ AC 𝒫 𝑧 ) )
16	13 14 15	mp2b	⊢ ( 𝒫 𝑧 ∈ AC 𝒫 𝑧 → 𝑧 ∈ AC 𝒫 𝑧 )
17		acnnum	⊢ ( 𝑧 ∈ AC 𝒫 𝑧 ↔ 𝑧 ∈ dom card )
18	16 17	sylib	⊢ ( 𝒫 𝑧 ∈ AC 𝒫 𝑧 → 𝑧 ∈ dom card )
19		numacn	⊢ ( 𝑦 ∈ V → ( 𝑧 ∈ dom card → 𝑧 ∈ AC 𝑦 ) )
20	11 18 19	mpsyl	⊢ ( 𝒫 𝑧 ∈ AC 𝒫 𝑧 → 𝑧 ∈ AC 𝑦 )
21	10 20	syl	⊢ ( ∀ 𝑥 𝑥 ∈ AC 𝑥 → 𝑧 ∈ AC 𝑦 )
22	12	a1i	⊢ ( ∀ 𝑥 𝑥 ∈ AC 𝑥 → 𝑧 ∈ V )
23	21 22	2thd	⊢ ( ∀ 𝑥 𝑥 ∈ AC 𝑥 → ( 𝑧 ∈ AC 𝑦 ↔ 𝑧 ∈ V ) )
24	23	eqrdv	⊢ ( ∀ 𝑥 𝑥 ∈ AC 𝑥 → AC 𝑦 = V )
25	24	alrimiv	⊢ ( ∀ 𝑥 𝑥 ∈ AC 𝑥 → ∀ 𝑦 AC 𝑦 = V )
26		dfacacn	⊢ ( CHOICE ↔ ∀ 𝑦 AC 𝑦 = V )
27	25 26	sylibr	⊢ ( ∀ 𝑥 𝑥 ∈ AC 𝑥 → CHOICE )
28	5 27	impbii	⊢ ( CHOICE ↔ ∀ 𝑥 𝑥 ∈ AC 𝑥 )