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 
|- ( E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) <-> A. x A. y A. z A. w ( ( ph /\ [ z / x ] [ w / y ] ph ) -> ( x = z /\ y = w ) ) )

Proof

Step Hyp Ref Expression
1 2mo2 
 |-  ( ( E* x E. y ph /\ E* y E. x ph ) <-> E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) )
2 nfmo1 
 |-  F/ x E* x E. y ph
3 nfe1 
 |-  F/ x E. x ph
4 3 nfmov 
 |-  F/ x E* y E. x ph
5 2 4 nfan 
 |-  F/ x ( E* x E. y ph /\ E* y E. x ph )
6 nfe1 
 |-  F/ y E. y ph
7 6 nfmov 
 |-  F/ y E* x E. y ph
8 nfmo1 
 |-  F/ y E* y E. x ph
9 7 8 nfan 
 |-  F/ y ( E* x E. y ph /\ E* y E. x ph )
10 19.8a 
 |-  ( ph -> E. y ph )
11 spsbe 
 |-  ( [ w / y ] ph -> E. y ph )
12 11 sbimi 
 |-  ( [ z / x ] [ w / y ] ph -> [ z / x ] E. y ph )
13 nfv 
 |-  F/ z E. y ph
14 13 mo3 
 |-  ( E* x E. y ph <-> A. x A. z ( ( E. y ph /\ [ z / x ] E. y ph ) -> x = z ) )
15 14 biimpi 
 |-  ( E* x E. y ph -> A. x A. z ( ( E. y ph /\ [ z / x ] E. y ph ) -> x = z ) )
16 15 19.21bbi 
 |-  ( E* x E. y ph -> ( ( E. y ph /\ [ z / x ] E. y ph ) -> x = z ) )
17 10 12 16 syl2ani 
 |-  ( E* x E. y ph -> ( ( ph /\ [ z / x ] [ w / y ] ph ) -> x = z ) )
18 19.8a 
 |-  ( ph -> E. x ph )
19 sbcom2 
 |-  ( [ z / x ] [ w / y ] ph <-> [ w / y ] [ z / x ] ph )
20 spsbe 
 |-  ( [ z / x ] ph -> E. x ph )
21 20 sbimi 
 |-  ( [ w / y ] [ z / x ] ph -> [ w / y ] E. x ph )
22 19 21 sylbi 
 |-  ( [ z / x ] [ w / y ] ph -> [ w / y ] E. x ph )
23 nfv 
 |-  F/ w E. x ph
24 23 mo3 
 |-  ( E* y E. x ph <-> A. y A. w ( ( E. x ph /\ [ w / y ] E. x ph ) -> y = w ) )
25 24 biimpi 
 |-  ( E* y E. x ph -> A. y A. w ( ( E. x ph /\ [ w / y ] E. x ph ) -> y = w ) )
26 25 19.21bbi 
 |-  ( E* y E. x ph -> ( ( E. x ph /\ [ w / y ] E. x ph ) -> y = w ) )
27 18 22 26 syl2ani 
 |-  ( E* y E. x ph -> ( ( ph /\ [ z / x ] [ w / y ] ph ) -> y = w ) )
28 17 27 anim12ii 
 |-  ( ( E* x E. y ph /\ E* y E. x ph ) -> ( ( ph /\ [ z / x ] [ w / y ] ph ) -> ( x = z /\ y = w ) ) )
29 9 28 alrimi 
 |-  ( ( E* x E. y ph /\ E* y E. x ph ) -> A. y ( ( ph /\ [ z / x ] [ w / y ] ph ) -> ( x = z /\ y = w ) ) )
30 5 29 alrimi 
 |-  ( ( E* x E. y ph /\ E* y E. x ph ) -> A. x A. y ( ( ph /\ [ z / x ] [ w / y ] ph ) -> ( x = z /\ y = w ) ) )
31 30 alrimivv 
 |-  ( ( E* x E. y ph /\ E* y E. x ph ) -> A. z A. w A. x A. y ( ( ph /\ [ z / x ] [ w / y ] ph ) -> ( x = z /\ y = w ) ) )
32 1 31 sylbir 
 |-  ( E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) -> A. z A. w A. x A. y ( ( ph /\ [ z / x ] [ w / y ] ph ) -> ( x = z /\ y = w ) ) )
