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

Metamath Proof Explorer

Theorem euotd

Description: Prove existential uniqueness for an ordered triple. (Contributed by Mario Carneiro, 20-May-2015)

Ref Expression
Hypotheses euotd.1 
|- ( ph -> A e. U )
euotd.2 
|- ( ph -> B e. V )
euotd.3 
|- ( ph -> C e. W )
euotd.4 
|- ( ph -> ( ps <-> ( a = A /\ b = B /\ c = C ) ) )
Assertion euotd 
|- ( ph -> E! x E. a E. b E. c ( x = <. a , b , c >. /\ ps ) )

Proof

Step Hyp Ref Expression
1 euotd.1 
 |-  ( ph -> A e. U )
2 euotd.2 
 |-  ( ph -> B e. V )
3 euotd.3 
 |-  ( ph -> C e. W )
4 euotd.4 
 |-  ( ph -> ( ps <-> ( a = A /\ b = B /\ c = C ) ) )
5 4 biimpa 
 |-  ( ( ph /\ ps ) -> ( a = A /\ b = B /\ c = C ) )
6 vex 
 |-  a e. _V
7 vex 
 |-  b e. _V
8 vex 
 |-  c e. _V
9 6 7 8 otth 
 |-  ( <. a , b , c >. = <. A , B , C >. <-> ( a = A /\ b = B /\ c = C ) )
10 5 9 sylibr 
 |-  ( ( ph /\ ps ) -> <. a , b , c >. = <. A , B , C >. )
11 10 eqeq2d 
 |-  ( ( ph /\ ps ) -> ( x = <. a , b , c >. <-> x = <. A , B , C >. ) )
12 11 biimpd 
 |-  ( ( ph /\ ps ) -> ( x = <. a , b , c >. -> x = <. A , B , C >. ) )
13 12 impancom 
 |-  ( ( ph /\ x = <. a , b , c >. ) -> ( ps -> x = <. A , B , C >. ) )
14 13 expimpd 
 |-  ( ph -> ( ( x = <. a , b , c >. /\ ps ) -> x = <. A , B , C >. ) )
15 14 exlimdv 
 |-  ( ph -> ( E. c ( x = <. a , b , c >. /\ ps ) -> x = <. A , B , C >. ) )
16 15 exlimdvv 
 |-  ( ph -> ( E. a E. b E. c ( x = <. a , b , c >. /\ ps ) -> x = <. A , B , C >. ) )
17 tru 
 |-  T.
18 2 adantr 
 |-  ( ( ph /\ a = A ) -> B e. V )
19 3 ad2antrr 
 |-  ( ( ( ph /\ a = A ) /\ b = B ) -> C e. W )
20 simpr 
 |-  ( ( ph /\ ( a = A /\ b = B /\ c = C ) ) -> ( a = A /\ b = B /\ c = C ) )
21 20 9 sylibr 
 |-  ( ( ph /\ ( a = A /\ b = B /\ c = C ) ) -> <. a , b , c >. = <. A , B , C >. )
22 21 eqcomd 
 |-  ( ( ph /\ ( a = A /\ b = B /\ c = C ) ) -> <. A , B , C >. = <. a , b , c >. )
23 4 biimpar 
 |-  ( ( ph /\ ( a = A /\ b = B /\ c = C ) ) -> ps )
24 22 23 jca 
 |-  ( ( ph /\ ( a = A /\ b = B /\ c = C ) ) -> ( <. A , B , C >. = <. a , b , c >. /\ ps ) )
25 trud 
 |-  ( ( ph /\ ( a = A /\ b = B /\ c = C ) ) -> T. )
26 24 25 2thd 
 |-  ( ( ph /\ ( a = A /\ b = B /\ c = C ) ) -> ( ( <. A , B , C >. = <. a , b , c >. /\ ps ) <-> T. ) )
27 26 3anassrs 
 |-  ( ( ( ( ph /\ a = A ) /\ b = B ) /\ c = C ) -> ( ( <. A , B , C >. = <. a , b , c >. /\ ps ) <-> T. ) )
28 19 27 sbcied 
 |-  ( ( ( ph /\ a = A ) /\ b = B ) -> ( [. C / c ]. ( <. A , B , C >. = <. a , b , c >. /\ ps ) <-> T. ) )
29 18 28 sbcied 
 |-  ( ( ph /\ a = A ) -> ( [. B / b ]. [. C / c ]. ( <. A , B , C >. = <. a , b , c >. /\ ps ) <-> T. ) )
30 1 29 sbcied 
 |-  ( ph -> ( [. A / a ]. [. B / b ]. [. C / c ]. ( <. A , B , C >. = <. a , b , c >. /\ ps ) <-> T. ) )
31 17 30 mpbiri 
 |-  ( ph -> [. A / a ]. [. B / b ]. [. C / c ]. ( <. A , B , C >. = <. a , b , c >. /\ ps ) )
32 31 spesbcd 
 |-  ( ph -> E. a [. B / b ]. [. C / c ]. ( <. A , B , C >. = <. a , b , c >. /\ ps ) )
33 nfcv 
 |-  F/_ b B
34 nfsbc1v 
 |-  F/ b [. B / b ]. [. C / c ]. ( <. A , B , C >. = <. a , b , c >. /\ ps )
35 34 nfex 
 |-  F/ b E. a [. B / b ]. [. C / c ]. ( <. A , B , C >. = <. a , b , c >. /\ ps )
