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

Metamath Proof Explorer

Theorem dfac8c

Description: If the union of a set is well-orderable, then the set has a choice function. (Contributed by Mario Carneiro, 5-Jan-2013)

Ref Expression
Assertion dfac8c ( 𝐴 ∈ 𝐵 → ( ∃ 𝑟 𝑟 We ∪ 𝐴 → ∃ 𝑓 ∀ 𝑧 ∈ 𝐴 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( 𝑥 ∈ ( 𝐴 ∖ { ∅ } ) ↦ ( ℩ 𝑦 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ¬ 𝑤 𝑟 𝑦 ) ) = ( 𝑥 ∈ ( 𝐴 ∖ { ∅ } ) ↦ ( ℩ 𝑦 ∈ 𝑥 ∀ 𝑤 ∈ 𝑥 ¬ 𝑤 𝑟 𝑦 ) )
2 1 dfac8clem ⊢ ( 𝐴 ∈ 𝐵 → ( ∃ 𝑟 𝑟 We ∪ 𝐴 → ∃ 𝑓 ∀ 𝑧 ∈ 𝐴 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) )