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 imbitrrdi 
 |-  ( 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 imbitrrdi 
 |-  ( [. <. 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 >. ) ) )