Metamath Proof Explorer

Theorem opreu2reuALT

Description: Correspondence between uniqueness of ordered pairs and double restricted existential uniqueness quantification. Alternate proof of one direction only, use opreu2reurex instead. (Contributed by Thierry Arnoux, 4-Jul-2023) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis opsbc2ie.a 
|- ( p = <. a , b >. -> ( ph <-> ch ) )
Assertion opreu2reuALT 
|- ( ( E! a e. A E. b e. B ch /\ E! b e. B E. a e. A ch ) -> E! p e. ( A X. B ) ph )

Proof

Step Hyp Ref Expression
1 opsbc2ie.a 
 |-  ( p = <. a , b >. -> ( ph <-> ch ) )
2 2reu4 
 |-  ( ( E! a e. A E. b e. B ch /\ E! b e. B E. a e. A ch ) <-> ( E. a e. A E. b e. B ch /\ E. x e. A E. y e. B A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) ) )
3 simpllr 
 |-  ( ( ( ( E. a e. A E. b e. B ch /\ x e. A ) /\ y e. B ) /\ A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) ) -> x e. A )
4 simplr 
 |-  ( ( ( ( E. a e. A E. b e. B ch /\ x e. A ) /\ y e. B ) /\ A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) ) -> y e. B )
5 opelxpi 
 |-  ( ( x e. A /\ y e. B ) -> <. x , y >. e. ( A X. B ) )
6 3 4 5 syl2anc 
 |-  ( ( ( ( E. a e. A E. b e. B ch /\ x e. A ) /\ y e. B ) /\ A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) ) -> <. x , y >. e. ( A X. B ) )
7 nfre1 
 |-  F/ a E. a e. A E. b e. B ch
8 nfv 
 |-  F/ a x e. A
9 7 8 nfan 
 |-  F/ a ( E. a e. A E. b e. B ch /\ x e. A )
10 nfv 
 |-  F/ a y e. B
11 9 10 nfan 
 |-  F/ a ( ( E. a e. A E. b e. B ch /\ x e. A ) /\ y e. B )
12 nfra1 
 |-  F/ a A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) )
13 11 12 nfan 
 |-  F/ a ( ( ( E. a e. A E. b e. B ch /\ x e. A ) /\ y e. B ) /\ A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) )
14 nfcv 
 |-  F/_ a y
15 nfsbc1v 
 |-  F/ a [. x / a ]. ch
16 14 15 nfsbc 
 |-  F/ a [. y / b ]. [. x / a ]. ch
17 nfcv 
 |-  F/_ b A
18 nfre1 
 |-  F/ b E. b e. B ch
19 17 18 nfrexw 
 |-  F/ b E. a e. A E. b e. B ch
20 nfv 
 |-  F/ b x e. A
21 19 20 nfan 
 |-  F/ b ( E. a e. A E. b e. B ch /\ x e. A )
22 nfv 
 |-  F/ b y e. B
23 21 22 nfan 
 |-  F/ b ( ( E. a e. A E. b e. B ch /\ x e. A ) /\ y e. B )
24 nfra1 
 |-  F/ b A. b e. B ( ch -> ( a = x /\ b = y ) )
25 17 24 nfral 
 |-  F/ b A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) )
26 23 25 nfan 
 |-  F/ b ( ( ( E. a e. A E. b e. B ch /\ x e. A ) /\ y e. B ) /\ A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) )
27 nfv 
 |-  F/ b a e. A
28 26 27 nfan 
 |-  F/ b ( ( ( ( E. a e. A E. b e. B ch /\ x e. A ) /\ y e. B ) /\ A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) ) /\ a e. A )
29 28 18 nfan 
 |-  F/ b ( ( ( ( ( E. a e. A E. b e. B ch /\ x e. A ) /\ y e. B ) /\ A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) ) /\ a e. A ) /\ E. b e. B ch )
30 nfsbc1v 
 |-  F/ b [. y / b ]. [. x / a ]. ch
31 rspa 
 |-  ( ( A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) /\ a e. A ) -> A. b e. B ( ch -> ( a = x /\ b = y ) ) )
32 31 ad5ant23 
 |-  ( ( ( ( ( ( ( E. a e. A E. b e. B ch /\ x e. A ) /\ y e. B ) /\ A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) ) /\ a e. A ) /\ b e. B ) /\ ch ) -> A. b e. B ( ch -> ( a = x /\ b = y ) ) )
33 simplr 
 |-  ( ( ( ( ( ( ( E. a e. A E. b e. B ch /\ x e. A ) /\ y e. B ) /\ A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) ) /\ a e. A ) /\ b e. B ) /\ ch ) -> b e. B )
34 simpr 
 |-  ( ( ( ( ( ( ( E. a e. A E. b e. B ch /\ x e. A ) /\ y e. B ) /\ A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) ) /\ a e. A ) /\ b e. B ) /\ ch ) -> ch )
