Metamath Proof Explorer

Theorem reupr

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

Ref Expression
Hypotheses reupr.a 
|- ( p = { a , b } -> ( ps <-> ch ) )
reupr.x 
|- ( p = { x , y } -> ( ps <-> th ) )
Assertion reupr 
|- ( X e. V -> ( E! p e. ( Pairs ` X ) ps <-> E. a e. X E. b e. X ( ch /\ A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) ) ) )

Proof

Step Hyp Ref Expression
1 reupr.a 
 |-  ( p = { a , b } -> ( ps <-> ch ) )
2 reupr.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. ( Pairs ` X ) ps <-> E. p e. ( Pairs ` X ) ( ps /\ A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) ) )
8 sprel 
 |-  ( p e. ( Pairs ` X ) -> E. a e. X E. b e. X p = { a , b } )
9 1 biimpcd 
 |-  ( ps -> ( p = { a , b } -> ch ) )
10 9 adantr 
 |-  ( ( ps /\ A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) ) -> ( p = { a , b } -> ch ) )
11 10 ad2antlr 
 |-  ( ( ( X e. V /\ ( ps /\ A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) ) ) /\ ( a e. X /\ b e. X ) ) -> ( p = { a , b } -> ch ) )
12 11 imp 
 |-  ( ( ( ( X e. V /\ ( ps /\ A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) ) ) /\ ( a e. X /\ b e. X ) ) /\ p = { a , b } ) -> ch )
13 pm3.22 
 |-  ( ( ( x e. X /\ y e. X ) /\ X e. V ) -> ( X e. V /\ ( x e. X /\ y e. X ) ) )
14 13 adantr 
 |-  ( ( ( ( x e. X /\ y e. X ) /\ X e. V ) /\ ps ) -> ( X e. V /\ ( x e. X /\ y e. X ) ) )
