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

Metamath Proof Explorer

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 𝑥 )