Description: An alternate definition of double existential uniqueness (see 2eu4 ). A mistake sometimes made in the literature is to use E! x E! y to mean "exactly one x and exactly one y ". (For example, see Proposition 7.53 of TakeutiZaring p. 53.) It turns out that this is actually a weaker assertion, as can be seen by expanding out the formal definitions. This theorem shows that the erroneous definition can be repaired by conjoining A. x E* y ph as an additional condition. The correct definition apparently has never been published ( E* means "there exists at most one"). (Contributed by NM, 26-Oct-2003) Avoid ax-13 . (Revised by Wolf Lammen, 2-Oct-2023)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | 2eu5 | |- ( ( E! x E! y ph /\ A. x E* y ph ) <-> ( E. x E. y ph /\ E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 2eu1v | |- ( A. x E* y ph -> ( E! x E! y ph <-> ( E! x E. y ph /\ E! y E. x ph ) ) ) |
|
| 2 | 1 | pm5.32ri | |- ( ( E! x E! y ph /\ A. x E* y ph ) <-> ( ( E! x E. y ph /\ E! y E. x ph ) /\ A. x E* y ph ) ) |
| 3 | eumo | |- ( E! y E. x ph -> E* y E. x ph ) |
|
| 4 | 3 | adantl | |- ( ( E! x E. y ph /\ E! y E. x ph ) -> E* y E. x ph ) |
| 5 | 2moexv | |- ( E* y E. x ph -> A. x E* y ph ) |
|
| 6 | 4 5 | syl | |- ( ( E! x E. y ph /\ E! y E. x ph ) -> A. x E* y ph ) |
| 7 | 6 | pm4.71i | |- ( ( E! x E. y ph /\ E! y E. x ph ) <-> ( ( E! x E. y ph /\ E! y E. x ph ) /\ A. x E* y ph ) ) |
| 8 | 2eu4 | |- ( ( E! x E. y ph /\ E! y E. x ph ) <-> ( E. x E. y ph /\ E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) ) ) |
|
| 9 | 2 7 8 | 3bitr2i | |- ( ( E! x E! y ph /\ A. x E* y ph ) <-> ( E. x E. y ph /\ E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) ) ) |