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 ] ph -> ( E! p e. ( X X. X ) E. a E. b ( p = <. a , b >. /\ ph ) -> E. a E. b ( a = b /\ ph ) ) )

Proof

Step Hyp Ref Expression
1 eqeq1 
 |-  ( p = <. x , y >. -> ( p = <. a , b >. <-> <. x , y >. = <. a , b >. ) )
2 1 anbi1d 
 |-  ( p = <. x , y >. -> ( ( p = <. a , b >. /\ ph ) <-> ( <. x , y >. = <. a , b >. /\ ph ) ) )
3 2 2exbidv 
 |-  ( p = <. x , y >. -> ( E. a E. b ( p = <. a , b >. /\ ph ) <-> E. a E. b ( <. x , y >. = <. a , b >. /\ ph ) ) )
4 eqeq1 
 |-  ( p = <. v , w >. -> ( p = <. a , b >. <-> <. v , w >. = <. a , b >. ) )
5 4 anbi1d 
 |-  ( p = <. v , w >. -> ( ( p = <. a , b >. /\ ph ) <-> ( <. v , w >. = <. a , b >. /\ ph ) ) )
6 5 2exbidv 
 |-  ( p = <. v , w >. -> ( E. a E. b ( p = <. a , b >. /\ ph ) <-> E. a E. b ( <. v , w >. = <. a , b >. /\ ph ) ) )
7 3 6 reuop 
 |-  ( E! p e. ( X X. X ) E. a E. b ( p = <. a , b >. /\ ph ) <-> E. x e. X E. y e. X ( E. a E. b ( <. x , y >. = <. a , b >. /\ ph ) /\ A. v e. X A. w e. X ( E. a E. b ( <. v , w >. = <. a , b >. /\ ph ) -> <. v , w >. = <. x , y >. ) ) )
8 nfich1 
 |-  F/ a [ a <> b ] ph
9 nfv 
 |-  F/ a ( x e. X /\ y e. X )
10 8 9 nfan 
 |-  F/ a ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) )
11 nfcv 
 |-  F/_ a X
12 nfe1 
 |-  F/ a E. a E. b ( <. v , w >. = <. a , b >. /\ ph )
13 nfv 
 |-  F/ a <. v , w >. = <. x , y >.
14 12 13 nfim 
 |-  F/ a ( E. a E. b ( <. v , w >. = <. a , b >. /\ ph ) -> <. v , w >. = <. x , y >. )
15 11 14 nfralw 
 |-  F/ a A. w e. X ( E. a E. b ( <. v , w >. = <. a , b >. /\ ph ) -> <. v , w >. = <. x , y >. )
16 11 15 nfralw 
 |-  F/ a A. v e. X A. w e. X ( E. a E. b ( <. v , w >. = <. a , b >. /\ ph ) -> <. v , w >. = <. x , y >. )
17 nfe1 
 |-  F/ a E. a E. b ( a = b /\ ph )
18 16 17 nfim 
 |-  F/ a ( A. v e. X A. w e. X ( E. a E. b ( <. v , w >. = <. a , b >. /\ ph ) -> <. v , w >. = <. x , y >. ) -> E. a E. b ( a = b /\ ph ) )
19 nfich2 
 |-  F/ b [ a <> b ] ph
20 nfv 
 |-  F/ b ( x e. X /\ y e. X )
21 19 20 nfan 
 |-  F/ b ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) )
22 nfcv 
 |-  F/_ b X
23 nfe1 
 |-  F/ b E. b ( <. v , w >. = <. a , b >. /\ ph )
24 23 nfex 
 |-  F/ b E. a E. b ( <. v , w >. = <. a , b >. /\ ph )
25 nfv 
 |-  F/ b <. v , w >. = <. x , y >.
26 24 25 nfim 
 |-  F/ b ( E. a E. b ( <. v , w >. = <. a , b >. /\ ph ) -> <. v , w >. = <. x , y >. )
27 22 26 nfralw 
 |-  F/ b A. w e. X ( E. a E. b ( <. v , w >. = <. a , b >. /\ ph ) -> <. v , w >. = <. x , y >. )
