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

Metamath Proof Explorer

Theorem 2mo

Description: Two ways of expressing "there exists at most one ordered pair <. x , y >. such that ph ( x , y ) holds. See also 2mo2 . (Contributed by NM, 2-Feb-2005) (Revised by Mario Carneiro, 17-Oct-2016) (Proof shortened by Wolf Lammen, 2-Nov-2019)

Ref Expression
Assertion 2mo ( ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ∀ 𝑤 ( ( 𝜑 ∧ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ) → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) )

Proof

Step Hyp Ref Expression
1 2mo2 ⊢ ( ( ∃* 𝑥 ∃ 𝑦 𝜑 ∧ ∃* 𝑦 ∃ 𝑥 𝜑 ) ↔ ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) )
2 nfmo1 ⊢ Ⅎ 𝑥 ∃* 𝑥 ∃ 𝑦 𝜑
3 nfe1 ⊢ Ⅎ 𝑥 ∃ 𝑥 𝜑
4 3 nfmov ⊢ Ⅎ 𝑥 ∃* 𝑦 ∃ 𝑥 𝜑
5 2 4 nfan ⊢ Ⅎ 𝑥 ( ∃* 𝑥 ∃ 𝑦 𝜑 ∧ ∃* 𝑦 ∃ 𝑥 𝜑 )
6 nfe1 ⊢ Ⅎ 𝑦 ∃ 𝑦 𝜑
7 6 nfmov ⊢ Ⅎ 𝑦 ∃* 𝑥 ∃ 𝑦 𝜑
8 nfmo1 ⊢ Ⅎ 𝑦 ∃* 𝑦 ∃ 𝑥 𝜑
9 7 8 nfan ⊢ Ⅎ 𝑦 ( ∃* 𝑥 ∃ 𝑦 𝜑 ∧ ∃* 𝑦 ∃ 𝑥 𝜑 )
10 19.8a ⊢ ( 𝜑 → ∃ 𝑦 𝜑 )
11 spsbe ⊢ ( [ 𝑤 / 𝑦 ] 𝜑 → ∃ 𝑦 𝜑 )
12 11 sbimi ⊢ ( [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 → [ 𝑧 / 𝑥 ] ∃ 𝑦 𝜑 )
13 nfv ⊢ Ⅎ 𝑧 ∃ 𝑦 𝜑
14 13 mo3 ⊢ ( ∃* 𝑥 ∃ 𝑦 𝜑 ↔ ∀ 𝑥 ∀ 𝑧 ( ( ∃ 𝑦 𝜑 ∧ [ 𝑧 / 𝑥 ] ∃ 𝑦 𝜑 ) → 𝑥 = 𝑧 ) )
15 14 biimpi ⊢ ( ∃* 𝑥 ∃ 𝑦 𝜑 → ∀ 𝑥 ∀ 𝑧 ( ( ∃ 𝑦 𝜑 ∧ [ 𝑧 / 𝑥 ] ∃ 𝑦 𝜑 ) → 𝑥 = 𝑧 ) )
16 15 19.21bbi ⊢ ( ∃* 𝑥 ∃ 𝑦 𝜑 → ( ( ∃ 𝑦 𝜑 ∧ [ 𝑧 / 𝑥 ] ∃ 𝑦 𝜑 ) → 𝑥 = 𝑧 ) )
17 10 12 16 syl2ani ⊢ ( ∃* 𝑥 ∃ 𝑦 𝜑 → ( ( 𝜑 ∧ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ) → 𝑥 = 𝑧 ) )
18 19.8a ⊢ ( 𝜑 → ∃ 𝑥 𝜑 )
19 sbcom2 ⊢ ( [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ [ 𝑤 / 𝑦 ] [ 𝑧 / 𝑥 ] 𝜑 )
20 spsbe ⊢ ( [ 𝑧 / 𝑥 ] 𝜑 → ∃ 𝑥 𝜑 )
21 20 sbimi ⊢ ( [ 𝑤 / 𝑦 ] [ 𝑧 / 𝑥 ] 𝜑 → [ 𝑤 / 𝑦 ] ∃ 𝑥 𝜑 )
22 19 21 sylbi ⊢ ( [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 → [ 𝑤 / 𝑦 ] ∃ 𝑥 𝜑 )
23 nfv ⊢ Ⅎ 𝑤 ∃ 𝑥 𝜑
24 23 mo3 ⊢ ( ∃* 𝑦 ∃ 𝑥 𝜑 ↔ ∀ 𝑦 ∀ 𝑤 ( ( ∃ 𝑥 𝜑 ∧ [ 𝑤 / 𝑦 ] ∃ 𝑥 𝜑 ) → 𝑦 = 𝑤 ) )
25 24 biimpi ⊢ ( ∃* 𝑦 ∃ 𝑥 𝜑 → ∀ 𝑦 ∀ 𝑤 ( ( ∃ 𝑥 𝜑 ∧ [ 𝑤 / 𝑦 ] ∃ 𝑥 𝜑 ) → 𝑦 = 𝑤 ) )
26 25 19.21bbi ⊢ ( ∃* 𝑦 ∃ 𝑥 𝜑 → ( ( ∃ 𝑥 𝜑 ∧ [ 𝑤 / 𝑦 ] ∃ 𝑥 𝜑 ) → 𝑦 = 𝑤 ) )
27 18 22 26 syl2ani ⊢ ( ∃* 𝑦 ∃ 𝑥 𝜑 → ( ( 𝜑 ∧ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ) → 𝑦 = 𝑤 ) )
28 17 27 anim12ii ⊢ ( ( ∃* 𝑥 ∃ 𝑦 𝜑 ∧ ∃* 𝑦 ∃ 𝑥 𝜑 ) → ( ( 𝜑 ∧ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ) → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) )
29 9 28 alrimi ⊢ ( ( ∃* 𝑥 ∃ 𝑦 𝜑 ∧ ∃* 𝑦 ∃ 𝑥 𝜑 ) → ∀ 𝑦 ( ( 𝜑 ∧ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ) → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) )
30 5 29 alrimi ⊢ ( ( ∃* 𝑥 ∃ 𝑦 𝜑 ∧ ∃* 𝑦 ∃ 𝑥 𝜑 ) → ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ) → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) )
31 30 alrimivv ⊢ ( ( ∃* 𝑥 ∃ 𝑦 𝜑 ∧ ∃* 𝑦 ∃ 𝑥 𝜑 ) → ∀ 𝑧 ∀ 𝑤 ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ) → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) )
32 1 31 sylbir ⊢ ( ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) → ∀ 𝑧 ∀ 𝑤 ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ) → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) )
33 nfs1v ⊢ Ⅎ 𝑥 [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑
34 nfs1v ⊢ Ⅎ 𝑦 [ 𝑤 / 𝑦 ] 𝜑
35 34 nfsbv ⊢ Ⅎ 𝑦 [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑
36 pm3.21 ⊢ ( [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 → ( 𝜑 → ( 𝜑 ∧ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ) ) )
37 36 imim1d ⊢ ( [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 → ( ( ( 𝜑 ∧ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ) → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) → ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) )
38 35 37 alimd ⊢ ( [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 → ( ∀ 𝑦 ( ( 𝜑 ∧ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ) → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) → ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) )
39 33 38 alimd ⊢ ( [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 → ( ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ) → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) → ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) )
40 39 com12 ⊢ ( ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ) → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) → ( [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 → ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) )
41 40 aleximi ⊢ ( ∀ 𝑤 ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ) → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) → ( ∃ 𝑤 [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 → ∃ 𝑤 ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) )
42 41 aleximi ⊢ ( ∀ 𝑧 ∀ 𝑤 ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ) → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) → ( ∃ 𝑧 ∃ 𝑤 [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 → ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ) )
43 2nexaln ⊢ ( ¬ ∃ 𝑥 ∃ 𝑦 𝜑 ↔ ∀ 𝑥 ∀ 𝑦 ¬ 𝜑 )
44 nfv ⊢ Ⅎ 𝑤 𝜑
45 nfv ⊢ Ⅎ 𝑧 𝜑
46 44 45 2sb8ef ⊢ ( ∃ 𝑥 ∃ 𝑦 𝜑 ↔ ∃ 𝑧 ∃ 𝑤 [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 )
47 43 46 xchnxbi ⊢ ( ¬ ∃ 𝑧 ∃ 𝑤 [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ ∀ 𝑥 ∀ 𝑦 ¬ 𝜑 )
48 pm2.21 ⊢ ( ¬ 𝜑 → ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) )
49 48 2alimi ⊢ ( ∀ 𝑥 ∀ 𝑦 ¬ 𝜑 → ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) )
50 49 2eximi ⊢ ( ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∀ 𝑦 ¬ 𝜑 → ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) )
51 50 19.23bi ⊢ ( ∃ 𝑤 ∀ 𝑥 ∀ 𝑦 ¬ 𝜑 → ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) )
52 51 19.23bi ⊢ ( ∀ 𝑥 ∀ 𝑦 ¬ 𝜑 → ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) )
53 47 52 sylbi ⊢ ( ¬ ∃ 𝑧 ∃ 𝑤 [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 → ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) )
54 42 53 pm2.61d1 ⊢ ( ∀ 𝑧 ∀ 𝑤 ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ) → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) → ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) )
55 32 54 impbii ⊢ ( ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ↔ ∀ 𝑧 ∀ 𝑤 ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ) → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) )
56 alrot4 ⊢ ( ∀ 𝑧 ∀ 𝑤 ∀ 𝑥 ∀ 𝑦 ( ( 𝜑 ∧ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ) → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ∀ 𝑤 ( ( 𝜑 ∧ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ) → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) )
57 55 56 bitri ⊢ ( ∃ 𝑧 ∃ 𝑤 ∀ 𝑥 ∀ 𝑦 ( 𝜑 → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) ↔ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ∀ 𝑤 ( ( 𝜑 ∧ [ 𝑧 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ) → ( 𝑥 = 𝑧 ∧ 𝑦 = 𝑤 ) ) )