Metamath Proof Explorer

Theorem mirimanofffr

Description: Relative version of mirimanofff (which corresponds to the case V = _V ). (Contributed by Adrian Ducourtial, 28-Oct-2026)

Ref Expression
Hypothesis mirimanofffr.1 
|- M = { x e. V | A. y ( x e. y -> E. z e. y ( z i^i y ) = (/) ) }
Assertion mirimanofffr 
|- M e/ V

Proof

Step Hyp Ref Expression
1 mirimanofffr.1 
 |-  M = { x e. V | A. y ( x e. y -> E. z e. y ( z i^i y ) = (/) ) }
2 pm3.24 
 |-  -. ( v e. M /\ -. v e. M )
3 ancom 
 |-  ( ( v e. M /\ -. v e. M ) <-> ( -. v e. M /\ v e. M ) )
4 2 3 mtbi 
 |-  -. ( -. v e. M /\ v e. M )
5 4 nex 
 |-  -. E. v ( -. v e. M /\ v e. M )
6 pm2.24 
 |-  ( M e. V -> ( -. M e. V -> -. A. y ( M e. y -> E. z e. y ( z i^i y ) = (/) ) ) )
7 idd 
 |-  ( M e. V -> ( -. A. y ( M e. y -> E. z e. y ( z i^i y ) = (/) ) -> -. A. y ( M e. y -> E. z e. y ( z i^i y ) = (/) ) ) )
8 snexg 
 |-  ( M e. V -> { M } e. _V )
9 snidg 
 |-  ( M e. V -> M e. { M } )
10 eleq1 
 |-  ( x = M -> ( x e. y <-> M e. y ) )
11 10 imbi1d 
 |-  ( x = M -> ( ( x e. y -> E. z e. y ( z i^i y ) = (/) ) <-> ( M e. y -> E. z e. y ( z i^i y ) = (/) ) ) )
12 11 albidv 
 |-  ( x = M -> ( A. y ( x e. y -> E. z e. y ( z i^i y ) = (/) ) <-> A. y ( M e. y -> E. z e. y ( z i^i y ) = (/) ) ) )
13 12 1 elrab2 
 |-  ( M e. M <-> ( M e. V /\ A. y ( M e. y -> E. z e. y ( z i^i y ) = (/) ) ) )
14 13 simprbi 
 |-  ( M e. M -> A. y ( M e. y -> E. z e. y ( z i^i y ) = (/) ) )
15 eleq2 
 |-  ( y = { M } -> ( M e. y <-> M e. { M } ) )
16 ineq2 
 |-  ( y = { M } -> ( z i^i y ) = ( z i^i { M } ) )
17 16 eqeq1d 
 |-  ( y = { M } -> ( ( z i^i y ) = (/) <-> ( z i^i { M } ) = (/) ) )
18 17 rexeqbi1dv 
 |-  ( y = { M } -> ( E. z e. y ( z i^i y ) = (/) <-> E. z e. { M } ( z i^i { M } ) = (/) ) )
19 15 18 imbi12d 
 |-  ( y = { M } -> ( ( M e. y -> E. z e. y ( z i^i y ) = (/) ) <-> ( M e. { M } -> E. z e. { M } ( z i^i { M } ) = (/) ) ) )
20 19 spcgv 
 |-  ( { M } e. _V -> ( A. y ( M e. y -> E. z e. y ( z i^i y ) = (/) ) -> ( M e. { M } -> E. z e. { M } ( z i^i { M } ) = (/) ) ) )
21 14 20 syl5 
 |-  ( { M } e. _V -> ( M e. M -> ( M e. { M } -> E. z e. { M } ( z i^i { M } ) = (/) ) ) )
22 21 com23 
 |-  ( { M } e. _V -> ( M e. { M } -> ( M e. M -> E. z e. { M } ( z i^i { M } ) = (/) ) ) )
23 8 9 22 sylc 
 |-  ( M e. V -> ( M e. M -> E. z e. { M } ( z i^i { M } ) = (/) ) )
24 elsn2g 
 |-  ( M e. V -> ( z e. { M } <-> z = M ) )
25 ineq1 
 |-  ( z = M -> ( z i^i { M } ) = ( M i^i { M } ) )
