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 ∪ 𝐴 → ∃ 𝑓 ∀ 𝑧 ∈ 𝐴 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) )