Metamath Proof Explorer


Theorem reuop

Description: There is a unique ordered pair fulfilling a wff iff there are uniquely two sets fulfilling a corresponding wff. (Contributed by AV, 23-Jun-2023)

Ref Expression
Hypotheses reu3op.a
|- ( p = <. a , b >. -> ( ps <-> ch ) )
reuop.x
|- ( p = <. x , y >. -> ( ps <-> th ) )
Assertion reuop
|- ( E! p e. ( X X. Y ) ps <-> E. a e. X E. b e. Y ( ch /\ A. x e. X A. y e. Y ( th -> <. x , y >. = <. a , b >. ) ) )

Proof

Step Hyp Ref Expression
1 reu3op.a
 |-  ( p = <. a , b >. -> ( ps <-> ch ) )
2 reuop.x
 |-  ( p = <. x , y >. -> ( ps <-> th ) )
3 nfsbc1v
 |-  F/ p [. q / p ]. ps
4 nfsbc1v
 |-  F/ p [. w / p ]. ps
5 sbceq1a
 |-  ( p = w -> ( ps <-> [. w / p ]. ps ) )
6 dfsbcq
 |-  ( w = q -> ( [. w / p ]. ps <-> [. q / p ]. ps ) )
7 3 4 5 6 reu8nf
 |-  ( E! p e. ( X X. Y ) ps <-> E. p e. ( X X. Y ) ( ps /\ A. q e. ( X X. Y ) ( [. q / p ]. ps -> p = q ) ) )
8 elxp2
 |-  ( p e. ( X X. Y ) <-> E. a e. X E. b e. Y p = <. a , b >. )
9 1 biimpcd
 |-  ( ps -> ( p = <. a , b >. -> ch ) )
10 9 adantr
 |-  ( ( ps /\ A. q e. ( X X. Y ) ( [. q / p ]. ps -> p = q ) ) -> ( p = <. a , b >. -> ch ) )
11 10 adantr
 |-  ( ( ( ps /\ A. q e. ( X X. Y ) ( [. q / p ]. ps -> p = q ) ) /\ ( a e. X /\ b e. Y ) ) -> ( p = <. a , b >. -> ch ) )
12 11 imp
 |-  ( ( ( ( ps /\ A. q e. ( X X. Y ) ( [. q / p ]. ps -> p = q ) ) /\ ( a e. X /\ b e. Y ) ) /\ p = <. a , b >. ) -> ch )
13 opelxpi
 |-  ( ( x e. X /\ y e. Y ) -> <. x , y >. e. ( X X. Y ) )
14 dfsbcq
 |-  ( q = <. x , y >. -> ( [. q / p ]. ps <-> [. <. x , y >. / p ]. ps ) )
15 eqeq2
 |-  ( q = <. x , y >. -> ( p = q <-> p = <. x , y >. ) )
16 14 15 imbi12d
 |-  ( q = <. x , y >. -> ( ( [. q / p ]. ps -> p = q ) <-> ( [. <. x , y >. / p ]. ps -> p = <. x , y >. ) ) )
17 16 adantl
 |-  ( ( ( x e. X /\ y e. Y ) /\ q = <. x , y >. ) -> ( ( [. q / p ]. ps -> p = q ) <-> ( [. <. x , y >. / p ]. ps -> p = <. x , y >. ) ) )
18 13 17 rspcdv
 |-  ( ( x e. X /\ y e. Y ) -> ( A. q e. ( X X. Y ) ( [. q / p ]. ps -> p = q ) -> ( [. <. x , y >. / p ]. ps -> p = <. x , y >. ) ) )
19 18 adantr
 |-  ( ( ( x e. X /\ y e. Y ) /\ ps ) -> ( A. q e. ( X X. Y ) ( [. q / p ]. ps -> p = q ) -> ( [. <. x , y >. / p ]. ps -> p = <. x , y >. ) ) )
20 opex
 |-  <. x , y >. e. _V
21 20 2 sbcie
 |-  ( [. <. x , y >. / p ]. ps <-> th )
22 pm2.27
 |-  ( [. <. x , y >. / p ]. ps -> ( ( [. <. x , y >. / p ]. ps -> p = <. x , y >. ) -> p = <. x , y >. ) )