26 25 eqeq1d 
 |-  ( z = M -> ( ( z i^i { M } ) = (/) <-> ( M i^i { M } ) = (/) ) )
27 24 26 biimtrdi 
 |-  ( M e. V -> ( z e. { M } -> ( ( z i^i { M } ) = (/) <-> ( M i^i { M } ) = (/) ) ) )
28 27 imp 
 |-  ( ( M e. V /\ z e. { M } ) -> ( ( z i^i { M } ) = (/) <-> ( M i^i { M } ) = (/) ) )
29 disjr 
 |-  ( ( M i^i { M } ) = (/) <-> A. w e. { M } -. w e. M )
30 28 29 bitrdi 
 |-  ( ( M e. V /\ z e. { M } ) -> ( ( z i^i { M } ) = (/) <-> A. w e. { M } -. w e. M ) )
31 eleq1 
 |-  ( w = M -> ( w e. M <-> M e. M ) )
32 31 notbid 
 |-  ( w = M -> ( -. w e. M <-> -. M e. M ) )
33 32 rspcv 
 |-  ( M e. { M } -> ( A. w e. { M } -. w e. M -> -. M e. M ) )
34 9 33 syl 
 |-  ( M e. V -> ( A. w e. { M } -. w e. M -> -. M e. M ) )
35 34 adantr 
 |-  ( ( M e. V /\ z e. { M } ) -> ( A. w e. { M } -. w e. M -> -. M e. M ) )
36 30 35 sylbid 
 |-  ( ( M e. V /\ z e. { M } ) -> ( ( z i^i { M } ) = (/) -> -. M e. M ) )
37 36 rexlimdva 
 |-  ( M e. V -> ( E. z e. { M } ( z i^i { M } ) = (/) -> -. M e. M ) )
38 23 37 syld 
 |-  ( M e. V -> ( M e. M -> -. M e. M ) )
39 38 pm2.01d 
 |-  ( M e. V -> -. M e. M )
40 13 notbii 
 |-  ( -. M e. M <-> -. ( M e. V /\ A. y ( M e. y -> E. z e. y ( z i^i y ) = (/) ) ) )
41 39 40 sylib 
 |-  ( M e. V -> -. ( M e. V /\ A. y ( M e. y -> E. z e. y ( z i^i y ) = (/) ) ) )
42 ianor 
 |-  ( -. ( M e. V /\ A. y ( M e. y -> E. z e. y ( z i^i y ) = (/) ) ) <-> ( -. M e. V \/ -. A. y ( M e. y -> E. z e. y ( z i^i y ) = (/) ) ) )
43 41 42 sylib 
 |-  ( M e. V -> ( -. M e. V \/ -. A. y ( M e. y -> E. z e. y ( z i^i y ) = (/) ) ) )
44 6 7 43 mpjaod 
 |-  ( M e. V -> -. A. y ( M e. y -> E. z e. y ( z i^i y ) = (/) ) )
45 exanali 
 |-  ( E. y ( M e. y /\ -. E. z e. y ( z i^i y ) = (/) ) <-> -. A. y ( M e. y -> E. z e. y ( z i^i y ) = (/) ) )
46 44 45 sylibr 
 |-  ( M e. V -> E. y ( M e. y /\ -. E. z e. y ( z i^i y ) = (/) ) )
47 df-rex 
 |-  ( E. z e. y ( z i^i y ) = (/) <-> E. z ( z e. y /\ ( z i^i y ) = (/) ) )
48 47 notbii 
 |-  ( -. E. z e. y ( z i^i y ) = (/) <-> -. E. z ( z e. y /\ ( z i^i y ) = (/) ) )
49 alnex 
 |-  ( A. z -. ( z e. y /\ ( z i^i y ) = (/) ) <-> -. E. z ( z e. y /\ ( z i^i y ) = (/) ) )
50 ianor 
 |-  ( -. ( z e. y /\ ( z i^i y ) = (/) ) <-> ( -. z e. y \/ -. ( z i^i y ) = (/) ) )
51 imor 
 |-  ( ( z e. y -> -. ( z i^i y ) = (/) ) <-> ( -. z e. y \/ -. ( z i^i y ) = (/) ) )
