Description: The expression CHOICE will be used as a readable shorthand for any form of the axiom of choice; all concrete forms are long, cryptic, have dummy variables, or all three, making it useful to have a short name. Similar to the Axiom of Choice (first form) of Enderton p. 49.
There is a slight problem with taking the exact form of ax-ac as our definition, because the equivalence to more standard forms ( dfac2 ) requires the Axiom of Regularity, which we often try to avoid. Thus, we take the first of the "textbook forms" as the definition and derive the form of ax-ac itself as dfac0 . (Contributed by Mario Carneiro, 22-Feb-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-ac | ⊢ ( CHOICE ↔ ∀ 𝑥 ∃ 𝑓 ( 𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | wac | ⊢ CHOICE | |
| 1 | vx | ⊢ 𝑥 | |
| 2 | vf | ⊢ 𝑓 | |
| 3 | 2 | cv | ⊢ 𝑓 |
| 4 | 1 | cv | ⊢ 𝑥 |
| 5 | 3 4 | wss | ⊢ 𝑓 ⊆ 𝑥 |
| 6 | 4 | cdm | ⊢ dom 𝑥 |
| 7 | 3 6 | wfn | ⊢ 𝑓 Fn dom 𝑥 |
| 8 | 5 7 | wa | ⊢ ( 𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥 ) |
| 9 | 8 2 | wex | ⊢ ∃ 𝑓 ( 𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥 ) |
| 10 | 9 1 | wal | ⊢ ∀ 𝑥 ∃ 𝑓 ( 𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥 ) |
| 11 | 0 10 | wb | ⊢ ( CHOICE ↔ ∀ 𝑥 ∃ 𝑓 ( 𝑓 ⊆ 𝑥 ∧ 𝑓 Fn dom 𝑥 ) ) |