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=ab→ψ↔χ
reupr.x ⊢p=xy→ψ↔θ
Assertion reupr ⊢X∈V→∃!p∈Pairs⁡Xψ↔∃a∈X∃b∈Xχ∧∀x∈X∀y∈Xθ→xy=ab

Proof

Step Hyp Ref Expression
1 reupr.a ⊢p=ab→ψ↔χ
2 reupr.x ⊢p=xy→ψ↔θ
3 nfsbc1v ⊢Ⅎp[˙q/p]˙ψ
4 nfsbc1v ⊢Ⅎp[˙w/p]˙ψ
5 sbceq1a ⊢p=w→ψ↔[˙w/p]˙ψ
6 dfsbcq ⊢w=q→[˙w/p]˙ψ↔[˙q/p]˙ψ
7 3 4 5 6 reu8nf ⊢∃!p∈Pairs⁡Xψ↔∃p∈Pairs⁡Xψ∧∀q∈Pairs⁡X[˙q/p]˙ψ→p=q
8 sprel ⊢p∈Pairs⁡X→∃a∈X∃b∈Xp=ab
9 1 biimpcd ⊢ψ→p=ab→χ
10 9 adantr ⊢ψ∧∀q∈Pairs⁡X[˙q/p]˙ψ→p=q→p=ab→χ
11 10 ad2antlr ⊢X∈V∧ψ∧∀q∈Pairs⁡X[˙q/p]˙ψ→p=q∧a∈X∧b∈X→p=ab→χ
12 11 imp ⊢X∈V∧ψ∧∀q∈Pairs⁡X[˙q/p]˙ψ→p=q∧a∈X∧b∈X∧p=ab→χ
13 pm3.22 ⊢x∈X∧y∈X∧X∈V→X∈V∧x∈X∧y∈X
14 13 adantr ⊢x∈X∧y∈X∧X∈V∧ψ→X∈V∧x∈X∧y∈X
15 prelspr ⊢X∈V∧x∈X∧y∈X→xy∈Pairs⁡X
16 dfsbcq ⊢q=xy→[˙q/p]˙ψ↔[˙xy/p]˙ψ
17 eqeq2 ⊢q=xy→p=q↔p=xy
18 16 17 imbi12d ⊢q=xy→[˙q/p]˙ψ→p=q↔[˙xy/p]˙ψ→p=xy
19 18 adantl ⊢X∈V∧x∈X∧y∈X∧q=xy→[˙q/p]˙ψ→p=q↔[˙xy/p]˙ψ→p=xy
20 15 19 rspcdv ⊢X∈V∧x∈X∧y∈X→∀q∈Pairs⁡X[˙q/p]˙ψ→p=q→[˙xy/p]˙ψ→p=xy
21 14 20 syl ⊢x∈X∧y∈X∧X∈V∧ψ→∀q∈Pairs⁡X[˙q/p]˙ψ→p=q→[˙xy/p]˙ψ→p=xy
22 zfpair2 ⊢xy∈V
23 22 2 sbcie ⊢[˙xy/p]˙ψ↔θ
24 pm2.27 ⊢[˙xy/p]˙ψ→[˙xy/p]˙ψ→p=xy→p=xy
25 23 24 sylbir ⊢θ→[˙xy/p]˙ψ→p=xy→p=xy
26 eqcom ⊢xy=p↔p=xy
27 25 26 syl6ibr ⊢θ→[˙xy/p]˙ψ→p=xy→xy=p
28 27 com12 ⊢[˙xy/p]˙ψ→p=xy→θ→xy=p
29 eqeq2 ⊢ab=p→xy=ab↔xy=p
30 29 eqcoms ⊢p=ab→xy=ab↔xy=p
31 30 imbi2d ⊢p=ab→θ→xy=ab↔θ→xy=p
32 28 31 syl5ibrcom ⊢[˙xy/p]˙ψ→p=xy→p=ab→θ→xy=ab
33 32 a1d ⊢[˙xy/p]˙ψ→p=xy→a∈X∧b∈X→p=ab→θ→xy=ab
34 21 33 syl6 ⊢x∈X∧y∈X∧X∈V∧ψ→∀q∈Pairs⁡X[˙q/p]˙ψ→p=q→a∈X∧b∈X→p=ab→θ→xy=ab
35 34 expimpd ⊢x∈X∧y∈X∧X∈V→ψ∧∀q∈Pairs⁡X[˙q/p]˙ψ→p=q→a∈X∧b∈X→p=ab→θ→xy=ab
36 35 expimpd ⊢x∈X∧y∈X→X∈V∧ψ∧∀q∈Pairs⁡X[˙q/p]˙ψ→p=q→a∈X∧b∈X→p=ab→θ→xy=ab
37 36 imp4c ⊢x∈X∧y∈X→X∈V∧ψ∧∀q∈Pairs⁡X[˙q/p]˙ψ→p=q∧a∈X∧b∈X∧p=ab→θ→xy=ab
38 37 impcom ⊢X∈V∧ψ∧∀q∈Pairs⁡X[˙q/p]˙ψ→p=q∧a∈X∧b∈X∧p=ab∧x∈X∧y∈X→θ→xy=ab
39 38 ralrimivva ⊢X∈V∧ψ∧∀q∈Pairs⁡X[˙q/p]˙ψ→p=q∧a∈X∧b∈X∧p=ab→∀x∈X∀y∈Xθ→xy=ab
40 12 39 jca ⊢X∈V∧ψ∧∀q∈Pairs⁡X[˙q/p]˙ψ→p=q∧a∈X∧b∈X∧p=ab→χ∧∀x∈X∀y∈Xθ→xy=ab
41 40 ex ⊢X∈V∧ψ∧∀q∈Pairs⁡X[˙q/p]˙ψ→p=q∧a∈X∧b∈X→p=ab→χ∧∀x∈X∀y∈Xθ→xy=ab
42 41 reximdvva ⊢X∈V∧ψ∧∀q∈Pairs⁡X[˙q/p]˙ψ→p=q→∃a∈X∃b∈Xp=ab→∃a∈X∃b∈Xχ∧∀x∈X∀y∈Xθ→xy=ab
43 42 expcom ⊢ψ∧∀q∈Pairs⁡X[˙q/p]˙ψ→p=q→X∈V→∃a∈X∃b∈Xp=ab→∃a∈X∃b∈Xχ∧∀x∈X∀y∈Xθ→xy=ab
44 43 com13 ⊢∃a∈X∃b∈Xp=ab→X∈V→ψ∧∀q∈Pairs⁡X[˙q/p]˙ψ→p=q→∃a∈X∃b∈Xχ∧∀x∈X∀y∈Xθ→xy=ab
45 8 44 syl ⊢p∈Pairs⁡X→X∈V→ψ∧∀q∈Pairs⁡X[˙q/p]˙ψ→p=q→∃a∈X∃b∈Xχ∧∀x∈X∀y∈Xθ→xy=ab
46 45 impcom ⊢X∈V∧p∈Pairs⁡X→ψ∧∀q∈Pairs⁡X[˙q/p]˙ψ→p=q→∃a∈X∃b∈Xχ∧∀x∈X∀y∈Xθ→xy=ab
47 46 rexlimdva ⊢X∈V→∃p∈Pairs⁡Xψ∧∀q∈Pairs⁡X[˙q/p]˙ψ→p=q→∃a∈X∃b∈Xχ∧∀x∈X∀y∈Xθ→xy=ab
48 prelspr ⊢X∈V∧a∈X∧b∈X→ab∈Pairs⁡X
49 48 adantr ⊢X∈V∧a∈X∧b∈X∧χ∧∀x∈X∀y∈Xθ→xy=ab→ab∈Pairs⁡X
50 simprl ⊢X∈V∧a∈X∧b∈X∧χ∧∀x∈X∀y∈Xθ→xy=ab→χ
51 nfsbc1v ⊢Ⅎx[˙c/x]˙θ
52 nfv ⊢Ⅎxcy=ab
53 51 52 nfim ⊢Ⅎx[˙c/x]˙θ→cy=ab
54 nfsbc1v ⊢Ⅎy[˙d/y]˙[˙c/x]˙θ
55 nfv ⊢Ⅎycd=ab
56 54 55 nfim ⊢Ⅎy[˙d/y]˙[˙c/x]˙θ→cd=ab
57 sbceq1a ⊢x=c→θ↔[˙c/x]˙θ
58 preq1 ⊢x=c→xy=cy
59 58 eqeq1d ⊢x=c→xy=ab↔cy=ab
60 57 59 imbi12d ⊢x=c→θ→xy=ab↔[˙c/x]˙θ→cy=ab
61 sbceq1a ⊢y=d→[˙c/x]˙θ↔[˙d/y]˙[˙c/x]˙θ
62 preq2 ⊢y=d→cy=cd
63 62 eqeq1d ⊢y=d→cy=ab↔cd=ab
64 61 63 imbi12d ⊢y=d→[˙c/x]˙θ→cy=ab↔[˙d/y]˙[˙c/x]˙θ→cd=ab
65 53 56 60 64 rspc2 ⊢c∈X∧d∈X→∀x∈X∀y∈Xθ→xy=ab→[˙d/y]˙[˙c/x]˙θ→cd=ab
66 65 ad2antlr ⊢X∈V∧a∈X∧b∈X∧c∈X∧d∈X∧χ→∀x∈X∀y∈Xθ→xy=ab→[˙d/y]˙[˙c/x]˙θ→cd=ab
67 2 sbcpr ⊢[˙cd/p]˙ψ↔[˙d/y]˙[˙c/x]˙θ
68 pm2.27 ⊢[˙d/y]˙[˙c/x]˙θ→[˙d/y]˙[˙c/x]˙θ→cd=ab→cd=ab
69 67 68 sylbi ⊢[˙cd/p]˙ψ→[˙d/y]˙[˙c/x]˙θ→cd=ab→cd=ab
70 eqcom ⊢ab=cd↔cd=ab
71 69 70 syl6ibr ⊢[˙cd/p]˙ψ→[˙d/y]˙[˙c/x]˙θ→cd=ab→ab=cd
72 71 com12 ⊢[˙d/y]˙[˙c/x]˙θ→cd=ab→[˙cd/p]˙ψ→ab=cd
73 66 72 syl6 ⊢X∈V∧a∈X∧b∈X∧c∈X∧d∈X∧χ→∀x∈X∀y∈Xθ→xy=ab→[˙cd/p]˙ψ→ab=cd
74 73 expimpd ⊢X∈V∧a∈X∧b∈X∧c∈X∧d∈X→χ∧∀x∈X∀y∈Xθ→xy=ab→[˙cd/p]˙ψ→ab=cd
75 74 expcom ⊢c∈X∧d∈X→X∈V∧a∈X∧b∈X→χ∧∀x∈X∀y∈Xθ→xy=ab→[˙cd/p]˙ψ→ab=cd
76 75 impd ⊢c∈X∧d∈X→X∈V∧a∈X∧b∈X∧χ∧∀x∈X∀y∈Xθ→xy=ab→[˙cd/p]˙ψ→ab=cd
77 76 impcom ⊢X∈V∧a∈X∧b∈X∧χ∧∀x∈X∀y∈Xθ→xy=ab∧c∈X∧d∈X→[˙cd/p]˙ψ→ab=cd
78 dfsbcq ⊢q=cd→[˙q/p]˙ψ↔[˙cd/p]˙ψ
79 eqeq2 ⊢q=cd→ab=q↔ab=cd
80 78 79 imbi12d ⊢q=cd→[˙q/p]˙ψ→ab=q↔[˙cd/p]˙ψ→ab=cd
81 77 80 syl5ibrcom ⊢X∈V∧a∈X∧b∈X∧χ∧∀x∈X∀y∈Xθ→xy=ab∧c∈X∧d∈X→q=cd→[˙q/p]˙ψ→ab=q
82 81 rexlimdvva ⊢X∈V∧a∈X∧b∈X∧χ∧∀x∈X∀y∈Xθ→xy=ab→∃c∈X∃d∈Xq=cd→[˙q/p]˙ψ→ab=q
83 sprel ⊢q∈Pairs⁡X→∃c∈X∃d∈Xq=cd
84 82 83 impel ⊢X∈V∧a∈X∧b∈X∧χ∧∀x∈X∀y∈Xθ→xy=ab∧q∈Pairs⁡X→[˙q/p]˙ψ→ab=q
85 84 ralrimiva ⊢X∈V∧a∈X∧b∈X∧χ∧∀x∈X∀y∈Xθ→xy=ab→∀q∈Pairs⁡X[˙q/p]˙ψ→ab=q
86 nfv ⊢Ⅎpχ
87 nfcv ⊢Ⅎ_pPairs⁡X
88 nfv ⊢Ⅎpab=q
89 3 88 nfim ⊢Ⅎp[˙q/p]˙ψ→ab=q
90 87 89 nfralw ⊢Ⅎp∀q∈Pairs⁡X[˙q/p]˙ψ→ab=q
91 86 90 nfan ⊢Ⅎpχ∧∀q∈Pairs⁡X[˙q/p]˙ψ→ab=q
92 eqeq1 ⊢p=ab→p=q↔ab=q
93 92 imbi2d ⊢p=ab→[˙q/p]˙ψ→p=q↔[˙q/p]˙ψ→ab=q
94 93 ralbidv ⊢p=ab→∀q∈Pairs⁡X[˙q/p]˙ψ→p=q↔∀q∈Pairs⁡X[˙q/p]˙ψ→ab=q
95 1 94 anbi12d ⊢p=ab→ψ∧∀q∈Pairs⁡X[˙q/p]˙ψ→p=q↔χ∧∀q∈Pairs⁡X[˙q/p]˙ψ→ab=q
96 91 95 rspce ⊢ab∈Pairs⁡X∧χ∧∀q∈Pairs⁡X[˙q/p]˙ψ→ab=q→∃p∈Pairs⁡Xψ∧∀q∈Pairs⁡X[˙q/p]˙ψ→p=q
97 49 50 85 96 syl12anc ⊢X∈V∧a∈X∧b∈X∧χ∧∀x∈X∀y∈Xθ→xy=ab→∃p∈Pairs⁡Xψ∧∀q∈Pairs⁡X[˙q/p]˙ψ→p=q
98 97 ex ⊢X∈V∧a∈X∧b∈X→χ∧∀x∈X∀y∈Xθ→xy=ab→∃p∈Pairs⁡Xψ∧∀q∈Pairs⁡X[˙q/p]˙ψ→p=q
99 98 rexlimdvva ⊢X∈V→∃a∈X∃b∈Xχ∧∀x∈X∀y∈Xθ→xy=ab→∃p∈Pairs⁡Xψ∧∀q∈Pairs⁡X[˙q/p]˙ψ→p=q
100 47 99 impbid ⊢X∈V→∃p∈Pairs⁡Xψ∧∀q∈Pairs⁡X[˙q/p]˙ψ→p=q↔∃a∈X∃b∈Xχ∧∀x∈X∀y∈Xθ→xy=ab
101 7 100 bitrid ⊢X∈V→∃!p∈Pairs⁡Xψ↔∃a∈X∃b∈Xχ∧∀x∈X∀y∈Xθ→xy=ab