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 ∈ V | ∀ y x ∈ y → ∃ z ∈ y z ∩ y = ∅
Assertion mirimanofffr ⊢ M ∉ V

Proof

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