36 sbceq1a 
 |-  ( b = B -> ( [. C / c ]. ( <. A , B , C >. = <. a , b , c >. /\ ps ) <-> [. B / b ]. [. C / c ]. ( <. A , B , C >. = <. a , b , c >. /\ ps ) ) )
37 36 exbidv 
 |-  ( b = B -> ( E. a [. C / c ]. ( <. A , B , C >. = <. a , b , c >. /\ ps ) <-> E. a [. B / b ]. [. C / c ]. ( <. A , B , C >. = <. a , b , c >. /\ ps ) ) )
38 33 35 37 spcegf 
 |-  ( B e. V -> ( E. a [. B / b ]. [. C / c ]. ( <. A , B , C >. = <. a , b , c >. /\ ps ) -> E. b E. a [. C / c ]. ( <. A , B , C >. = <. a , b , c >. /\ ps ) ) )
39 2 32 38 sylc 
 |-  ( ph -> E. b E. a [. C / c ]. ( <. A , B , C >. = <. a , b , c >. /\ ps ) )
40 nfcv 
 |-  F/_ c C
41 nfsbc1v 
 |-  F/ c [. C / c ]. ( <. A , B , C >. = <. a , b , c >. /\ ps )
42 41 nfex 
 |-  F/ c E. a [. C / c ]. ( <. A , B , C >. = <. a , b , c >. /\ ps )
43 42 nfex 
 |-  F/ c E. b E. a [. C / c ]. ( <. A , B , C >. = <. a , b , c >. /\ ps )
44 sbceq1a 
 |-  ( c = C -> ( ( <. A , B , C >. = <. a , b , c >. /\ ps ) <-> [. C / c ]. ( <. A , B , C >. = <. a , b , c >. /\ ps ) ) )
45 44 2exbidv 
 |-  ( c = C -> ( E. b E. a ( <. A , B , C >. = <. a , b , c >. /\ ps ) <-> E. b E. a [. C / c ]. ( <. A , B , C >. = <. a , b , c >. /\ ps ) ) )
46 40 43 45 spcegf 
 |-  ( C e. W -> ( E. b E. a [. C / c ]. ( <. A , B , C >. = <. a , b , c >. /\ ps ) -> E. c E. b E. a ( <. A , B , C >. = <. a , b , c >. /\ ps ) ) )
47 3 39 46 sylc 
 |-  ( ph -> E. c E. b E. a ( <. A , B , C >. = <. a , b , c >. /\ ps ) )
48 excom13 
 |-  ( E. c E. b E. a ( <. A , B , C >. = <. a , b , c >. /\ ps ) <-> E. a E. b E. c ( <. A , B , C >. = <. a , b , c >. /\ ps ) )
49 47 48 sylib 
 |-  ( ph -> E. a E. b E. c ( <. A , B , C >. = <. a , b , c >. /\ ps ) )
50 eqeq1 
 |-  ( x = <. A , B , C >. -> ( x = <. a , b , c >. <-> <. A , B , C >. = <. a , b , c >. ) )
51 50 anbi1d 
 |-  ( x = <. A , B , C >. -> ( ( x = <. a , b , c >. /\ ps ) <-> ( <. A , B , C >. = <. a , b , c >. /\ ps ) ) )
52 51 3exbidv 
 |-  ( x = <. A , B , C >. -> ( E. a E. b E. c ( x = <. a , b , c >. /\ ps ) <-> E. a E. b E. c ( <. A , B , C >. = <. a , b , c >. /\ ps ) ) )
53 49 52 syl5ibrcom 
 |-  ( ph -> ( x = <. A , B , C >. -> E. a E. b E. c ( x = <. a , b , c >. /\ ps ) ) )
54 16 53 impbid 
 |-  ( ph -> ( E. a E. b E. c ( x = <. a , b , c >. /\ ps ) <-> x = <. A , B , C >. ) )
55 54 alrimiv 
 |-  ( ph -> A. x ( E. a E. b E. c ( x = <. a , b , c >. /\ ps ) <-> x = <. A , B , C >. ) )
56 otex 
 |-  <. A , B , C >. e. _V
57 eqeq2 
 |-  ( y = <. A , B , C >. -> ( x = y <-> x = <. A , B , C >. ) )
58 57 bibi2d 
 |-  ( y = <. A , B , C >. -> ( ( E. a E. b E. c ( x = <. a , b , c >. /\ ps ) <-> x = y ) <-> ( E. a E. b E. c ( x = <. a , b , c >. /\ ps ) <-> x = <. A , B , C >. ) ) )
59 58 albidv 
 |-  ( y = <. A , B , C >. -> ( A. x ( E. a E. b E. c ( x = <. a , b , c >. /\ ps ) <-> x = y ) <-> A. x ( E. a E. b E. c ( x = <. a , b , c >. /\ ps ) <-> x = <. A , B , C >. ) ) )
60 56 59 spcev 
 |-  ( A. x ( E. a E. b E. c ( x = <. a , b , c >. /\ ps ) <-> x = <. A , B , C >. ) -> E. y A. x ( E. a E. b E. c ( x = <. a , b , c >. /\ ps ) <-> x = y ) )
61 55 60 syl 
 |-  ( ph -> E. y A. x ( E. a E. b E. c ( x = <. a , b , c >. /\ ps ) <-> x = y ) )
62 eu6 
 |-  ( E! x E. a E. b E. c ( x = <. a , b , c >. /\ ps ) <-> E. y A. x ( E. a E. b E. c ( x = <. a , b , c >. /\ ps ) <-> x = y ) )
63 61 62 sylibr 
 |-  ( ph -> E! x E. a E. b E. c ( x = <. a , b , c >. /\ ps ) )