23 21 22 sylbir
 |-  ( th -> ( ( [. <. x , y >. / p ]. ps -> p = <. x , y >. ) -> p = <. x , y >. ) )
24 eqcom
 |-  ( <. x , y >. = p <-> p = <. x , y >. )
25 23 24 syl6ibr
 |-  ( th -> ( ( [. <. x , y >. / p ]. ps -> p = <. x , y >. ) -> <. x , y >. = p ) )
26 25 com12
 |-  ( ( [. <. x , y >. / p ]. ps -> p = <. x , y >. ) -> ( th -> <. x , y >. = p ) )
27 eqeq2
 |-  ( <. a , b >. = p -> ( <. x , y >. = <. a , b >. <-> <. x , y >. = p ) )
28 27 eqcoms
 |-  ( p = <. a , b >. -> ( <. x , y >. = <. a , b >. <-> <. x , y >. = p ) )
29 28 imbi2d
 |-  ( p = <. a , b >. -> ( ( th -> <. x , y >. = <. a , b >. ) <-> ( th -> <. x , y >. = p ) ) )
30 26 29 syl5ibrcom
 |-  ( ( [. <. x , y >. / p ]. ps -> p = <. x , y >. ) -> ( p = <. a , b >. -> ( th -> <. x , y >. = <. a , b >. ) ) )
31 30 a1d
 |-  ( ( [. <. x , y >. / p ]. ps -> p = <. x , y >. ) -> ( ( a e. X /\ b e. Y ) -> ( p = <. a , b >. -> ( th -> <. x , y >. = <. a , b >. ) ) ) )
32 19 31 syl6
 |-  ( ( ( x e. X /\ y e. Y ) /\ ps ) -> ( A. q e. ( X X. Y ) ( [. q / p ]. ps -> p = q ) -> ( ( a e. X /\ b e. Y ) -> ( p = <. a , b >. -> ( th -> <. x , y >. = <. a , b >. ) ) ) ) )
33 32 expimpd
 |-  ( ( x e. X /\ y e. Y ) -> ( ( ps /\ A. q e. ( X X. Y ) ( [. q / p ]. ps -> p = q ) ) -> ( ( a e. X /\ b e. Y ) -> ( p = <. a , b >. -> ( th -> <. x , y >. = <. a , b >. ) ) ) ) )
34 33 imp4c
 |-  ( ( x e. X /\ y e. Y ) -> ( ( ( ( ps /\ A. q e. ( X X. Y ) ( [. q / p ]. ps -> p = q ) ) /\ ( a e. X /\ b e. Y ) ) /\ p = <. a , b >. ) -> ( th -> <. x , y >. = <. a , b >. ) ) )
35 34 impcom
 |-  ( ( ( ( ( ps /\ A. q e. ( X X. Y ) ( [. q / p ]. ps -> p = q ) ) /\ ( a e. X /\ b e. Y ) ) /\ p = <. a , b >. ) /\ ( x e. X /\ y e. Y ) ) -> ( th -> <. x , y >. = <. a , b >. ) )
36 35 ralrimivva
 |-  ( ( ( ( ps /\ A. q e. ( X X. Y ) ( [. q / p ]. ps -> p = q ) ) /\ ( a e. X /\ b e. Y ) ) /\ p = <. a , b >. ) -> A. x e. X A. y e. Y ( th -> <. x , y >. = <. a , b >. ) )
37 12 36 jca
 |-  ( ( ( ( ps /\ A. q e. ( X X. Y ) ( [. q / p ]. ps -> p = q ) ) /\ ( a e. X /\ b e. Y ) ) /\ p = <. a , b >. ) -> ( ch /\ A. x e. X A. y e. Y ( th -> <. x , y >. = <. a , b >. ) ) )
38 37 ex
 |-  ( ( ( ps /\ A. q e. ( X X. Y ) ( [. q / p ]. ps -> p = q ) ) /\ ( a e. X /\ b e. Y ) ) -> ( p = <. a , b >. -> ( ch /\ A. x e. X A. y e. Y ( th -> <. x , y >. = <. a , b >. ) ) ) )
39 38 reximdvva
 |-  ( ( ps /\ A. q e. ( X X. Y ) ( [. q / p ]. ps -> p = q ) ) -> ( E. a e. X E. b e. Y p = <. a , b >. -> E. a e. X E. b e. Y ( ch /\ A. x e. X A. y e. Y ( th -> <. x , y >. = <. a , b >. ) ) ) )