15 prelspr 
 |-  ( ( X e. V /\ ( x e. X /\ y e. X ) ) -> { x , y } e. ( Pairs ` X ) )
16 dfsbcq 
 |-  ( q = { x , y } -> ( [. q / p ]. ps <-> [. { x , y } / p ]. ps ) )
17 eqeq2 
 |-  ( q = { x , y } -> ( p = q <-> p = { x , y } ) )
18 16 17 imbi12d 
 |-  ( q = { x , y } -> ( ( [. q / p ]. ps -> p = q ) <-> ( [. { x , y } / p ]. ps -> p = { x , y } ) ) )
19 18 adantl 
 |-  ( ( ( X e. V /\ ( x e. X /\ y e. X ) ) /\ q = { x , y } ) -> ( ( [. q / p ]. ps -> p = q ) <-> ( [. { x , y } / p ]. ps -> p = { x , y } ) ) )
20 15 19 rspcdv 
 |-  ( ( X e. V /\ ( x e. X /\ y e. X ) ) -> ( A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) -> ( [. { x , y } / p ]. ps -> p = { x , y } ) ) )
21 14 20 syl 
 |-  ( ( ( ( x e. X /\ y e. X ) /\ X e. V ) /\ ps ) -> ( A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) -> ( [. { x , y } / p ]. ps -> p = { x , y } ) ) )
22 zfpair2 
 |-  { x , y } e. _V
23 22 2 sbcie 
 |-  ( [. { x , y } / p ]. ps <-> th )
24 pm2.27 
 |-  ( [. { x , y } / p ]. ps -> ( ( [. { x , y } / p ]. ps -> p = { x , y } ) -> p = { x , y } ) )
25 23 24 sylbir 
 |-  ( th -> ( ( [. { x , y } / p ]. ps -> p = { x , y } ) -> p = { x , y } ) )
26 eqcom 
 |-  ( { x , y } = p <-> p = { x , y } )
27 25 26 imbitrrdi 
 |-  ( th -> ( ( [. { x , y } / p ]. ps -> p = { x , y } ) -> { x , y } = p ) )
28 27 com12 
 |-  ( ( [. { x , y } / p ]. ps -> p = { x , y } ) -> ( th -> { x , y } = p ) )
29 eqeq2 
 |-  ( { a , b } = p -> ( { x , y } = { a , b } <-> { x , y } = p ) )
30 29 eqcoms 
 |-  ( p = { a , b } -> ( { x , y } = { a , b } <-> { x , y } = p ) )
31 30 imbi2d 
 |-  ( p = { a , b } -> ( ( th -> { x , y } = { a , b } ) <-> ( th -> { x , y } = p ) ) )
32 28 31 syl5ibrcom 
 |-  ( ( [. { x , y } / p ]. ps -> p = { x , y } ) -> ( p = { a , b } -> ( th -> { x , y } = { a , b } ) ) )
33 32 a1d 
 |-  ( ( [. { x , y } / p ]. ps -> p = { x , y } ) -> ( ( a e. X /\ b e. X ) -> ( p = { a , b } -> ( th -> { x , y } = { a , b } ) ) ) )
34 21 33 syl6 
 |-  ( ( ( ( x e. X /\ y e. X ) /\ X e. V ) /\ ps ) -> ( A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) -> ( ( a e. X /\ b e. X ) -> ( p = { a , b } -> ( th -> { x , y } = { a , b } ) ) ) ) )
35 34 expimpd 
 |-  ( ( ( x e. X /\ y e. X ) /\ X e. V ) -> ( ( ps /\ A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) ) -> ( ( a e. X /\ b e. X ) -> ( p = { a , b } -> ( th -> { x , y } = { a , b } ) ) ) ) )
36 35 expimpd 
 |-  ( ( x e. X /\ y e. X ) -> ( ( X e. V /\ ( ps /\ A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) ) ) -> ( ( a e. X /\ b e. X ) -> ( p = { a , b } -> ( th -> { x , y } = { a , b } ) ) ) ) )
37 36 imp4c 
 |-  ( ( x e. X /\ y e. X ) -> ( ( ( ( X e. V /\ ( ps /\ A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) ) ) /\ ( a e. X /\ b e. X ) ) /\ p = { a , b } ) -> ( th -> { x , y } = { a , b } ) ) )
38 37 impcom 
 |-  ( ( ( ( ( X e. V /\ ( ps /\ A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) ) ) /\ ( a e. X /\ b e. X ) ) /\ p = { a , b } ) /\ ( x e. X /\ y e. X ) ) -> ( th -> { x , y } = { a , b } ) )
39 38 ralrimivva 
 |-  ( ( ( ( X e. V /\ ( ps /\ A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) ) ) /\ ( a e. X /\ b e. X ) ) /\ p = { a , b } ) -> A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) )
40 12 39 jca 
 |-  ( ( ( ( X e. V /\ ( ps /\ A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) ) ) /\ ( a e. X /\ b e. X ) ) /\ p = { a , b } ) -> ( ch /\ A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) ) )
41 40 ex 
 |-  ( ( ( X e. V /\ ( ps /\ A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) ) ) /\ ( a e. X /\ b e. X ) ) -> ( p = { a , b } -> ( ch /\ A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) ) ) )
42 41 reximdvva 
 |-  ( ( X e. V /\ ( ps /\ A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) ) ) -> ( E. a e. X E. b e. X p = { a , b } -> E. a e. X E. b e. X ( ch /\ A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) ) ) )
43 42 expcom 
 |-  ( ( ps /\ A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) ) -> ( X e. V -> ( E. a e. X E. b e. X p = { a , b } -> E. a e. X E. b e. X ( ch /\ A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) ) ) ) )
44 43 com13 
 |-  ( E. a e. X E. b e. X p = { a , b } -> ( X e. V -> ( ( ps /\ A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) ) -> E. a e. X E. b e. X ( ch /\ A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) ) ) ) )
45 8 44 syl 
 |-  ( p e. ( Pairs ` X ) -> ( X e. V -> ( ( ps /\ A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) ) -> E. a e. X E. b e. X ( ch /\ A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) ) ) ) )
46 45 impcom 
 |-  ( ( X e. V /\ p e. ( Pairs ` X ) ) -> ( ( ps /\ A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) ) -> E. a e. X E. b e. X ( ch /\ A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) ) ) )
47 46 rexlimdva 
 |-  ( X e. V -> ( E. p e. ( Pairs ` X ) ( ps /\ A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) ) -> E. a e. X E. b e. X ( ch /\ A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) ) ) )
48 prelspr 
 |-  ( ( X e. V /\ ( a e. X /\ b e. X ) ) -> { a , b } e. ( Pairs ` X ) )
49 48 adantr 
 |-  ( ( ( X e. V /\ ( a e. X /\ b e. X ) ) /\ ( ch /\ A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) ) ) -> { a , b } e. ( Pairs ` X ) )
50 simprl 
 |-  ( ( ( X e. V /\ ( a e. X /\ b e. X ) ) /\ ( ch /\ A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) ) ) -> ch )
