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 ⊢ 𝑀 = { 𝑥 ∈ 𝑉 ∣ ∀ 𝑦 ( 𝑥 ∈ 𝑦 → ∃ 𝑧 ∈ 𝑦 ( 𝑧 ∩ 𝑦 ) = ∅ ) }
Assertion mirimanofffr 𝑀 ∉ 𝑉

Proof

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