35 rspa 
 |-  ( ( A. b e. B ( ch -> ( a = x /\ b = y ) ) /\ b e. B ) -> ( ch -> ( a = x /\ b = y ) ) )
36 35 imp 
 |-  ( ( ( A. b e. B ( ch -> ( a = x /\ b = y ) ) /\ b e. B ) /\ ch ) -> ( a = x /\ b = y ) )
37 32 33 34 36 syl21anc 
 |-  ( ( ( ( ( ( ( E. a e. A E. b e. B ch /\ x e. A ) /\ y e. B ) /\ A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) ) /\ a e. A ) /\ b e. B ) /\ ch ) -> ( a = x /\ b = y ) )
38 37 simprd 
 |-  ( ( ( ( ( ( ( E. a e. A E. b e. B ch /\ x e. A ) /\ y e. B ) /\ A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) ) /\ a e. A ) /\ b e. B ) /\ ch ) -> b = y )
39 37 simpld 
 |-  ( ( ( ( ( ( ( E. a e. A E. b e. B ch /\ x e. A ) /\ y e. B ) /\ A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) ) /\ a e. A ) /\ b e. B ) /\ ch ) -> a = x )
40 sbceq1a 
 |-  ( a = x -> ( ch <-> [. x / a ]. ch ) )
41 40 biimpa 
 |-  ( ( a = x /\ ch ) -> [. x / a ]. ch )
42 39 34 41 syl2anc 
 |-  ( ( ( ( ( ( ( E. a e. A E. b e. B ch /\ x e. A ) /\ y e. B ) /\ A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) ) /\ a e. A ) /\ b e. B ) /\ ch ) -> [. x / a ]. ch )
43 sbceq1a 
 |-  ( b = y -> ( [. x / a ]. ch <-> [. y / b ]. [. x / a ]. ch ) )
44 43 biimpa 
 |-  ( ( b = y /\ [. x / a ]. ch ) -> [. y / b ]. [. x / a ]. ch )
45 38 42 44 syl2anc 
 |-  ( ( ( ( ( ( ( E. a e. A E. b e. B ch /\ x e. A ) /\ y e. B ) /\ A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) ) /\ a e. A ) /\ b e. B ) /\ ch ) -> [. y / b ]. [. x / a ]. ch )
46 45 adantllr 
 |-  ( ( ( ( ( ( ( ( E. a e. A E. b e. B ch /\ x e. A ) /\ y e. B ) /\ A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) ) /\ a e. A ) /\ E. b e. B ch ) /\ b e. B ) /\ ch ) -> [. y / b ]. [. x / a ]. ch )
47 simpr 
 |-  ( ( ( ( ( ( E. a e. A E. b e. B ch /\ x e. A ) /\ y e. B ) /\ A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) ) /\ a e. A ) /\ E. b e. B ch ) -> E. b e. B ch )
48 29 30 46 47 r19.29af2 
 |-  ( ( ( ( ( ( E. a e. A E. b e. B ch /\ x e. A ) /\ y e. B ) /\ A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) ) /\ a e. A ) /\ E. b e. B ch ) -> [. y / b ]. [. x / a ]. ch )
49 simplll 
 |-  ( ( ( ( E. a e. A E. b e. B ch /\ x e. A ) /\ y e. B ) /\ A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) ) -> E. a e. A E. b e. B ch )
50 13 16 48 49 r19.29af2 
 |-  ( ( ( ( E. a e. A E. b e. B ch /\ x e. A ) /\ y e. B ) /\ A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) ) -> [. y / b ]. [. x / a ]. ch )
51 1st2nd2 
 |-  ( p e. ( A X. B ) -> p = <. ( 1st ` p ) , ( 2nd ` p ) >. )
52 51 ad2antlr 
 |-  ( ( ( ( ( ( E. a e. A E. b e. B ch /\ x e. A ) /\ y e. B ) /\ A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) ) /\ p e. ( A X. B ) ) /\ ph ) -> p = <. ( 1st ` p ) , ( 2nd ` p ) >. )
53 nfv 
 |-  F/ a p e. ( A X. B )
54 13 53 nfan 
 |-  F/ a ( ( ( ( E. a e. A E. b e. B ch /\ x e. A ) /\ y e. B ) /\ A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) ) /\ p e. ( A X. B ) )
55 nfv 
 |-  F/ a ph
56 54 55 nfan 
 |-  F/ a ( ( ( ( ( E. a e. A E. b e. B ch /\ x e. A ) /\ y e. B ) /\ A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) ) /\ p e. ( A X. B ) ) /\ ph )
57 nfv 
 |-  F/ b p e. ( A X. B )
58 26 57 nfan 
 |-  F/ b ( ( ( ( E. a e. A E. b e. B ch /\ x e. A ) /\ y e. B ) /\ A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) ) /\ p e. ( A X. B ) )
