Metamath Proof Explorer

Theorem ween

Description: A set is numerable iff it can be well-ordered. (Contributed by Mario Carneiro, 5-Jan-2013)

Ref Expression
Assertion ween ⊢ A ∈ dom ⁡ card ↔ ∃ r r We A

Proof

Step Hyp Ref Expression
1 dfac8b ⊢ A ∈ dom ⁡ card → ∃ r r We A
2 weso ⊢ r We A → r Or A
3 vex ⊢ r ∈ V
4 soex ⊢ r Or A ∧ r ∈ V → A ∈ V
5 2 3 4 sylancl ⊢ r We A → A ∈ V
6 5 exlimiv ⊢ ∃ r r We A → A ∈ V
7 unipw ⊢ ⋃ 𝒫 A = A
8 weeq2 ⊢ ⋃ 𝒫 A = A → r We ⋃ 𝒫 A ↔ r We A
9 7 8 ax-mp ⊢ r We ⋃ 𝒫 A ↔ r We A
10 9 exbii ⊢ ∃ r r We ⋃ 𝒫 A ↔ ∃ r r We A
11 10 biimpri ⊢ ∃ r r We A → ∃ r r We ⋃ 𝒫 A
12 pwexg ⊢ A ∈ V → 𝒫 A ∈ V
13 dfac8c ⊢ 𝒫 A ∈ V → ∃ r r We ⋃ 𝒫 A → ∃ f ∀ x ∈ 𝒫 A x ≠ ∅ → f ⁡ x ∈ x
14 12 13 syl ⊢ A ∈ V → ∃ r r We ⋃ 𝒫 A → ∃ f ∀ x ∈ 𝒫 A x ≠ ∅ → f ⁡ x ∈ x
15 dfac8a ⊢ A ∈ V → ∃ f ∀ x ∈ 𝒫 A x ≠ ∅ → f ⁡ x ∈ x → A ∈ dom ⁡ card
16 14 15 syld ⊢ A ∈ V → ∃ r r We ⋃ 𝒫 A → A ∈ dom ⁡ card
17 6 11 16 sylc ⊢ ∃ r r We A → A ∈ dom ⁡ card
18 1 17 impbii ⊢ A ∈ dom ⁡ card ↔ ∃ r r We A