52 50 51 bitr4i 
 |-  ( -. ( z e. y /\ ( z i^i y ) = (/) ) <-> ( z e. y -> -. ( z i^i y ) = (/) ) )
53 52 albii 
 |-  ( A. z -. ( z e. y /\ ( z i^i y ) = (/) ) <-> A. z ( z e. y -> -. ( z i^i y ) = (/) ) )
54 48 49 53 3bitr2i 
 |-  ( -. E. z e. y ( z i^i y ) = (/) <-> A. z ( z e. y -> -. ( z i^i y ) = (/) ) )
55 df-ral 
 |-  ( A. z e. y -. ( z i^i y ) = (/) <-> A. z ( z e. y -> -. ( z i^i y ) = (/) ) )
56 df-ral 
 |-  ( A. w e. y -. w e. z <-> A. w ( w e. y -> -. w e. z ) )
57 56 notbii 
 |-  ( -. A. w e. y -. w e. z <-> -. A. w ( w e. y -> -. w e. z ) )
58 disjr 
 |-  ( ( z i^i y ) = (/) <-> A. w e. y -. w e. z )
59 57 58 xchnxbir 
 |-  ( -. ( z i^i y ) = (/) <-> -. A. w ( w e. y -> -. w e. z ) )
60 exnal 
 |-  ( E. w -. ( w e. y -> -. w e. z ) <-> -. A. w ( w e. y -> -. w e. z ) )
61 pm4.63 
 |-  ( -. ( w e. y -> -. w e. z ) <-> ( w e. y /\ w e. z ) )
62 61 exbii 
 |-  ( E. w -. ( w e. y -> -. w e. z ) <-> E. w ( w e. y /\ w e. z ) )
63 59 60 62 3bitr2i 
 |-  ( -. ( z i^i y ) = (/) <-> E. w ( w e. y /\ w e. z ) )
64 df-rex 
 |-  ( E. w e. y w e. z <-> E. w ( w e. y /\ w e. z ) )
65 63 64 bitr4i 
 |-  ( -. ( z i^i y ) = (/) <-> E. w e. y w e. z )
66 65 ralbii 
 |-  ( A. z e. y -. ( z i^i y ) = (/) <-> A. z e. y E. w e. y w e. z )
67 54 55 66 3bitr2i 
 |-  ( -. E. z e. y ( z i^i y ) = (/) <-> A. z e. y E. w e. y w e. z )
68 67 anbi2i 
 |-  ( ( M e. y /\ -. E. z e. y ( z i^i y ) = (/) ) <-> ( M e. y /\ A. z e. y E. w e. y w e. z ) )
69 68 exbii 
 |-  ( E. y ( M e. y /\ -. E. z e. y ( z i^i y ) = (/) ) <-> E. y ( M e. y /\ A. z e. y E. w e. y w e. z ) )
70 46 69 sylib 
 |-  ( M e. V -> E. y ( M e. y /\ A. z e. y E. w e. y w e. z ) )
71 eleq2w2 
 |-  ( z = M -> ( w e. z <-> w e. M ) )
72 71 rexbidv 
 |-  ( z = M -> ( E. w e. y w e. z <-> E. w e. y w e. M ) )
73 72 rspcva 
 |-  ( ( M e. y /\ A. z e. y E. w e. y w e. z ) -> E. w e. y w e. M )
74 73 anim2i 
 |-  ( ( A. z e. y E. w e. y w e. z /\ ( M e. y /\ A. z e. y E. w e. y w e. z ) ) -> ( A. z e. y E. w e. y w e. z /\ E. w e. y w e. M ) )
75 74 anabss7 
 |-  ( ( M e. y /\ A. z e. y E. w e. y w e. z ) -> ( A. z e. y E. w e. y w e. z /\ E. w e. y w e. M ) )
76 75 eximi 
 |-  ( E. y ( M e. y /\ A. z e. y E. w e. y w e. z ) -> E. y ( A. z e. y E. w e. y w e. z /\ E. w e. y w e. M ) )
77 70 76 syl 
 |-  ( M e. V -> E. y ( A. z e. y E. w e. y w e. z /\ E. w e. y w e. M ) )