28 22 27 nfralw 
 |-  F/ b A. v e. X A. w e. X ( E. a E. b ( <. v , w >. = <. a , b >. /\ ph ) -> <. v , w >. = <. x , y >. )
29 nfe1 
 |-  F/ b E. b ( a = b /\ ph )
30 29 nfex 
 |-  F/ b E. a E. b ( a = b /\ ph )
31 28 30 nfim 
 |-  F/ b ( A. v e. X A. w e. X ( E. a E. b ( <. v , w >. = <. a , b >. /\ ph ) -> <. v , w >. = <. x , y >. ) -> E. a E. b ( a = b /\ ph ) )
32 opeq12 
 |-  ( ( v = y /\ w = x ) -> <. v , w >. = <. y , x >. )
33 32 eqeq1d 
 |-  ( ( v = y /\ w = x ) -> ( <. v , w >. = <. a , b >. <-> <. y , x >. = <. a , b >. ) )
34 33 anbi1d 
 |-  ( ( v = y /\ w = x ) -> ( ( <. v , w >. = <. a , b >. /\ ph ) <-> ( <. y , x >. = <. a , b >. /\ ph ) ) )
35 34 2exbidv 
 |-  ( ( v = y /\ w = x ) -> ( E. a E. b ( <. v , w >. = <. a , b >. /\ ph ) <-> E. a E. b ( <. y , x >. = <. a , b >. /\ ph ) ) )
36 32 eqeq1d 
 |-  ( ( v = y /\ w = x ) -> ( <. v , w >. = <. x , y >. <-> <. y , x >. = <. x , y >. ) )
37 35 36 imbi12d 
 |-  ( ( v = y /\ w = x ) -> ( ( E. a E. b ( <. v , w >. = <. a , b >. /\ ph ) -> <. v , w >. = <. x , y >. ) <-> ( E. a E. b ( <. y , x >. = <. a , b >. /\ ph ) -> <. y , x >. = <. x , y >. ) ) )
38 37 rspc2gv 
 |-  ( ( y e. X /\ x e. X ) -> ( A. v e. X A. w e. X ( E. a E. b ( <. v , w >. = <. a , b >. /\ ph ) -> <. v , w >. = <. x , y >. ) -> ( E. a E. b ( <. y , x >. = <. a , b >. /\ ph ) -> <. y , x >. = <. x , y >. ) ) )
39 38 ancoms 
 |-  ( ( x e. X /\ y e. X ) -> ( A. v e. X A. w e. X ( E. a E. b ( <. v , w >. = <. a , b >. /\ ph ) -> <. v , w >. = <. x , y >. ) -> ( E. a E. b ( <. y , x >. = <. a , b >. /\ ph ) -> <. y , x >. = <. x , y >. ) ) )
40 39 adantl 
 |-  ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) -> ( A. v e. X A. w e. X ( E. a E. b ( <. v , w >. = <. a , b >. /\ ph ) -> <. v , w >. = <. x , y >. ) -> ( E. a E. b ( <. y , x >. = <. a , b >. /\ ph ) -> <. y , x >. = <. x , y >. ) ) )
41 simprr 
 |-  ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) -> y e. X )
42 41 adantr 
 |-  ( ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) /\ ( <. x , y >. = <. a , b >. /\ ph ) ) -> y e. X )
43 simpl 
 |-  ( ( x e. X /\ y e. X ) -> x e. X )
44 43 adantl 
 |-  ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) -> x e. X )
45 44 adantr 
 |-  ( ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) /\ ( <. x , y >. = <. a , b >. /\ ph ) ) -> x e. X )
46 eqidd 
 |-  ( ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) /\ ( <. x , y >. = <. a , b >. /\ ph ) ) -> <. y , x >. = <. y , x >. )
47 vex 
 |-  x e. _V
48 vex 
 |-  y e. _V
49 47 48 opth 
 |-  ( <. x , y >. = <. a , b >. <-> ( x = a /\ y = b ) )
50 sbceq1a 
 |-  ( b = y -> ( ph <-> [. y / b ]. ph ) )