51 nfsbc1v 
 |-  F/ x [. c / x ]. th
52 nfv 
 |-  F/ x { c , y } = { a , b }
53 51 52 nfim 
 |-  F/ x ( [. c / x ]. th -> { c , y } = { a , b } )
54 nfsbc1v 
 |-  F/ y [. d / y ]. [. c / x ]. th
55 nfv 
 |-  F/ y { c , d } = { a , b }
56 54 55 nfim 
 |-  F/ y ( [. d / y ]. [. c / x ]. th -> { c , d } = { a , b } )
57 sbceq1a 
 |-  ( x = c -> ( th <-> [. c / x ]. th ) )
58 preq1 
 |-  ( x = c -> { x , y } = { c , y } )
59 58 eqeq1d 
 |-  ( x = c -> ( { x , y } = { a , b } <-> { c , y } = { a , b } ) )
60 57 59 imbi12d 
 |-  ( x = c -> ( ( th -> { x , y } = { a , b } ) <-> ( [. c / x ]. th -> { c , y } = { a , b } ) ) )
61 sbceq1a 
 |-  ( y = d -> ( [. c / x ]. th <-> [. d / y ]. [. c / x ]. th ) )
62 preq2 
 |-  ( y = d -> { c , y } = { c , d } )
63 62 eqeq1d 
 |-  ( y = d -> ( { c , y } = { a , b } <-> { c , d } = { a , b } ) )
64 61 63 imbi12d 
 |-  ( y = d -> ( ( [. c / x ]. th -> { c , y } = { a , b } ) <-> ( [. d / y ]. [. c / x ]. th -> { c , d } = { a , b } ) ) )
65 53 56 60 64 rspc2 
 |-  ( ( c e. X /\ d e. X ) -> ( A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) -> ( [. d / y ]. [. c / x ]. th -> { c , d } = { a , b } ) ) )
66 65 ad2antlr 
 |-  ( ( ( ( X e. V /\ ( a e. X /\ b e. X ) ) /\ ( c e. X /\ d e. X ) ) /\ ch ) -> ( A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) -> ( [. d / y ]. [. c / x ]. th -> { c , d } = { a , b } ) ) )
67 2 sbcpr 
 |-  ( [. { c , d } / p ]. ps <-> [. d / y ]. [. c / x ]. th )
68 pm2.27 
 |-  ( [. d / y ]. [. c / x ]. th -> ( ( [. d / y ]. [. c / x ]. th -> { c , d } = { a , b } ) -> { c , d } = { a , b } ) )
69 67 68 sylbi 
 |-  ( [. { c , d } / p ]. ps -> ( ( [. d / y ]. [. c / x ]. th -> { c , d } = { a , b } ) -> { c , d } = { a , b } ) )
70 eqcom 
 |-  ( { a , b } = { c , d } <-> { c , d } = { a , b } )
71 69 70 imbitrrdi 
 |-  ( [. { c , d } / p ]. ps -> ( ( [. d / y ]. [. c / x ]. th -> { c , d } = { a , b } ) -> { a , b } = { c , d } ) )
72 71 com12 
 |-  ( ( [. d / y ]. [. c / x ]. th -> { c , d } = { a , b } ) -> ( [. { c , d } / p ]. ps -> { a , b } = { c , d } ) )
73 66 72 syl6 
 |-  ( ( ( ( X e. V /\ ( a e. X /\ b e. X ) ) /\ ( c e. X /\ d e. X ) ) /\ ch ) -> ( A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) -> ( [. { c , d } / p ]. ps -> { a , b } = { c , d } ) ) )
74 73 expimpd 
 |-  ( ( ( X e. V /\ ( a e. X /\ b e. X ) ) /\ ( c e. X /\ d e. X ) ) -> ( ( ch /\ A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) ) -> ( [. { c , d } / p ]. ps -> { a , b } = { c , d } ) ) )
75 74 expcom 
 |-  ( ( c e. X /\ d e. X ) -> ( ( X e. V /\ ( a e. X /\ b e. X ) ) -> ( ( ch /\ A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) ) -> ( [. { c , d } / p ]. ps -> { a , b } = { c , d } ) ) ) )
76 75 impd 
 |-  ( ( c e. X /\ d e. X ) -> ( ( ( X e. V /\ ( a e. X /\ b e. X ) ) /\ ( ch /\ A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) ) ) -> ( [. { c , d } / p ]. ps -> { a , b } = { c , d } ) ) )
