Metamath Proof Explorer

Theorem dfac8

Description: A proof of the equivalency of the well-ordering theorem weth and the axiom of choice ac7 . (Contributed by Mario Carneiro, 5-Jan-2013)

Ref Expression
Assertion dfac8 ⊢CHOICE↔∀x∃rrWex

Proof

Step Hyp Ref Expression
1 dfac3 ⊢CHOICE↔∀y∃f∀z∈yz≠∅→f⁡z∈z
2 vex ⊢x∈V
3 vpwex ⊢𝒫x∈V
4 raleq ⊢y=𝒫x→∀z∈yz≠∅→f⁡z∈z↔∀z∈𝒫xz≠∅→f⁡z∈z
5 4 exbidv ⊢y=𝒫x→∃f∀z∈yz≠∅→f⁡z∈z↔∃f∀z∈𝒫xz≠∅→f⁡z∈z
6 3 5 spcv ⊢∀y∃f∀z∈yz≠∅→f⁡z∈z→∃f∀z∈𝒫xz≠∅→f⁡z∈z
7 dfac8a ⊢x∈V→∃f∀z∈𝒫xz≠∅→f⁡z∈z→x∈dom⁡card
8 2 6 7 mpsyl ⊢∀y∃f∀z∈yz≠∅→f⁡z∈z→x∈dom⁡card
9 dfac8b ⊢x∈dom⁡card→∃rrWex
10 8 9 syl ⊢∀y∃f∀z∈yz≠∅→f⁡z∈z→∃rrWex
11 10 alrimiv ⊢∀y∃f∀z∈yz≠∅→f⁡z∈z→∀x∃rrWex
12 vex ⊢y∈V
13 vuniex ⊢⋃y∈V
14 weeq2 ⊢x=⋃y→rWex↔rWe⋃y
15 14 exbidv ⊢x=⋃y→∃rrWex↔∃rrWe⋃y
16 13 15 spcv ⊢∀x∃rrWex→∃rrWe⋃y
17 dfac8c ⊢y∈V→∃rrWe⋃y→∃f∀z∈yz≠∅→f⁡z∈z
18 12 16 17 mpsyl ⊢∀x∃rrWex→∃f∀z∈yz≠∅→f⁡z∈z
19 18 alrimiv ⊢∀x∃rrWex→∀y∃f∀z∈yz≠∅→f⁡z∈z
20 11 19 impbii ⊢∀y∃f∀z∈yz≠∅→f⁡z∈z↔∀x∃rrWex
21 1 20 bitri ⊢CHOICE↔∀x∃rrWex