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

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 ( 𝐴 ∈ dom card ↔ ∃ 𝑟 𝑟 We 𝐴 )

Proof

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