59 nfv 
 |-  F/ b ph
60 58 59 nfan 
 |-  F/ b ( ( ( ( ( E. a e. A E. b e. B ch /\ x e. A ) /\ y e. B ) /\ A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) ) /\ p e. ( A X. B ) ) /\ ph )
61 nfv 
 |-  F/ a ( ph -> ( ( 1st ` p ) = x /\ ( 2nd ` p ) = y ) )
62 nfv 
 |-  F/ b ( ph -> ( ( 1st ` p ) = x /\ ( 2nd ` p ) = y ) )
63 xp1st 
 |-  ( p e. ( A X. B ) -> ( 1st ` p ) e. A )
64 63 ad2antlr 
 |-  ( ( ( ( ( ( E. a e. A E. b e. B ch /\ x e. A ) /\ y e. B ) /\ A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) ) /\ p e. ( A X. B ) ) /\ ph ) -> ( 1st ` p ) e. A )
65 xp2nd 
 |-  ( p e. ( A X. B ) -> ( 2nd ` p ) e. B )
66 65 ad2antlr 
 |-  ( ( ( ( ( ( E. a e. A E. b e. B ch /\ x e. A ) /\ y e. B ) /\ A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) ) /\ p e. ( A X. B ) ) /\ ph ) -> ( 2nd ` p ) e. B )
67 eqcom 
 |-  ( ( 1st ` p ) = a <-> a = ( 1st ` p ) )
68 eqcom 
 |-  ( ( 2nd ` p ) = b <-> b = ( 2nd ` p ) )
69 eqopi 
 |-  ( ( p e. ( A X. B ) /\ ( ( 1st ` p ) = a /\ ( 2nd ` p ) = b ) ) -> p = <. a , b >. )
70 69 1 syl 
 |-  ( ( p e. ( A X. B ) /\ ( ( 1st ` p ) = a /\ ( 2nd ` p ) = b ) ) -> ( ph <-> ch ) )
71 70 bicomd 
 |-  ( ( p e. ( A X. B ) /\ ( ( 1st ` p ) = a /\ ( 2nd ` p ) = b ) ) -> ( ch <-> ph ) )
72 71 ancoms 
 |-  ( ( ( ( 1st ` p ) = a /\ ( 2nd ` p ) = b ) /\ p e. ( A X. B ) ) -> ( ch <-> ph ) )
73 72 ex 
 |-  ( ( ( 1st ` p ) = a /\ ( 2nd ` p ) = b ) -> ( p e. ( A X. B ) -> ( ch <-> ph ) ) )
74 67 68 73 syl2anbr 
 |-  ( ( a = ( 1st ` p ) /\ b = ( 2nd ` p ) ) -> ( p e. ( A X. B ) -> ( ch <-> ph ) ) )
75 74 impcom 
 |-  ( ( p e. ( A X. B ) /\ ( a = ( 1st ` p ) /\ b = ( 2nd ` p ) ) ) -> ( ch <-> ph ) )
76 75 ad4ant24 
 |-  ( ( ( ( ( ( ( E. a e. A E. b e. B ch /\ x e. A ) /\ y e. B ) /\ A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) ) /\ p e. ( A X. B ) ) /\ ph ) /\ ( a = ( 1st ` p ) /\ b = ( 2nd ` p ) ) ) -> ( ch <-> ph ) )
77 simpl 
 |-  ( ( a = ( 1st ` p ) /\ b = ( 2nd ` p ) ) -> a = ( 1st ` p ) )
78 77 eqeq1d 
 |-  ( ( a = ( 1st ` p ) /\ b = ( 2nd ` p ) ) -> ( a = x <-> ( 1st ` p ) = x ) )
79 simpr 
 |-  ( ( a = ( 1st ` p ) /\ b = ( 2nd ` p ) ) -> b = ( 2nd ` p ) )
80 79 eqeq1d 
 |-  ( ( a = ( 1st ` p ) /\ b = ( 2nd ` p ) ) -> ( b = y <-> ( 2nd ` p ) = y ) )
81 78 80 anbi12d 
 |-  ( ( a = ( 1st ` p ) /\ b = ( 2nd ` p ) ) -> ( ( a = x /\ b = y ) <-> ( ( 1st ` p ) = x /\ ( 2nd ` p ) = y ) ) )
82 81 adantl 
 |-  ( ( ( ( ( ( ( E. a e. A E. b e. B ch /\ x e. A ) /\ y e. B ) /\ A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) ) /\ p e. ( A X. B ) ) /\ ph ) /\ ( a = ( 1st ` p ) /\ b = ( 2nd ` p ) ) ) -> ( ( a = x /\ b = y ) <-> ( ( 1st ` p ) = x /\ ( 2nd ` p ) = y ) ) )
