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 ∃ r r We x

Proof

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