Metamath Proof Explorer

Theorem ichreuopeq

Description: If the setvar variables are interchangeable in a wff, and there is a unique ordered pair fulfilling the wff, then both setvar variables must be equal. (Contributed by AV, 28-Aug-2023)

Ref Expression
Assertion ichreuopeq ⊢a⇄bφ→∃!p∈X×X∃a∃bp=ab∧φ→∃a∃ba=b∧φ

Proof

Step Hyp Ref Expression
1 eqeq1 ⊢p=xy→p=ab↔xy=ab
2 1 anbi1d ⊢p=xy→p=ab∧φ↔xy=ab∧φ
3 2 2exbidv ⊢p=xy→∃a∃bp=ab∧φ↔∃a∃bxy=ab∧φ
4 eqeq1 ⊢p=vw→p=ab↔vw=ab
5 4 anbi1d ⊢p=vw→p=ab∧φ↔vw=ab∧φ
6 5 2exbidv ⊢p=vw→∃a∃bp=ab∧φ↔∃a∃bvw=ab∧φ
7 3 6 reuop ⊢∃!p∈X×X∃a∃bp=ab∧φ↔∃x∈X∃y∈X∃a∃bxy=ab∧φ∧∀v∈X∀w∈X∃a∃bvw=ab∧φ→vw=xy
8 nfich1 ⊢Ⅎaa⇄bφ
9 nfv ⊢Ⅎax∈X∧y∈X
10 8 9 nfan ⊢Ⅎaa⇄bφ∧x∈X∧y∈X
11 nfcv ⊢Ⅎ_aX
12 nfe1 ⊢Ⅎa∃a∃bvw=ab∧φ
13 nfv ⊢Ⅎavw=xy
14 12 13 nfim ⊢Ⅎa∃a∃bvw=ab∧φ→vw=xy
15 11 14 nfralw ⊢Ⅎa∀w∈X∃a∃bvw=ab∧φ→vw=xy
16 11 15 nfralw ⊢Ⅎa∀v∈X∀w∈X∃a∃bvw=ab∧φ→vw=xy
17 nfe1 ⊢Ⅎa∃a∃ba=b∧φ
18 16 17 nfim ⊢Ⅎa∀v∈X∀w∈X∃a∃bvw=ab∧φ→vw=xy→∃a∃ba=b∧φ
19 nfich2 ⊢Ⅎba⇄bφ
20 nfv ⊢Ⅎbx∈X∧y∈X
21 19 20 nfan ⊢Ⅎba⇄bφ∧x∈X∧y∈X
22 nfcv ⊢Ⅎ_bX
23 nfe1 ⊢Ⅎb∃bvw=ab∧φ
24 23 nfex ⊢Ⅎb∃a∃bvw=ab∧φ
25 nfv ⊢Ⅎbvw=xy
26 24 25 nfim ⊢Ⅎb∃a∃bvw=ab∧φ→vw=xy
27 22 26 nfralw ⊢Ⅎb∀w∈X∃a∃bvw=ab∧φ→vw=xy
28 22 27 nfralw ⊢Ⅎb∀v∈X∀w∈X∃a∃bvw=ab∧φ→vw=xy
29 nfe1 ⊢Ⅎb∃ba=b∧φ
30 29 nfex ⊢Ⅎb∃a∃ba=b∧φ
31 28 30 nfim ⊢Ⅎb∀v∈X∀w∈X∃a∃bvw=ab∧φ→vw=xy→∃a∃ba=b∧φ
32 opeq12 ⊢v=y∧w=x→vw=yx
33 32 eqeq1d ⊢v=y∧w=x→vw=ab↔yx=ab
34 33 anbi1d ⊢v=y∧w=x→vw=ab∧φ↔yx=ab∧φ
35 34 2exbidv ⊢v=y∧w=x→∃a∃bvw=ab∧φ↔∃a∃byx=ab∧φ
36 32 eqeq1d ⊢v=y∧w=x→vw=xy↔yx=xy
37 35 36 imbi12d ⊢v=y∧w=x→∃a∃bvw=ab∧φ→vw=xy↔∃a∃byx=ab∧φ→yx=xy
38 37 rspc2gv ⊢y∈X∧x∈X→∀v∈X∀w∈X∃a∃bvw=ab∧φ→vw=xy→∃a∃byx=ab∧φ→yx=xy
39 38 ancoms ⊢x∈X∧y∈X→∀v∈X∀w∈X∃a∃bvw=ab∧φ→vw=xy→∃a∃byx=ab∧φ→yx=xy
40 39 adantl ⊢a⇄bφ∧x∈X∧y∈X→∀v∈X∀w∈X∃a∃bvw=ab∧φ→vw=xy→∃a∃byx=ab∧φ→yx=xy
41 simprr ⊢a⇄bφ∧x∈X∧y∈X→y∈X
42 41 adantr ⊢a⇄bφ∧x∈X∧y∈X∧xy=ab∧φ→y∈X
43 simpl ⊢x∈X∧y∈X→x∈X
44 43 adantl ⊢a⇄bφ∧x∈X∧y∈X→x∈X
45 44 adantr ⊢a⇄bφ∧x∈X∧y∈X∧xy=ab∧φ→x∈X
46 eqidd ⊢a⇄bφ∧x∈X∧y∈X∧xy=ab∧φ→yx=yx
47 vex ⊢x∈V
48 vex ⊢y∈V
49 47 48 opth ⊢xy=ab↔x=a∧y=b
50 sbceq1a ⊢b=y→φ↔[˙y/b]˙φ
51 50 equcoms ⊢y=b→φ↔[˙y/b]˙φ
52 sbceq1a ⊢a=x→[˙y/b]˙φ↔[˙x/a]˙[˙y/b]˙φ
53 52 equcoms ⊢x=a→[˙y/b]˙φ↔[˙x/a]˙[˙y/b]˙φ
54 51 53 sylan9bbr ⊢x=a∧y=b→φ↔[˙x/a]˙[˙y/b]˙φ
55 dfich2 ⊢a⇄bφ↔∀x∀yxaybφ↔yaxbφ
56 2sp ⊢∀x∀yxaybφ↔yaxbφ→xaybφ↔yaxbφ
57 sbsbc ⊢ybφ↔[˙y/b]˙φ
58 57 sbbii ⊢xaybφ↔xa[˙y/b]˙φ
59 sbsbc ⊢xa[˙y/b]˙φ↔[˙x/a]˙[˙y/b]˙φ
60 58 59 bitri ⊢xaybφ↔[˙x/a]˙[˙y/b]˙φ
61 sbsbc ⊢xbφ↔[˙x/b]˙φ
62 61 sbbii ⊢yaxbφ↔ya[˙x/b]˙φ
63 sbsbc ⊢ya[˙x/b]˙φ↔[˙y/a]˙[˙x/b]˙φ
64 62 63 bitri ⊢yaxbφ↔[˙y/a]˙[˙x/b]˙φ
65 56 60 64 3bitr3g ⊢∀x∀yxaybφ↔yaxbφ→[˙x/a]˙[˙y/b]˙φ↔[˙y/a]˙[˙x/b]˙φ
66 55 65 sylbi ⊢a⇄bφ→[˙x/a]˙[˙y/b]˙φ↔[˙y/a]˙[˙x/b]˙φ
67 66 biimpd ⊢a⇄bφ→[˙x/a]˙[˙y/b]˙φ→[˙y/a]˙[˙x/b]˙φ
68 67 adantr ⊢a⇄bφ∧x∈X∧y∈X→[˙x/a]˙[˙y/b]˙φ→[˙y/a]˙[˙x/b]˙φ
69 68 com12 ⊢[˙x/a]˙[˙y/b]˙φ→a⇄bφ∧x∈X∧y∈X→[˙y/a]˙[˙x/b]˙φ
70 54 69 syl6bi ⊢x=a∧y=b→φ→a⇄bφ∧x∈X∧y∈X→[˙y/a]˙[˙x/b]˙φ
71 49 70 sylbi ⊢xy=ab→φ→a⇄bφ∧x∈X∧y∈X→[˙y/a]˙[˙x/b]˙φ
72 71 imp ⊢xy=ab∧φ→a⇄bφ∧x∈X∧y∈X→[˙y/a]˙[˙x/b]˙φ
73 72 impcom ⊢a⇄bφ∧x∈X∧y∈X∧xy=ab∧φ→[˙y/a]˙[˙x/b]˙φ
74 sbccom ⊢[˙x/b]˙[˙y/a]˙φ↔[˙y/a]˙[˙x/b]˙φ
75 73 74 sylibr ⊢a⇄bφ∧x∈X∧y∈X∧xy=ab∧φ→[˙x/b]˙[˙y/a]˙φ
76 46 75 jca ⊢a⇄bφ∧x∈X∧y∈X∧xy=ab∧φ→yx=yx∧[˙x/b]˙[˙y/a]˙φ
77 nfcv ⊢Ⅎ_bx
78 nfv ⊢Ⅎbyx=yx
79 nfsbc1v ⊢Ⅎb[˙x/b]˙[˙y/a]˙φ
80 78 79 nfan ⊢Ⅎbyx=yx∧[˙x/b]˙[˙y/a]˙φ
81 opeq2 ⊢b=x→yb=yx
82 81 eqeq2d ⊢b=x→yx=yb↔yx=yx
83 sbceq1a ⊢b=x→[˙y/a]˙φ↔[˙x/b]˙[˙y/a]˙φ
84 82 83 anbi12d ⊢b=x→yx=yb∧[˙y/a]˙φ↔yx=yx∧[˙x/b]˙[˙y/a]˙φ
85 77 80 84 spcegf ⊢x∈X→yx=yx∧[˙x/b]˙[˙y/a]˙φ→∃byx=yb∧[˙y/a]˙φ
86 45 76 85 sylc ⊢a⇄bφ∧x∈X∧y∈X∧xy=ab∧φ→∃byx=yb∧[˙y/a]˙φ
87 nfcv ⊢Ⅎ_ay
88 nfv ⊢Ⅎayx=yb
89 nfsbc1v ⊢Ⅎa[˙y/a]˙φ
90 88 89 nfan ⊢Ⅎayx=yb∧[˙y/a]˙φ
91 90 nfex ⊢Ⅎa∃byx=yb∧[˙y/a]˙φ
92 opeq1 ⊢a=y→ab=yb
93 92 eqeq2d ⊢a=y→yx=ab↔yx=yb
94 sbceq1a ⊢a=y→φ↔[˙y/a]˙φ
95 93 94 anbi12d ⊢a=y→yx=ab∧φ↔yx=yb∧[˙y/a]˙φ
96 95 exbidv ⊢a=y→∃byx=ab∧φ↔∃byx=yb∧[˙y/a]˙φ
97 87 91 96 spcegf ⊢y∈X→∃byx=yb∧[˙y/a]˙φ→∃a∃byx=ab∧φ
98 42 86 97 sylc ⊢a⇄bφ∧x∈X∧y∈X∧xy=ab∧φ→∃a∃byx=ab∧φ
99 simpl ⊢y=x∧x=a∧y=b→y=x
100 simprr ⊢y=x∧x=a∧y=b→y=b
101 simpl ⊢x=a∧y=b→x=a
102 101 adantl ⊢y=x∧x=a∧y=b→x=a
103 99 100 102 3eqtr3rd ⊢y=x∧x=a∧y=b→a=b
104 103 anim1i ⊢y=x∧x=a∧y=b∧φ→a=b∧φ
105 104 exp31 ⊢y=x→x=a∧y=b→φ→a=b∧φ
106 49 105 biimtrid ⊢y=x→xy=ab→φ→a=b∧φ
107 106 impd ⊢y=x→xy=ab∧φ→a=b∧φ
108 48 47 opth1 ⊢yx=xy→y=x
109 107 108 syl11 ⊢xy=ab∧φ→yx=xy→a=b∧φ
110 109 adantl ⊢a⇄bφ∧x∈X∧y∈X∧xy=ab∧φ→yx=xy→a=b∧φ
111 110 imp ⊢a⇄bφ∧x∈X∧y∈X∧xy=ab∧φ∧yx=xy→a=b∧φ
112 111 19.8ad ⊢a⇄bφ∧x∈X∧y∈X∧xy=ab∧φ∧yx=xy→∃ba=b∧φ
113 112 19.8ad ⊢a⇄bφ∧x∈X∧y∈X∧xy=ab∧φ∧yx=xy→∃a∃ba=b∧φ
114 113 ex ⊢a⇄bφ∧x∈X∧y∈X∧xy=ab∧φ→yx=xy→∃a∃ba=b∧φ
115 98 114 embantd ⊢a⇄bφ∧x∈X∧y∈X∧xy=ab∧φ→∃a∃byx=ab∧φ→yx=xy→∃a∃ba=b∧φ
116 115 ex ⊢a⇄bφ∧x∈X∧y∈X→xy=ab∧φ→∃a∃byx=ab∧φ→yx=xy→∃a∃ba=b∧φ
117 40 116 syl5d ⊢a⇄bφ∧x∈X∧y∈X→xy=ab∧φ→∀v∈X∀w∈X∃a∃bvw=ab∧φ→vw=xy→∃a∃ba=b∧φ
118 21 31 117 exlimd ⊢a⇄bφ∧x∈X∧y∈X→∃bxy=ab∧φ→∀v∈X∀w∈X∃a∃bvw=ab∧φ→vw=xy→∃a∃ba=b∧φ
119 10 18 118 exlimd ⊢a⇄bφ∧x∈X∧y∈X→∃a∃bxy=ab∧φ→∀v∈X∀w∈X∃a∃bvw=ab∧φ→vw=xy→∃a∃ba=b∧φ
120 119 impd ⊢a⇄bφ∧x∈X∧y∈X→∃a∃bxy=ab∧φ∧∀v∈X∀w∈X∃a∃bvw=ab∧φ→vw=xy→∃a∃ba=b∧φ
121 120 rexlimdvva ⊢a⇄bφ→∃x∈X∃y∈X∃a∃bxy=ab∧φ∧∀v∈X∀w∈X∃a∃bvw=ab∧φ→vw=xy→∃a∃ba=b∧φ
122 7 121 biimtrid ⊢a⇄bφ→∃!p∈X×X∃a∃bp=ab∧φ→∃a∃ba=b∧φ