Metamath Proof Explorer

Theorem 2eu6

Description: Two equivalent expressions for double existential uniqueness. (Contributed by NM, 2-Feb-2005) (Revised by Mario Carneiro, 17-Oct-2016) (Proof shortened by Wolf Lammen, 2-Oct-2019)

Ref Expression
Assertion 2eu6 ( ( ∃! 𝑥 ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃ 𝑥 𝜑 ) ↔ ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∀ 𝑦 ( 𝜑 ↔ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) )

Proof

Step Hyp Ref Expression
1 2eu4 ⊢ ( ( ∃! 𝑥 ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃ 𝑥 𝜑 ) ↔ ( ∃ 𝑥 ∃ 𝑦 𝜑 ∧ ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) )
2 nfia1 ⊢ Ⅎ 𝑥 ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) → ∀ 𝑥 ∀ 𝑦 ( 𝜑 ↔ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) )
3 nfa1 ⊢ Ⅎ 𝑦 ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) )
4 nfv ⊢ Ⅎ 𝑦 𝑥 = 𝑧
5 simpl ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → 𝑥 = 𝑧 )
6 5 imim2i ⊢ ( ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) → ( 𝜑 → 𝑥 = 𝑧 ) )
7 6 sps ⊢ ( ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) → ( 𝜑 → 𝑥 = 𝑧 ) )
8 3 4 7 exlimd ⊢ ( ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) → ( ∃ 𝑦 𝜑 → 𝑥 = 𝑧 ) )
9 ax12v ⊢ ( 𝑥 = 𝑧 → ( ∃ 𝑦 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑧 → ∃ 𝑦 𝜑 ) ) )
10 8 9 syli ⊢ ( ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) → ( ∃ 𝑦 𝜑 → ∀ 𝑥 ( 𝑥 = 𝑧 → ∃ 𝑦 𝜑 ) ) )
11 10 com12 ⊢ ( ∃ 𝑦 𝜑 → ( ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) → ∀ 𝑥 ( 𝑥 = 𝑧 → ∃ 𝑦 𝜑 ) ) )
12 11 spsd ⊢ ( ∃ 𝑦 𝜑 → ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) → ∀ 𝑥 ( 𝑥 = 𝑧 → ∃ 𝑦 𝜑 ) ) )
13 nfs1v ⊢ Ⅎ 𝑦 [ 𝑤 / 𝑦 ] 𝜑
14 simpr ⊢ ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → 𝑦 = 𝑤 )
15 14 imim2i ⊢ ( ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) → ( 𝜑 → 𝑦 = 𝑤 ) )
16 sbequ1 ⊢ ( 𝑦 = 𝑤 → ( 𝜑 → [ 𝑤 / 𝑦 ] 𝜑 ) )
17 15 16 syli ⊢ ( ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) → ( 𝜑 → [ 𝑤 / 𝑦 ] 𝜑 ) )
18 17 sps ⊢ ( ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) → ( 𝜑 → [ 𝑤 / 𝑦 ] 𝜑 ) )
19 3 13 18 exlimd ⊢ ( ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) → ( ∃ 𝑦 𝜑 → [ 𝑤 / 𝑦 ] 𝜑 ) )
20 19 imim2d ⊢ ( ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) → ( ( 𝑥 = 𝑧 → ∃ 𝑦 𝜑 ) → ( 𝑥 = 𝑧 → [ 𝑤 / 𝑦 ] 𝜑 ) ) )
21 20 al2imi ⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) → ( ∀ 𝑥 ( 𝑥 = 𝑧 → ∃ 𝑦 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑧 → [ 𝑤 / 𝑦 ] 𝜑 ) ) )
22 sb6 ⊢ ( [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ ∀ 𝑥 ( 𝑥 = 𝑧 → [ 𝑤 / 𝑦 ] 𝜑 ) )
23 2sb6 ⊢ ( [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → 𝜑 ) )
24 22 23 bitr3i ⊢ ( ∀ 𝑥 ( 𝑥 = 𝑧 → [ 𝑤 / 𝑦 ] 𝜑 ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → 𝜑 ) )
25 21 24 syl6ib ⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) → ( ∀ 𝑥 ( 𝑥 = 𝑧 → ∃ 𝑦 𝜑 ) → ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → 𝜑 ) ) )
26 12 25 sylcom ⊢ ( ∃ 𝑦 𝜑 → ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) → ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → 𝜑 ) ) )
27 26 ancld ⊢ ( ∃ 𝑦 𝜑 → ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) → ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ∧ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → 𝜑 ) ) ) )
28 2albiim ⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 ↔ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ↔ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ∧ ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → 𝜑 ) ) )
29 27 28 syl6ibr ⊢ ( ∃ 𝑦 𝜑 → ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) → ∀ 𝑥 ∀ 𝑦 ( 𝜑 ↔ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) )
30 2 29 exlimi ⊢ ( ∃ 𝑥 ∃ 𝑦 𝜑 → ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) → ∀ 𝑥 ∀ 𝑦 ( 𝜑 ↔ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) )
31 30 2eximdv ⊢ ( ∃ 𝑥 ∃ 𝑦 𝜑 → ( ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) → ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∀ 𝑦 ( 𝜑 ↔ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) )
32 31 imp ⊢ ( ( ∃ 𝑥 ∃ 𝑦 𝜑 ∧ ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) → ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∀ 𝑦 ( 𝜑 ↔ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) )
33 biimpr ⊢ ( ( 𝜑 ↔ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) → ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → 𝜑 ) )
34 33 2alimi ⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 ↔ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) → ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → 𝜑 ) )
35 34 2eximi ⊢ ( ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∀ 𝑦 ( 𝜑 ↔ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) → ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → 𝜑 ) )
36 2exsb ⊢ ( ∃ 𝑥 ∃ 𝑦 𝜑 ↔ ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∀ 𝑦 ( ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) → 𝜑 ) )
37 35 36 sylibr ⊢ ( ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∀ 𝑦 ( 𝜑 ↔ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) → ∃ 𝑥 ∃ 𝑦 𝜑 )
38 biimp ⊢ ( ( 𝜑 ↔ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) → ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) )
39 38 2alimi ⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝜑 ↔ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) → ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) )
40 39 2eximi ⊢ ( ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∀ 𝑦 ( 𝜑 ↔ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) → ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) )
41 37 40 jca ⊢ ( ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∀ 𝑦 ( 𝜑 ↔ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) → ( ∃ 𝑥 ∃ 𝑦 𝜑 ∧ ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) )
42 32 41 impbii ⊢ ( ( ∃ 𝑥 ∃ 𝑦 𝜑 ∧ ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) ↔ ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∀ 𝑦 ( 𝜑 ↔ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) )
43 1 42 bitri ⊢ ( ( ∃! 𝑥 ∃ 𝑦 𝜑 ∧ ∃! 𝑦 ∃ 𝑥 𝜑 ) ↔ ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∀ 𝑦 ( 𝜑 ↔ ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) )