51 50 equcoms 
 |-  ( y = b -> ( ph <-> [. y / b ]. ph ) )
52 sbceq1a 
 |-  ( a = x -> ( [. y / b ]. ph <-> [. x / a ]. [. y / b ]. ph ) )
53 52 equcoms 
 |-  ( x = a -> ( [. y / b ]. ph <-> [. x / a ]. [. y / b ]. ph ) )
54 51 53 sylan9bbr 
 |-  ( ( x = a /\ y = b ) -> ( ph <-> [. x / a ]. [. y / b ]. ph ) )
55 dfich2 
 |-  ( [ a <> b ] ph <-> A. x A. y ( [ x / a ] [ y / b ] ph <-> [ y / a ] [ x / b ] ph ) )
56 2sp 
 |-  ( A. x A. y ( [ x / a ] [ y / b ] ph <-> [ y / a ] [ x / b ] ph ) -> ( [ x / a ] [ y / b ] ph <-> [ y / a ] [ x / b ] ph ) )
57 sbsbc 
 |-  ( [ y / b ] ph <-> [. y / b ]. ph )
58 57 sbbii 
 |-  ( [ x / a ] [ y / b ] ph <-> [ x / a ] [. y / b ]. ph )
59 sbsbc 
 |-  ( [ x / a ] [. y / b ]. ph <-> [. x / a ]. [. y / b ]. ph )
60 58 59 bitri 
 |-  ( [ x / a ] [ y / b ] ph <-> [. x / a ]. [. y / b ]. ph )
61 sbsbc 
 |-  ( [ x / b ] ph <-> [. x / b ]. ph )
62 61 sbbii 
 |-  ( [ y / a ] [ x / b ] ph <-> [ y / a ] [. x / b ]. ph )
63 sbsbc 
 |-  ( [ y / a ] [. x / b ]. ph <-> [. y / a ]. [. x / b ]. ph )
64 62 63 bitri 
 |-  ( [ y / a ] [ x / b ] ph <-> [. y / a ]. [. x / b ]. ph )
65 56 60 64 3bitr3g 
 |-  ( A. x A. y ( [ x / a ] [ y / b ] ph <-> [ y / a ] [ x / b ] ph ) -> ( [. x / a ]. [. y / b ]. ph <-> [. y / a ]. [. x / b ]. ph ) )
66 55 65 sylbi 
 |-  ( [ a <> b ] ph -> ( [. x / a ]. [. y / b ]. ph <-> [. y / a ]. [. x / b ]. ph ) )
67 66 biimpd 
 |-  ( [ a <> b ] ph -> ( [. x / a ]. [. y / b ]. ph -> [. y / a ]. [. x / b ]. ph ) )
68 67 adantr 
 |-  ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) -> ( [. x / a ]. [. y / b ]. ph -> [. y / a ]. [. x / b ]. ph ) )
69 68 com12 
 |-  ( [. x / a ]. [. y / b ]. ph -> ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) -> [. y / a ]. [. x / b ]. ph ) )
70 54 69 syl6bi 
 |-  ( ( x = a /\ y = b ) -> ( ph -> ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) -> [. y / a ]. [. x / b ]. ph ) ) )
71 49 70 sylbi 
 |-  ( <. x , y >. = <. a , b >. -> ( ph -> ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) -> [. y / a ]. [. x / b ]. ph ) ) )
72 71 imp 
 |-  ( ( <. x , y >. = <. a , b >. /\ ph ) -> ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) -> [. y / a ]. [. x / b ]. ph ) )
73 72 impcom 
 |-  ( ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) /\ ( <. x , y >. = <. a , b >. /\ ph ) ) -> [. y / a ]. [. x / b ]. ph )
74 sbccom 
 |-  ( [. x / b ]. [. y / a ]. ph <-> [. y / a ]. [. x / b ]. ph )
75 73 74 sylibr 
 |-  ( ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) /\ ( <. x , y >. = <. a , b >. /\ ph ) ) -> [. x / b ]. [. y / a ]. ph )
