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

Metamath Proof Explorer

Theorem 2eu5

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 ⊢ ∃! x ∃! y φ ∧ ∀ x ∃* y φ ↔ ∃ x ∃ y φ ∧ ∃ z ∃ w ∀ x ∀ y φ → x = z ∧ y = w

Proof

Step Hyp Ref Expression
1 2eu1v ⊢ ∀ x ∃* y φ → ∃! x ∃! y φ ↔ ∃! x ∃ y φ ∧ ∃! y ∃ x φ
2 1 pm5.32ri ⊢ ∃! x ∃! y φ ∧ ∀ x ∃* y φ ↔ ∃! x ∃ y φ ∧ ∃! y ∃ x φ ∧ ∀ x ∃* y φ
3 eumo ⊢ ∃! y ∃ x φ → ∃* y ∃ x φ
4 2moexv ⊢ ∃* y ∃ x φ → ∀ x ∃* y φ
5 3 4 syl ⊢ ∃! y ∃ x φ → ∀ x ∃* y φ
6 5 adantl ⊢ ∃! x ∃ y φ ∧ ∃! y ∃ x φ → ∀ x ∃* y φ
7 6 pm4.71i ⊢ ∃! x ∃ y φ ∧ ∃! y ∃ x φ ↔ ∃! x ∃ y φ ∧ ∃! y ∃ x φ ∧ ∀ x ∃* y φ
8 2eu4 ⊢ ∃! x ∃ y φ ∧ ∃! y ∃ x φ ↔ ∃ x ∃ y φ ∧ ∃ z ∃ w ∀ x ∀ y φ → x = z ∧ y = w
9 2 7 8 3bitr2i ⊢ ∃! x ∃! y φ ∧ ∀ x ∃* y φ ↔ ∃ x ∃ y φ ∧ ∃ z ∃ w ∀ x ∀ y φ → x = z ∧ y = w