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 "exists at most one"). (Contributed by NM, 26-Oct-2003) Avoid ax-13 . (Revised by Wolf Lammen, 2-Oct-2023)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | 2eu5 | ⊢ ( ( ∃! 𝑥 ∃! 𝑦 𝜑 ∧ ∀ 𝑥 ∃* 𝑦 𝜑 ) ↔ ( ∃ 𝑥 ∃ 𝑦 𝜑 ∧ ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 2eu1v | ⊢ ( ∀ 𝑥 ∃* 𝑦 𝜑 → ( ∃! 𝑥 ∃! 𝑦 𝜑 ↔ ( ∃! 𝑥 ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃ 𝑥 𝜑 ) ) ) | |
| 2 | 1 | pm5.32ri | ⊢ ( ( ∃! 𝑥 ∃! 𝑦 𝜑 ∧ ∀ 𝑥 ∃* 𝑦 𝜑 ) ↔ ( ( ∃! 𝑥 ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃ 𝑥 𝜑 ) ∧ ∀ 𝑥 ∃* 𝑦 𝜑 ) ) |
| 3 | eumo | ⊢ ( ∃! 𝑦 ∃ 𝑥 𝜑 → ∃* 𝑦 ∃ 𝑥 𝜑 ) | |
| 4 | 3 | adantl | ⊢ ( ( ∃! 𝑥 ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃ 𝑥 𝜑 ) → ∃* 𝑦 ∃ 𝑥 𝜑 ) |
| 5 | 2moexv | ⊢ ( ∃* 𝑦 ∃ 𝑥 𝜑 → ∀ 𝑥 ∃* 𝑦 𝜑 ) | |
| 6 | 4 5 | syl | ⊢ ( ( ∃! 𝑥 ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃ 𝑥 𝜑 ) → ∀ 𝑥 ∃* 𝑦 𝜑 ) |
| 7 | 6 | pm4.71i | ⊢ ( ( ∃! 𝑥 ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃ 𝑥 𝜑 ) ↔ ( ( ∃! 𝑥 ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃ 𝑥 𝜑 ) ∧ ∀ 𝑥 ∃* 𝑦 𝜑 ) ) |
| 8 | 2eu4 | ⊢ ( ( ∃! 𝑥 ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃ 𝑥 𝜑 ) ↔ ( ∃ 𝑥 ∃ 𝑦 𝜑 ∧ ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) ) | |
| 9 | 2 7 8 | 3bitr2i | ⊢ ( ( ∃! 𝑥 ∃! 𝑦 𝜑 ∧ ∀ 𝑥 ∃* 𝑦 𝜑 ) ↔ ( ∃ 𝑥 ∃ 𝑦 𝜑 ∧ ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) ) |