76 46 75 jca 
 |-  ( ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) /\ ( <. x , y >. = <. a , b >. /\ ph ) ) -> ( <. y , x >. = <. y , x >. /\ [. x / b ]. [. y / a ]. ph ) )
77 nfcv 
 |-  F/_ b x
78 nfv 
 |-  F/ b <. y , x >. = <. y , x >.
79 nfsbc1v 
 |-  F/ b [. x / b ]. [. y / a ]. ph
80 78 79 nfan 
 |-  F/ b ( <. y , x >. = <. y , x >. /\ [. x / b ]. [. y / a ]. ph )
81 opeq2 
 |-  ( b = x -> <. y , b >. = <. y , x >. )
82 81 eqeq2d 
 |-  ( b = x -> ( <. y , x >. = <. y , b >. <-> <. y , x >. = <. y , x >. ) )
83 sbceq1a 
 |-  ( b = x -> ( [. y / a ]. ph <-> [. x / b ]. [. y / a ]. ph ) )
84 82 83 anbi12d 
 |-  ( b = x -> ( ( <. y , x >. = <. y , b >. /\ [. y / a ]. ph ) <-> ( <. y , x >. = <. y , x >. /\ [. x / b ]. [. y / a ]. ph ) ) )
85 77 80 84 spcegf 
 |-  ( x e. X -> ( ( <. y , x >. = <. y , x >. /\ [. x / b ]. [. y / a ]. ph ) -> E. b ( <. y , x >. = <. y , b >. /\ [. y / a ]. ph ) ) )
86 45 76 85 sylc 
 |-  ( ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) /\ ( <. x , y >. = <. a , b >. /\ ph ) ) -> E. b ( <. y , x >. = <. y , b >. /\ [. y / a ]. ph ) )
87 nfcv 
 |-  F/_ a y
88 nfv 
 |-  F/ a <. y , x >. = <. y , b >.
89 nfsbc1v 
 |-  F/ a [. y / a ]. ph
90 88 89 nfan 
 |-  F/ a ( <. y , x >. = <. y , b >. /\ [. y / a ]. ph )
91 90 nfex 
 |-  F/ a E. b ( <. y , x >. = <. y , b >. /\ [. y / a ]. ph )
92 opeq1 
 |-  ( a = y -> <. a , b >. = <. y , b >. )
93 92 eqeq2d 
 |-  ( a = y -> ( <. y , x >. = <. a , b >. <-> <. y , x >. = <. y , b >. ) )
94 sbceq1a 
 |-  ( a = y -> ( ph <-> [. y / a ]. ph ) )
95 93 94 anbi12d 
 |-  ( a = y -> ( ( <. y , x >. = <. a , b >. /\ ph ) <-> ( <. y , x >. = <. y , b >. /\ [. y / a ]. ph ) ) )
96 95 exbidv 
 |-  ( a = y -> ( E. b ( <. y , x >. = <. a , b >. /\ ph ) <-> E. b ( <. y , x >. = <. y , b >. /\ [. y / a ]. ph ) ) )
97 87 91 96 spcegf 
 |-  ( y e. X -> ( E. b ( <. y , x >. = <. y , b >. /\ [. y / a ]. ph ) -> E. a E. b ( <. y , x >. = <. a , b >. /\ ph ) ) )
98 42 86 97 sylc 
 |-  ( ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) /\ ( <. x , y >. = <. a , b >. /\ ph ) ) -> E. a E. b ( <. y , x >. = <. a , b >. /\ ph ) )
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 ) ) /\ ph ) -> ( a = b /\ ph ) )
105 104 exp31 
 |-  ( y = x -> ( ( x = a /\ y = b ) -> ( ph -> ( a = b /\ ph ) ) ) )
106 49 105 syl5bi 
 |-  ( y = x -> ( <. x , y >. = <. a , b >. -> ( ph -> ( a = b /\ ph ) ) ) )
107 106 impd 
 |-  ( y = x -> ( ( <. x , y >. = <. a , b >. /\ ph ) -> ( a = b /\ ph ) ) )
108 48 47 opth1 
 |-  ( <. y , x >. = <. x , y >. -> y = x )