33 nfs1v 
 |-  F/ x [ z / x ] [ w / y ] ph
34 nfs1v 
 |-  F/ y [ w / y ] ph
35 34 nfsbv 
 |-  F/ y [ z / x ] [ w / y ] ph
36 pm3.21 
 |-  ( [ z / x ] [ w / y ] ph -> ( ph -> ( ph /\ [ z / x ] [ w / y ] ph ) ) )
37 36 imim1d 
 |-  ( [ z / x ] [ w / y ] ph -> ( ( ( ph /\ [ z / x ] [ w / y ] ph ) -> ( x = z /\ y = w ) ) -> ( ph -> ( x = z /\ y = w ) ) ) )
38 35 37 alimd 
 |-  ( [ z / x ] [ w / y ] ph -> ( A. y ( ( ph /\ [ z / x ] [ w / y ] ph ) -> ( x = z /\ y = w ) ) -> A. y ( ph -> ( x = z /\ y = w ) ) ) )
39 33 38 alimd 
 |-  ( [ z / x ] [ w / y ] ph -> ( A. x A. y ( ( ph /\ [ z / x ] [ w / y ] ph ) -> ( x = z /\ y = w ) ) -> A. x A. y ( ph -> ( x = z /\ y = w ) ) ) )
40 39 com12 
 |-  ( A. x A. y ( ( ph /\ [ z / x ] [ w / y ] ph ) -> ( x = z /\ y = w ) ) -> ( [ z / x ] [ w / y ] ph -> A. x A. y ( ph -> ( x = z /\ y = w ) ) ) )
41 40 aleximi 
 |-  ( A. w A. x A. y ( ( ph /\ [ z / x ] [ w / y ] ph ) -> ( x = z /\ y = w ) ) -> ( E. w [ z / x ] [ w / y ] ph -> E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) ) )
42 41 aleximi 
 |-  ( A. z A. w A. x A. y ( ( ph /\ [ z / x ] [ w / y ] ph ) -> ( x = z /\ y = w ) ) -> ( E. z E. w [ z / x ] [ w / y ] ph -> E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) ) )
43 2nexaln 
 |-  ( -. E. x E. y ph <-> A. x A. y -. ph )
44 nfv 
 |-  F/ w ph
45 nfv 
 |-  F/ z ph
46 44 45 2sb8ev 
 |-  ( E. x E. y ph <-> E. z E. w [ z / x ] [ w / y ] ph )
47 43 46 xchnxbi 
 |-  ( -. E. z E. w [ z / x ] [ w / y ] ph <-> A. x A. y -. ph )
48 pm2.21 
 |-  ( -. ph -> ( ph -> ( x = z /\ y = w ) ) )
49 48 2alimi 
 |-  ( A. x A. y -. ph -> A. x A. y ( ph -> ( x = z /\ y = w ) ) )
50 49 2eximi 
 |-  ( E. z E. w A. x A. y -. ph -> E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) )
51 50 19.23bi 
 |-  ( E. w A. x A. y -. ph -> E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) )
52 51 19.23bi 
 |-  ( A. x A. y -. ph -> E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) )
53 47 52 sylbi 
 |-  ( -. E. z E. w [ z / x ] [ w / y ] ph -> E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) )
54 42 53 pm2.61d1 
 |-  ( A. z A. w A. x A. y ( ( ph /\ [ z / x ] [ w / y ] ph ) -> ( x = z /\ y = w ) ) -> E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) )
55 32 54 impbii 
 |-  ( E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) <-> A. z A. w A. x A. y ( ( ph /\ [ z / x ] [ w / y ] ph ) -> ( x = z /\ y = w ) ) )
56 alrot4 
 |-  ( A. z A. w A. x A. y ( ( ph /\ [ z / x ] [ w / y ] ph ) -> ( x = z /\ y = w ) ) <-> A. x A. y A. z A. w ( ( ph /\ [ z / x ] [ w / y ] ph ) -> ( x = z /\ y = w ) ) )
57 55 56 bitri 
 |-  ( E. z E. w A. x A. y ( ph -> ( x = z /\ y = w ) ) <-> A. x A. y A. z A. w ( ( ph /\ [ z / x ] [ w / y ] ph ) -> ( x = z /\ y = w ) ) )