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 9 bilanri 
 |-  ( ( ph /\ ( a = A /\ b = B /\ c = C ) ) -> <. a , b , c >. = <. A , B , C >. )
21 20 eqcomd 
 |-  ( ( ph /\ ( a = A /\ b = B /\ c = C ) ) -> <. A , B , C >. = <. a , b , c >. )
22 4 biimpar 
 |-  ( ( ph /\ ( a = A /\ b = B /\ c = C ) ) -> ps )
23 21 22 jca 
 |-  ( ( ph /\ ( a = A /\ b = B /\ c = C ) ) -> ( <. A , B , C >. = <. a , b , c >. /\ ps ) )
24 trud 
 |-  ( ( ph /\ ( a = A /\ b = B /\ c = C ) ) -> T. )
25 23 24 2thd 
 |-  ( ( ph /\ ( a = A /\ b = B /\ c = C ) ) -> ( ( <. A , B , C >. = <. a , b , c >. /\ ps ) <-> T. ) )
26 25 3anassrs 
 |-  ( ( ( ( ph /\ a = A ) /\ b = B ) /\ c = C ) -> ( ( <. A , B , C >. = <. a , b , c >. /\ ps ) <-> T. ) )
27 19 26 sbcied 
 |-  ( ( ( ph /\ a = A ) /\ b = B ) -> ( [. C / c ]. ( <. A , B , C >. = <. a , b , c >. /\ ps ) <-> T. ) )
28 18 27 sbcied 
 |-  ( ( ph /\ a = A ) -> ( [. B / b ]. [. C / c ]. ( <. A , B , C >. = <. a , b , c >. /\ ps ) <-> T. ) )
29 1 28 sbcied 
 |-  ( ph -> ( [. A / a ]. [. B / b ]. [. C / c ]. ( <. A , B , C >. = <. a , b , c >. /\ ps ) <-> T. ) )
30 17 29 mpbiri 
 |-  ( ph -> [. A / a ]. [. B / b ]. [. C / c ]. ( <. A , B , C >. = <. a , b , c >. /\ ps ) )
31 30 spesbcd 
 |-  ( ph -> E. a [. B / b ]. [. C / c ]. ( <. A , B , C >. = <. a , b , c >. /\ ps ) )
32 nfcv 
 |-  F/_ b B
33 nfsbc1v 
 |-  F/ b [. B / b ]. [. C / c ]. ( <. A , B , C >. = <. a , b , c >. /\ ps )
34 33 nfex 
 |-  F/ b E. a [. B / b ]. [. C / c ]. ( <. A , B , C >. = <. a , b , c >. /\ ps )
35 sbceq1a 
 |-  ( b = B -> ( [. C / c ]. ( <. A , B , C >. = <. a , b , c >. /\ ps ) <-> [. B / b ]. [. C / c ]. ( <. A , B , C >. = <. a , b , c >. /\ ps ) ) )
36 35 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 ) ) )
37 32 34 36 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 ) ) )
38 2 31 37 sylc 
 |-  ( ph -> E. b E. a [. C / c ]. ( <. A , B , C >. = <. a , b , c >. /\ ps ) )
39 nfcv 
 |-  F/_ c C
40 nfsbc1v 
 |-  F/ c [. C / c ]. ( <. A , B , C >. = <. a , b , c >. /\ ps )
41 40 nfex 
 |-  F/ c E. a [. C / c ]. ( <. A , B , C >. = <. a , b , c >. /\ ps )
42 41 nfex 
 |-  F/ c E. b E. a [. C / c ]. ( <. A , B , C >. = <. a , b , c >. /\ ps )
43 sbceq1a 
 |-  ( c = C -> ( ( <. A , B , C >. = <. a , b , c >. /\ ps ) <-> [. C / c ]. ( <. A , B , C >. = <. a , b , c >. /\ ps ) ) )
44 43 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 ) ) )
45 39 42 44 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 ) ) )
46 3 38 45 sylc 
 |-  ( ph -> E. c E. b E. a ( <. A , B , C >. = <. a , b , c >. /\ ps ) )
47 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 ) )
48 46 47 sylib 
 |-  ( ph -> E. a E. b E. c ( <. A , B , C >. = <. a , b , c >. /\ ps ) )
49 eqeq1 
 |-  ( x = <. A , B , C >. -> ( x = <. a , b , c >. <-> <. A , B , C >. = <. a , b , c >. ) )
50 49 anbi1d 
 |-  ( x = <. A , B , C >. -> ( ( x = <. a , b , c >. /\ ps ) <-> ( <. A , B , C >. = <. a , b , c >. /\ ps ) ) )
51 50 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 ) ) )
52 48 51 syl5ibrcom 
 |-  ( ph -> ( x = <. A , B , C >. -> E. a E. b E. c ( x = <. a , b , c >. /\ ps ) ) )
53 16 52 impbid 
 |-  ( ph -> ( E. a E. b E. c ( x = <. a , b , c >. /\ ps ) <-> x = <. A , B , C >. ) )
54 53 alrimiv 
 |-  ( ph -> A. x ( E. a E. b E. c ( x = <. a , b , c >. /\ ps ) <-> x = <. A , B , C >. ) )
55 otex 
 |-  <. A , B , C >. e. _V
56 eqeq2 
 |-  ( y = <. A , B , C >. -> ( x = y <-> x = <. A , B , C >. ) )
57 56 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 >. ) ) )
58 57 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 >. ) ) )
59 55 58 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 ) )
60 54 59 syl 
 |-  ( ph -> E. y A. x ( E. a E. b E. c ( x = <. a , b , c >. /\ ps ) <-> x = y ) )
61 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 ) )
62 60 61 sylibr 
 |-  ( ph -> E! x E. a E. b E. c ( x = <. a , b , c >. /\ ps ) )