77 76 impcom 
 |-  ( ( ( ( X e. V /\ ( a e. X /\ b e. X ) ) /\ ( ch /\ A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) ) ) /\ ( c e. X /\ d e. X ) ) -> ( [. { c , d } / p ]. ps -> { a , b } = { c , d } ) )
78 dfsbcq 
 |-  ( q = { c , d } -> ( [. q / p ]. ps <-> [. { c , d } / p ]. ps ) )
79 eqeq2 
 |-  ( q = { c , d } -> ( { a , b } = q <-> { a , b } = { c , d } ) )
80 78 79 imbi12d 
 |-  ( q = { c , d } -> ( ( [. q / p ]. ps -> { a , b } = q ) <-> ( [. { c , d } / p ]. ps -> { a , b } = { c , d } ) ) )
81 77 80 syl5ibrcom 
 |-  ( ( ( ( X e. V /\ ( a e. X /\ b e. X ) ) /\ ( ch /\ A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) ) ) /\ ( c e. X /\ d e. X ) ) -> ( q = { c , d } -> ( [. q / p ]. ps -> { a , b } = q ) ) )
82 81 rexlimdvva 
 |-  ( ( ( X e. V /\ ( a e. X /\ b e. X ) ) /\ ( ch /\ A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) ) ) -> ( E. c e. X E. d e. X q = { c , d } -> ( [. q / p ]. ps -> { a , b } = q ) ) )
83 sprel 
 |-  ( q e. ( Pairs ` X ) -> E. c e. X E. d e. X q = { c , d } )
84 82 83 impel 
 |-  ( ( ( ( X e. V /\ ( a e. X /\ b e. X ) ) /\ ( ch /\ A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) ) ) /\ q e. ( Pairs ` X ) ) -> ( [. q / p ]. ps -> { a , b } = q ) )
85 84 ralrimiva 
 |-  ( ( ( X e. V /\ ( a e. X /\ b e. X ) ) /\ ( ch /\ A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) ) ) -> A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> { a , b } = q ) )
86 nfv 
 |-  F/ p ch
87 nfcv 
 |-  F/_ p ( Pairs ` X )
88 nfv 
 |-  F/ p { a , b } = q
89 3 88 nfim 
 |-  F/ p ( [. q / p ]. ps -> { a , b } = q )
90 87 89 nfralw 
 |-  F/ p A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> { a , b } = q )
91 86 90 nfan 
 |-  F/ p ( ch /\ A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> { a , b } = q ) )
92 eqeq1 
 |-  ( p = { a , b } -> ( p = q <-> { a , b } = q ) )
93 92 imbi2d 
 |-  ( p = { a , b } -> ( ( [. q / p ]. ps -> p = q ) <-> ( [. q / p ]. ps -> { a , b } = q ) ) )
94 93 ralbidv 
 |-  ( p = { a , b } -> ( A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) <-> A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> { a , b } = q ) ) )
95 1 94 anbi12d 
 |-  ( p = { a , b } -> ( ( ps /\ A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) ) <-> ( ch /\ A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> { a , b } = q ) ) ) )
96 91 95 rspce 
 |-  ( ( { a , b } e. ( Pairs ` X ) /\ ( ch /\ A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> { a , b } = q ) ) ) -> E. p e. ( Pairs ` X ) ( ps /\ A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) ) )
97 49 50 85 96 syl12anc 
 |-  ( ( ( X e. V /\ ( a e. X /\ b e. X ) ) /\ ( ch /\ A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) ) ) -> E. p e. ( Pairs ` X ) ( ps /\ A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) ) )
98 97 ex 
 |-  ( ( X e. V /\ ( a e. X /\ b e. X ) ) -> ( ( ch /\ A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) ) -> E. p e. ( Pairs ` X ) ( ps /\ A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) ) ) )
99 98 rexlimdvva 
 |-  ( X e. V -> ( E. a e. X E. b e. X ( ch /\ A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) ) -> E. p e. ( Pairs ` X ) ( ps /\ A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) ) ) )
100 47 99 impbid 
 |-  ( X e. V -> ( E. p e. ( Pairs ` X ) ( ps /\ A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) ) <-> E. a e. X E. b e. X ( ch /\ A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) ) ) )
101 7 100 bitrid 
 |-  ( X e. V -> ( E! p e. ( Pairs ` X ) ps <-> E. a e. X E. b e. X ( ch /\ A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) ) ) )