40 39 com12
 |-  ( E. a e. X E. b e. Y p = <. a , b >. -> ( ( ps /\ A. q e. ( X X. Y ) ( [. q / p ]. ps -> p = q ) ) -> E. a e. X E. b e. Y ( ch /\ A. x e. X A. y e. Y ( th -> <. x , y >. = <. a , b >. ) ) ) )
41 8 40 sylbi
 |-  ( p e. ( X X. Y ) -> ( ( ps /\ A. q e. ( X X. Y ) ( [. q / p ]. ps -> p = q ) ) -> E. a e. X E. b e. Y ( ch /\ A. x e. X A. y e. Y ( th -> <. x , y >. = <. a , b >. ) ) ) )
42 41 rexlimiv
 |-  ( E. p e. ( X X. Y ) ( ps /\ A. q e. ( X X. Y ) ( [. q / p ]. ps -> p = q ) ) -> E. a e. X E. b e. Y ( ch /\ A. x e. X A. y e. Y ( th -> <. x , y >. = <. a , b >. ) ) )
43 opelxpi
 |-  ( ( a e. X /\ b e. Y ) -> <. a , b >. e. ( X X. Y ) )
44 43 adantr
 |-  ( ( ( a e. X /\ b e. Y ) /\ ( ch /\ A. x e. X A. y e. Y ( th -> <. x , y >. = <. a , b >. ) ) ) -> <. a , b >. e. ( X X. Y ) )
45 simprl
 |-  ( ( ( a e. X /\ b e. Y ) /\ ( ch /\ A. x e. X A. y e. Y ( th -> <. x , y >. = <. a , b >. ) ) ) -> ch )
46 nfsbc1v
 |-  F/ x [. c / x ]. th
47 nfv
 |-  F/ x <. c , y >. = <. a , b >.
48 46 47 nfim
 |-  F/ x ( [. c / x ]. th -> <. c , y >. = <. a , b >. )
49 nfsbc1v
 |-  F/ y [. d / y ]. [. c / x ]. th
50 nfv
 |-  F/ y <. c , d >. = <. a , b >.
51 49 50 nfim
 |-  F/ y ( [. d / y ]. [. c / x ]. th -> <. c , d >. = <. a , b >. )
52 sbceq1a
 |-  ( x = c -> ( th <-> [. c / x ]. th ) )
53 opeq1
 |-  ( x = c -> <. x , y >. = <. c , y >. )
54 53 eqeq1d
 |-  ( x = c -> ( <. x , y >. = <. a , b >. <-> <. c , y >. = <. a , b >. ) )
55 52 54 imbi12d
 |-  ( x = c -> ( ( th -> <. x , y >. = <. a , b >. ) <-> ( [. c / x ]. th -> <. c , y >. = <. a , b >. ) ) )
56 sbceq1a
 |-  ( y = d -> ( [. c / x ]. th <-> [. d / y ]. [. c / x ]. th ) )
57 opeq2
 |-  ( y = d -> <. c , y >. = <. c , d >. )
58 57 eqeq1d
 |-  ( y = d -> ( <. c , y >. = <. a , b >. <-> <. c , d >. = <. a , b >. ) )
59 56 58 imbi12d
 |-  ( y = d -> ( ( [. c / x ]. th -> <. c , y >. = <. a , b >. ) <-> ( [. d / y ]. [. c / x ]. th -> <. c , d >. = <. a , b >. ) ) )
60 48 51 55 59 rspc2
 |-  ( ( c e. X /\ d e. Y ) -> ( A. x e. X A. y e. Y ( th -> <. x , y >. = <. a , b >. ) -> ( [. d / y ]. [. c / x ]. th -> <. c , d >. = <. a , b >. ) ) )
61 60 ad2antlr
 |-  ( ( ( ( a e. X /\ b e. Y ) /\ ( c e. X /\ d e. Y ) ) /\ ch ) -> ( A. x e. X A. y e. Y ( th -> <. x , y >. = <. a , b >. ) -> ( [. d / y ]. [. c / x ]. th -> <. c , d >. = <. a , b >. ) ) )
62 2 sbcop
 |-  ( [. d / y ]. [. c / x ]. th <-> [. <. c , d >. / p ]. ps )