78 eleq1w 
 |-  ( w = v -> ( w e. M <-> v e. M ) )
79 78 cbvrexvw 
 |-  ( E. w e. y w e. M <-> E. v e. y v e. M )
80 79 anbi2i 
 |-  ( ( A. z e. y E. w e. y w e. z /\ E. w e. y w e. M ) <-> ( A. z e. y E. w e. y w e. z /\ E. v e. y v e. M ) )
81 80 exbii 
 |-  ( E. y ( A. z e. y E. w e. y w e. z /\ E. w e. y w e. M ) <-> E. y ( A. z e. y E. w e. y w e. z /\ E. v e. y v e. M ) )
82 77 81 sylib 
 |-  ( M e. V -> E. y ( A. z e. y E. w e. y w e. z /\ E. v e. y v e. M ) )
83 r19.41v 
 |-  ( E. v e. y ( v e. M /\ A. z e. y E. w e. y w e. z ) <-> ( E. v e. y v e. M /\ A. z e. y E. w e. y w e. z ) )
84 83 biancomi 
 |-  ( E. v e. y ( v e. M /\ A. z e. y E. w e. y w e. z ) <-> ( A. z e. y E. w e. y w e. z /\ E. v e. y v e. M ) )
85 84 exbii 
 |-  ( E. y E. v e. y ( v e. M /\ A. z e. y E. w e. y w e. z ) <-> E. y ( A. z e. y E. w e. y w e. z /\ E. v e. y v e. M ) )
86 82 85 sylibr 
 |-  ( M e. V -> E. y E. v e. y ( v e. M /\ A. z e. y E. w e. y w e. z ) )
87 df-rex 
 |-  ( E. v e. y ( v e. M /\ A. z e. y E. w e. y w e. z ) <-> E. v ( v e. y /\ ( v e. M /\ A. z e. y E. w e. y w e. z ) ) )
88 3anass 
 |-  ( ( v e. y /\ v e. M /\ A. z e. y E. w e. y w e. z ) <-> ( v e. y /\ ( v e. M /\ A. z e. y E. w e. y w e. z ) ) )
89 88 exbii 
 |-  ( E. v ( v e. y /\ v e. M /\ A. z e. y E. w e. y w e. z ) <-> E. v ( v e. y /\ ( v e. M /\ A. z e. y E. w e. y w e. z ) ) )
90 87 89 bitr4i 
 |-  ( E. v e. y ( v e. M /\ A. z e. y E. w e. y w e. z ) <-> E. v ( v e. y /\ v e. M /\ A. z e. y E. w e. y w e. z ) )
91 90 exbii 
 |-  ( E. y E. v e. y ( v e. M /\ A. z e. y E. w e. y w e. z ) <-> E. y E. v ( v e. y /\ v e. M /\ A. z e. y E. w e. y w e. z ) )
92 86 91 sylib 
 |-  ( M e. V -> E. y E. v ( v e. y /\ v e. M /\ A. z e. y E. w e. y w e. z ) )
93 excom 
 |-  ( E. y E. v ( v e. y /\ v e. M /\ A. z e. y E. w e. y w e. z ) <-> E. v E. y ( v e. y /\ v e. M /\ A. z e. y E. w e. y w e. z ) )
94 92 93 sylib 
 |-  ( M e. V -> E. v E. y ( v e. y /\ v e. M /\ A. z e. y E. w e. y w e. z ) )
95 3ancomb 
 |-  ( ( v e. y /\ v e. M /\ A. z e. y E. w e. y w e. z ) <-> ( v e. y /\ A. z e. y E. w e. y w e. z /\ v e. M ) )
96 95 2exbii 
 |-  ( E. v E. y ( v e. y /\ v e. M /\ A. z e. y E. w e. y w e. z ) <-> E. v E. y ( v e. y /\ A. z e. y E. w e. y w e. z /\ v e. M ) )
97 94 96 sylib 
 |-  ( M e. V -> E. v E. y ( v e. y /\ A. z e. y E. w e. y w e. z /\ v e. M ) )
98 df-3an 
 |-  ( ( v e. y /\ A. z e. y E. w e. y w e. z /\ v e. M ) <-> ( ( v e. y /\ A. z e. y E. w e. y w e. z ) /\ v e. M ) )