109 107 108 syl11 
 |-  ( ( <. x , y >. = <. a , b >. /\ ph ) -> ( <. y , x >. = <. x , y >. -> ( a = b /\ ph ) ) )
110 109 adantl 
 |-  ( ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) /\ ( <. x , y >. = <. a , b >. /\ ph ) ) -> ( <. y , x >. = <. x , y >. -> ( a = b /\ ph ) ) )
111 110 imp 
 |-  ( ( ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) /\ ( <. x , y >. = <. a , b >. /\ ph ) ) /\ <. y , x >. = <. x , y >. ) -> ( a = b /\ ph ) )
112 111 19.8ad 
 |-  ( ( ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) /\ ( <. x , y >. = <. a , b >. /\ ph ) ) /\ <. y , x >. = <. x , y >. ) -> E. b ( a = b /\ ph ) )
113 112 19.8ad 
 |-  ( ( ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) /\ ( <. x , y >. = <. a , b >. /\ ph ) ) /\ <. y , x >. = <. x , y >. ) -> E. a E. b ( a = b /\ ph ) )
114 113 ex 
 |-  ( ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) /\ ( <. x , y >. = <. a , b >. /\ ph ) ) -> ( <. y , x >. = <. x , y >. -> E. a E. b ( a = b /\ ph ) ) )
115 98 114 embantd 
 |-  ( ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) /\ ( <. x , y >. = <. a , b >. /\ ph ) ) -> ( ( E. a E. b ( <. y , x >. = <. a , b >. /\ ph ) -> <. y , x >. = <. x , y >. ) -> E. a E. b ( a = b /\ ph ) ) )
116 115 ex 
 |-  ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) -> ( ( <. x , y >. = <. a , b >. /\ ph ) -> ( ( E. a E. b ( <. y , x >. = <. a , b >. /\ ph ) -> <. y , x >. = <. x , y >. ) -> E. a E. b ( a = b /\ ph ) ) ) )
117 40 116 syl5d 
 |-  ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) -> ( ( <. x , y >. = <. a , b >. /\ ph ) -> ( A. v e. X A. w e. X ( E. a E. b ( <. v , w >. = <. a , b >. /\ ph ) -> <. v , w >. = <. x , y >. ) -> E. a E. b ( a = b /\ ph ) ) ) )
118 21 31 117 exlimd 
 |-  ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) -> ( E. b ( <. x , y >. = <. a , b >. /\ ph ) -> ( A. v e. X A. w e. X ( E. a E. b ( <. v , w >. = <. a , b >. /\ ph ) -> <. v , w >. = <. x , y >. ) -> E. a E. b ( a = b /\ ph ) ) ) )
119 10 18 118 exlimd 
 |-  ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) -> ( E. a E. b ( <. x , y >. = <. a , b >. /\ ph ) -> ( A. v e. X A. w e. X ( E. a E. b ( <. v , w >. = <. a , b >. /\ ph ) -> <. v , w >. = <. x , y >. ) -> E. a E. b ( a = b /\ ph ) ) ) )
120 119 impd 
 |-  ( ( [ a <> b ] ph /\ ( x e. X /\ y e. X ) ) -> ( ( E. a E. b ( <. x , y >. = <. a , b >. /\ ph ) /\ A. v e. X A. w e. X ( E. a E. b ( <. v , w >. = <. a , b >. /\ ph ) -> <. v , w >. = <. x , y >. ) ) -> E. a E. b ( a = b /\ ph ) ) )
121 120 rexlimdvva 
 |-  ( [ a <> b ] ph -> ( E. x e. X E. y e. X ( E. a E. b ( <. x , y >. = <. a , b >. /\ ph ) /\ A. v e. X A. w e. X ( E. a E. b ( <. v , w >. = <. a , b >. /\ ph ) -> <. v , w >. = <. x , y >. ) ) -> E. a E. b ( a = b /\ ph ) ) )
122 7 121 syl5bi 
 |-  ( [ a <> b ] ph -> ( E! p e. ( X X. X ) E. a E. b ( p = <. a , b >. /\ ph ) -> E. a E. b ( a = b /\ ph ) ) )