63 pm2.27
 |-  ( [. d / y ]. [. c / x ]. th -> ( ( [. d / y ]. [. c / x ]. th -> <. c , d >. = <. a , b >. ) -> <. c , d >. = <. a , b >. ) )
64 62 63 sylbir
 |-  ( [. <. c , d >. / p ]. ps -> ( ( [. d / y ]. [. c / x ]. th -> <. c , d >. = <. a , b >. ) -> <. c , d >. = <. a , b >. ) )
65 eqcom
 |-  ( <. a , b >. = <. c , d >. <-> <. c , d >. = <. a , b >. )
66 64 65 syl6ibr
 |-  ( [. <. c , d >. / p ]. ps -> ( ( [. d / y ]. [. c / x ]. th -> <. c , d >. = <. a , b >. ) -> <. a , b >. = <. c , d >. ) )
67 66 com12
 |-  ( ( [. d / y ]. [. c / x ]. th -> <. c , d >. = <. a , b >. ) -> ( [. <. c , d >. / p ]. ps -> <. a , b >. = <. c , d >. ) )
68 61 67 syl6
 |-  ( ( ( ( a e. X /\ b e. Y ) /\ ( c e. X /\ d e. Y ) ) /\ ch ) -> ( A. x e. X A. y e. Y ( th -> <. x , y >. = <. a , b >. ) -> ( [. <. c , d >. / p ]. ps -> <. a , b >. = <. c , d >. ) ) )
69 68 expimpd
 |-  ( ( ( a e. X /\ b e. Y ) /\ ( c e. X /\ d e. Y ) ) -> ( ( ch /\ A. x e. X A. y e. Y ( th -> <. x , y >. = <. a , b >. ) ) -> ( [. <. c , d >. / p ]. ps -> <. a , b >. = <. c , d >. ) ) )
70 69 expcom
 |-  ( ( c e. X /\ d e. Y ) -> ( ( a e. X /\ b e. Y ) -> ( ( ch /\ A. x e. X A. y e. Y ( th -> <. x , y >. = <. a , b >. ) ) -> ( [. <. c , d >. / p ]. ps -> <. a , b >. = <. c , d >. ) ) ) )
71 70 impd
 |-  ( ( c e. X /\ d e. Y ) -> ( ( ( a e. X /\ b e. Y ) /\ ( ch /\ A. x e. X A. y e. Y ( th -> <. x , y >. = <. a , b >. ) ) ) -> ( [. <. c , d >. / p ]. ps -> <. a , b >. = <. c , d >. ) ) )
72 71 impcom
 |-  ( ( ( ( a e. X /\ b e. Y ) /\ ( ch /\ A. x e. X A. y e. Y ( th -> <. x , y >. = <. a , b >. ) ) ) /\ ( c e. X /\ d e. Y ) ) -> ( [. <. c , d >. / p ]. ps -> <. a , b >. = <. c , d >. ) )
73 dfsbcq
 |-  ( q = <. c , d >. -> ( [. q / p ]. ps <-> [. <. c , d >. / p ]. ps ) )
74 eqeq2
 |-  ( q = <. c , d >. -> ( <. a , b >. = q <-> <. a , b >. = <. c , d >. ) )
75 73 74 imbi12d
 |-  ( q = <. c , d >. -> ( ( [. q / p ]. ps -> <. a , b >. = q ) <-> ( [. <. c , d >. / p ]. ps -> <. a , b >. = <. c , d >. ) ) )
76 72 75 syl5ibrcom
 |-  ( ( ( ( a e. X /\ b e. Y ) /\ ( ch /\ A. x e. X A. y e. Y ( th -> <. x , y >. = <. a , b >. ) ) ) /\ ( c e. X /\ d e. Y ) ) -> ( q = <. c , d >. -> ( [. q / p ]. ps -> <. a , b >. = q ) ) )
77 76 rexlimdvva
 |-  ( ( ( a e. X /\ b e. Y ) /\ ( ch /\ A. x e. X A. y e. Y ( th -> <. x , y >. = <. a , b >. ) ) ) -> ( E. c e. X E. d e. Y q = <. c , d >. -> ( [. q / p ]. ps -> <. a , b >. = q ) ) )
78 elxp2
 |-  ( q e. ( X X. Y ) <-> E. c e. X E. d e. Y q = <. c , d >. )