99 98 exbii 
 |-  ( E. y ( v e. y /\ A. z e. y E. w e. y w e. z /\ v e. M ) <-> E. y ( ( v e. y /\ A. z e. y E. w e. y w e. z ) /\ v e. M ) )
100 19.41v 
 |-  ( E. y ( ( v e. y /\ A. z e. y E. w e. y w e. z ) /\ v e. M ) <-> ( E. y ( v e. y /\ A. z e. y E. w e. y w e. z ) /\ v e. M ) )
101 pm4.61 
 |-  ( -. ( v e. y -> E. z e. y ( z i^i y ) = (/) ) <-> ( v e. y /\ -. E. z e. y ( z i^i y ) = (/) ) )
102 101 exbii 
 |-  ( E. y -. ( v e. y -> E. z e. y ( z i^i y ) = (/) ) <-> E. y ( v e. y /\ -. E. z e. y ( z i^i y ) = (/) ) )
103 exnal 
 |-  ( E. y -. ( v e. y -> E. z e. y ( z i^i y ) = (/) ) <-> -. A. y ( v e. y -> E. z e. y ( z i^i y ) = (/) ) )
104 48 anbi2i 
 |-  ( ( v e. y /\ -. E. z e. y ( z i^i y ) = (/) ) <-> ( v e. y /\ -. E. z ( z e. y /\ ( z i^i y ) = (/) ) ) )
105 104 exbii 
 |-  ( E. y ( v e. y /\ -. E. z e. y ( z i^i y ) = (/) ) <-> E. y ( v e. y /\ -. E. z ( z e. y /\ ( z i^i y ) = (/) ) ) )
106 102 103 105 3bitr3i 
 |-  ( -. A. y ( v e. y -> E. z e. y ( z i^i y ) = (/) ) <-> E. y ( v e. y /\ -. E. z ( z e. y /\ ( z i^i y ) = (/) ) ) )
107 49 anbi2i 
 |-  ( ( v e. y /\ A. z -. ( z e. y /\ ( z i^i y ) = (/) ) ) <-> ( v e. y /\ -. E. z ( z e. y /\ ( z i^i y ) = (/) ) ) )
108 107 exbii 
 |-  ( E. y ( v e. y /\ A. z -. ( z e. y /\ ( z i^i y ) = (/) ) ) <-> E. y ( v e. y /\ -. E. z ( z e. y /\ ( z i^i y ) = (/) ) ) )
109 50 albii 
 |-  ( A. z -. ( z e. y /\ ( z i^i y ) = (/) ) <-> A. z ( -. z e. y \/ -. ( z i^i y ) = (/) ) )
110 109 anbi2i 
 |-  ( ( v e. y /\ A. z -. ( z e. y /\ ( z i^i y ) = (/) ) ) <-> ( v e. y /\ A. z ( -. z e. y \/ -. ( z i^i y ) = (/) ) ) )
111 110 exbii 
 |-  ( E. y ( v e. y /\ A. z -. ( z e. y /\ ( z i^i y ) = (/) ) ) <-> E. y ( v e. y /\ A. z ( -. z e. y \/ -. ( z i^i y ) = (/) ) ) )
112 106 108 111 3bitr2i 
 |-  ( -. A. y ( v e. y -> E. z e. y ( z i^i y ) = (/) ) <-> E. y ( v e. y /\ A. z ( -. z e. y \/ -. ( z i^i y ) = (/) ) ) )
113 51 albii 
 |-  ( A. z ( z e. y -> -. ( z i^i y ) = (/) ) <-> A. z ( -. z e. y \/ -. ( z i^i y ) = (/) ) )
114 113 anbi2i 
 |-  ( ( v e. y /\ A. z ( z e. y -> -. ( z i^i y ) = (/) ) ) <-> ( v e. y /\ A. z ( -. z e. y \/ -. ( z i^i y ) = (/) ) ) )
115 114 exbii 
 |-  ( E. y ( v e. y /\ A. z ( z e. y -> -. ( z i^i y ) = (/) ) ) <-> E. y ( v e. y /\ A. z ( -. z e. y \/ -. ( z i^i y ) = (/) ) ) )