83 76 82 imbi12d 
 |-  ( ( ( ( ( ( ( E. a e. A E. b e. B ch /\ x e. A ) /\ y e. B ) /\ A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) ) /\ p e. ( A X. B ) ) /\ ph ) /\ ( a = ( 1st ` p ) /\ b = ( 2nd ` p ) ) ) -> ( ( ch -> ( a = x /\ b = y ) ) <-> ( ph -> ( ( 1st ` p ) = x /\ ( 2nd ` p ) = y ) ) ) )
84 simpllr 
 |-  ( ( ( ( ( ( E. a e. A E. b e. B ch /\ x e. A ) /\ y e. B ) /\ A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) ) /\ p e. ( A X. B ) ) /\ ph ) -> A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) )
85 56 60 61 62 64 66 83 84 rspc2daf 
 |-  ( ( ( ( ( ( E. a e. A E. b e. B ch /\ x e. A ) /\ y e. B ) /\ A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) ) /\ p e. ( A X. B ) ) /\ ph ) -> ( ph -> ( ( 1st ` p ) = x /\ ( 2nd ` p ) = y ) ) )
86 85 com12 
 |-  ( ph -> ( ( ( ( ( ( E. a e. A E. b e. B ch /\ x e. A ) /\ y e. B ) /\ A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) ) /\ p e. ( A X. B ) ) /\ ph ) -> ( ( 1st ` p ) = x /\ ( 2nd ` p ) = y ) ) )
87 86 anabsi7 
 |-  ( ( ( ( ( ( E. a e. A E. b e. B ch /\ x e. A ) /\ y e. B ) /\ A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) ) /\ p e. ( A X. B ) ) /\ ph ) -> ( ( 1st ` p ) = x /\ ( 2nd ` p ) = y ) )
88 87 simpld 
 |-  ( ( ( ( ( ( E. a e. A E. b e. B ch /\ x e. A ) /\ y e. B ) /\ A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) ) /\ p e. ( A X. B ) ) /\ ph ) -> ( 1st ` p ) = x )
89 87 simprd 
 |-  ( ( ( ( ( ( E. a e. A E. b e. B ch /\ x e. A ) /\ y e. B ) /\ A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) ) /\ p e. ( A X. B ) ) /\ ph ) -> ( 2nd ` p ) = y )
90 88 89 opeq12d 
 |-  ( ( ( ( ( ( E. a e. A E. b e. B ch /\ x e. A ) /\ y e. B ) /\ A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) ) /\ p e. ( A X. B ) ) /\ ph ) -> <. ( 1st ` p ) , ( 2nd ` p ) >. = <. x , y >. )
91 52 90 eqtrd 
 |-  ( ( ( ( ( ( E. a e. A E. b e. B ch /\ x e. A ) /\ y e. B ) /\ A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) ) /\ p e. ( A X. B ) ) /\ ph ) -> p = <. x , y >. )
92 91 ex 
 |-  ( ( ( ( ( E. a e. A E. b e. B ch /\ x e. A ) /\ y e. B ) /\ A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) ) /\ p e. ( A X. B ) ) -> ( ph -> p = <. x , y >. ) )
93 92 ralrimiva 
 |-  ( ( ( ( E. a e. A E. b e. B ch /\ x e. A ) /\ y e. B ) /\ A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) ) -> A. p e. ( A X. B ) ( ph -> p = <. x , y >. ) )
94 6 50 93 3jca 
 |-  ( ( ( ( E. a e. A E. b e. B ch /\ x e. A ) /\ y e. B ) /\ A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) ) -> ( <. x , y >. e. ( A X. B ) /\ [. y / b ]. [. x / a ]. ch /\ A. p e. ( A X. B ) ( ph -> p = <. x , y >. ) ) )
95 1 opsbc2ie 
 |-  ( p = <. x , y >. -> ( ph <-> [. y / b ]. [. x / a ]. ch ) )
96 95 eqreu 
 |-  ( ( <. x , y >. e. ( A X. B ) /\ [. y / b ]. [. x / a ]. ch /\ A. p e. ( A X. B ) ( ph -> p = <. x , y >. ) ) -> E! p e. ( A X. B ) ph )
97 94 96 syl 
 |-  ( ( ( ( E. a e. A E. b e. B ch /\ x e. A ) /\ y e. B ) /\ A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) ) -> E! p e. ( A X. B ) ph )
98 97 r19.29ffa 
 |-  ( ( E. a e. A E. b e. B ch /\ E. x e. A E. y e. B A. a e. A A. b e. B ( ch -> ( a = x /\ b = y ) ) ) -> E! p e. ( A X. B ) ph )
99 2 98 sylbi 
 |-  ( ( E! a e. A E. b e. B ch /\ E! b e. B E. a e. A ch ) -> E! p e. ( A X. B ) ph )