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

Proof

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