79 78 biimpi
 |-  ( q e. ( X X. Y ) -> E. c e. X E. d e. Y q = <. c , d >. )
80 77 79 impel
 |-  ( ( ( ( a e. X /\ b e. Y ) /\ ( ch /\ A. x e. X A. y e. Y ( th -> <. x , y >. = <. a , b >. ) ) ) /\ q e. ( X X. Y ) ) -> ( [. q / p ]. ps -> <. a , b >. = q ) )
81 80 ralrimiva
 |-  ( ( ( a e. X /\ b e. Y ) /\ ( ch /\ A. x e. X A. y e. Y ( th -> <. x , y >. = <. a , b >. ) ) ) -> A. q e. ( X X. Y ) ( [. q / p ]. ps -> <. a , b >. = q ) )
82 nfv
 |-  F/ p ch
83 nfcv
 |-  F/_ p ( X X. Y )
84 nfv
 |-  F/ p <. a , b >. = q
85 3 84 nfim
 |-  F/ p ( [. q / p ]. ps -> <. a , b >. = q )
86 83 85 nfralw
 |-  F/ p A. q e. ( X X. Y ) ( [. q / p ]. ps -> <. a , b >. = q )
87 82 86 nfan
 |-  F/ p ( ch /\ A. q e. ( X X. Y ) ( [. q / p ]. ps -> <. a , b >. = q ) )
88 eqeq1
 |-  ( p = <. a , b >. -> ( p = q <-> <. a , b >. = q ) )
89 88 imbi2d
 |-  ( p = <. a , b >. -> ( ( [. q / p ]. ps -> p = q ) <-> ( [. q / p ]. ps -> <. a , b >. = q ) ) )
90 89 ralbidv
 |-  ( p = <. a , b >. -> ( A. q e. ( X X. Y ) ( [. q / p ]. ps -> p = q ) <-> A. q e. ( X X. Y ) ( [. q / p ]. ps -> <. a , b >. = q ) ) )
91 1 90 anbi12d
 |-  ( p = <. a , b >. -> ( ( ps /\ A. q e. ( X X. Y ) ( [. q / p ]. ps -> p = q ) ) <-> ( ch /\ A. q e. ( X X. Y ) ( [. q / p ]. ps -> <. a , b >. = q ) ) ) )
92 87 91 rspce
 |-  ( ( <. a , b >. e. ( X X. Y ) /\ ( ch /\ A. q e. ( X X. Y ) ( [. q / p ]. ps -> <. a , b >. = q ) ) ) -> E. p e. ( X X. Y ) ( ps /\ A. q e. ( X X. Y ) ( [. q / p ]. ps -> p = q ) ) )
93 44 45 81 92 syl12anc
 |-  ( ( ( a e. X /\ b e. Y ) /\ ( ch /\ A. x e. X A. y e. Y ( th -> <. x , y >. = <. a , b >. ) ) ) -> E. p e. ( X X. Y ) ( ps /\ A. q e. ( X X. Y ) ( [. q / p ]. ps -> p = q ) ) )
94 93 ex
 |-  ( ( a e. X /\ b e. Y ) -> ( ( ch /\ A. x e. X A. y e. Y ( th -> <. x , y >. = <. a , b >. ) ) -> E. p e. ( X X. Y ) ( ps /\ A. q e. ( X X. Y ) ( [. q / p ]. ps -> p = q ) ) ) )
95 94 rexlimivv
 |-  ( E. a e. X E. b e. Y ( ch /\ A. x e. X A. y e. Y ( th -> <. x , y >. = <. a , b >. ) ) -> E. p e. ( X X. Y ) ( ps /\ A. q e. ( X X. Y ) ( [. q / p ]. ps -> p = q ) ) )
96 42 95 impbii
 |-  ( E. p e. ( X X. Y ) ( ps /\ A. q e. ( X X. Y ) ( [. q / p ]. ps -> p = q ) ) <-> E. a e. X E. b e. Y ( ch /\ A. x e. X A. y e. Y ( th -> <. x , y >. = <. a , b >. ) ) )
97 7 96 bitri
 |-  ( E! p e. ( X X. Y ) ps <-> E. a e. X E. b e. Y ( ch /\ A. x e. X A. y e. Y ( th -> <. x , y >. = <. a , b >. ) ) )