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 syl6ibr
 |-  ( 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 syl6ibr
 |-  ( [. { 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 syl5bb
 |-  ( 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 } ) ) ) )