116 112 115 bitr4i 
 |-  ( -. A. y ( v e. y -> E. z e. y ( z i^i y ) = (/) ) <-> E. y ( v e. y /\ A. z ( z e. y -> -. ( z i^i y ) = (/) ) ) )
117 55 anbi2i 
 |-  ( ( v e. y /\ A. z e. y -. ( z i^i y ) = (/) ) <-> ( v e. y /\ A. z ( z e. y -> -. ( z i^i y ) = (/) ) ) )
118 117 exbii 
 |-  ( E. y ( v e. y /\ A. z e. y -. ( z i^i y ) = (/) ) <-> E. y ( v e. y /\ A. z ( z e. y -> -. ( z i^i y ) = (/) ) ) )
119 66 anbi2i 
 |-  ( ( v e. y /\ A. z e. y -. ( z i^i y ) = (/) ) <-> ( v e. y /\ A. z e. y E. w e. y w e. z ) )
120 119 exbii 
 |-  ( E. y ( v e. y /\ A. z e. y -. ( z i^i y ) = (/) ) <-> E. y ( v e. y /\ A. z e. y E. w e. y w e. z ) )
121 116 118 120 3bitr2i 
 |-  ( -. A. y ( v e. y -> E. z e. y ( z i^i y ) = (/) ) <-> E. y ( v e. y /\ A. z e. y E. w e. y w e. z ) )
122 olc 
 |-  ( -. A. y ( v e. y -> E. z e. y ( z i^i y ) = (/) ) -> ( -. v e. V \/ -. A. y ( v e. y -> E. z e. y ( z i^i y ) = (/) ) ) )
123 ianor 
 |-  ( -. ( v e. V /\ A. y ( v e. y -> E. z e. y ( z i^i y ) = (/) ) ) <-> ( -. v e. V \/ -. A. y ( v e. y -> E. z e. y ( z i^i y ) = (/) ) ) )
124 elequ1 
 |-  ( x = v -> ( x e. y <-> v e. y ) )
125 124 imbi1d 
 |-  ( x = v -> ( ( x e. y -> E. z e. y ( z i^i y ) = (/) ) <-> ( v e. y -> E. z e. y ( z i^i y ) = (/) ) ) )
126 125 albidv 
 |-  ( x = v -> ( A. y ( x e. y -> E. z e. y ( z i^i y ) = (/) ) <-> A. y ( v e. y -> E. z e. y ( z i^i y ) = (/) ) ) )
127 126 1 elrab2 
 |-  ( v e. M <-> ( v e. V /\ A. y ( v e. y -> E. z e. y ( z i^i y ) = (/) ) ) )
128 123 127 xchnxbir 
 |-  ( -. v e. M <-> ( -. v e. V \/ -. A. y ( v e. y -> E. z e. y ( z i^i y ) = (/) ) ) )
129 122 128 sylibr 
 |-  ( -. A. y ( v e. y -> E. z e. y ( z i^i y ) = (/) ) -> -. v e. M )
130 121 129 sylbir 
 |-  ( E. y ( v e. y /\ A. z e. y E. w e. y w e. z ) -> -. v e. M )
131 130 anim1i 
 |-  ( ( E. y ( v e. y /\ A. z e. y E. w e. y w e. z ) /\ v e. M ) -> ( -. v e. M /\ v e. M ) )
132 100 131 sylbi 
 |-  ( E. y ( ( v e. y /\ A. z e. y E. w e. y w e. z ) /\ v e. M ) -> ( -. v e. M /\ v e. M ) )
133 99 132 sylbi 
 |-  ( E. y ( v e. y /\ A. z e. y E. w e. y w e. z /\ v e. M ) -> ( -. v e. M /\ v e. M ) )
134 133 eximi 
 |-  ( E. v E. y ( v e. y /\ A. z e. y E. w e. y w e. z /\ v e. M ) -> E. v ( -. v e. M /\ v e. M ) )
135 97 134 syl 
 |-  ( M e. V -> E. v ( -. v e. M /\ v e. M ) )
136 5 135 mto 
 |-  -. M e. V
137 136 nelir 
 |-  M e/ V