Step | Hyp | Ref
| Expression |
1 | | copisnmnd.c |
. . 3
⊢ (𝜑 → 𝐶 ∈ 𝐵) |
2 | | copisnmnd.n |
. . 3
⊢ (𝜑 → 1 <
(♯‘𝐵)) |
3 | | copisnmnd.b |
. . . . . . 7
⊢ 𝐵 = (Base‘𝑀) |
4 | 3 | fvexi 6731 |
. . . . . 6
⊢ 𝐵 ∈ V |
5 | 4 | a1i 11 |
. . . . 5
⊢ ((𝐶 ∈ 𝐵 ∧ 1 < (♯‘𝐵)) → 𝐵 ∈ V) |
6 | | simpr 488 |
. . . . 5
⊢ ((𝐶 ∈ 𝐵 ∧ 1 < (♯‘𝐵)) → 1 <
(♯‘𝐵)) |
7 | | simpl 486 |
. . . . 5
⊢ ((𝐶 ∈ 𝐵 ∧ 1 < (♯‘𝐵)) → 𝐶 ∈ 𝐵) |
8 | | hashgt12el2 13990 |
. . . . 5
⊢ ((𝐵 ∈ V ∧ 1 <
(♯‘𝐵) ∧
𝐶 ∈ 𝐵) → ∃𝑐 ∈ 𝐵 𝐶 ≠ 𝑐) |
9 | 5, 6, 7, 8 | syl3anc 1373 |
. . . 4
⊢ ((𝐶 ∈ 𝐵 ∧ 1 < (♯‘𝐵)) → ∃𝑐 ∈ 𝐵 𝐶 ≠ 𝑐) |
10 | | df-ne 2941 |
. . . . . . 7
⊢ (𝐶 ≠ 𝑐 ↔ ¬ 𝐶 = 𝑐) |
11 | 10 | rexbii 3170 |
. . . . . 6
⊢
(∃𝑐 ∈
𝐵 𝐶 ≠ 𝑐 ↔ ∃𝑐 ∈ 𝐵 ¬ 𝐶 = 𝑐) |
12 | | rexnal 3160 |
. . . . . 6
⊢
(∃𝑐 ∈
𝐵 ¬ 𝐶 = 𝑐 ↔ ¬ ∀𝑐 ∈ 𝐵 𝐶 = 𝑐) |
13 | 11, 12 | bitri 278 |
. . . . 5
⊢
(∃𝑐 ∈
𝐵 𝐶 ≠ 𝑐 ↔ ¬ ∀𝑐 ∈ 𝐵 𝐶 = 𝑐) |
14 | | eqidd 2738 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)) |
15 | | eqidd 2738 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ (𝑥 = 𝑎 ∧ 𝑦 = 𝑐)) → 𝐶 = 𝐶) |
16 | | simpr 488 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → 𝑎 ∈ 𝐵) |
17 | 16 | adantr 484 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → 𝑎 ∈ 𝐵) |
18 | | simpr 488 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → 𝑐 ∈ 𝐵) |
19 | 1 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → 𝐶 ∈ 𝐵) |
20 | 19 | adantr 484 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → 𝐶 ∈ 𝐵) |
21 | 14, 15, 17, 18, 20 | ovmpod 7361 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → (𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐) = 𝐶) |
22 | 21 | adantr 484 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ (𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐) = 𝑐) → (𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐) = 𝐶) |
23 | | simpr 488 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ (𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐) = 𝑐) → (𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐) = 𝑐) |
24 | 22, 23 | eqtr3d 2779 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) ∧ (𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐) = 𝑐) → 𝐶 = 𝑐) |
25 | 24 | ex 416 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑐 ∈ 𝐵) → ((𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐) = 𝑐 → 𝐶 = 𝑐)) |
26 | 25 | ralimdva 3100 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (∀𝑐 ∈ 𝐵 (𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐) = 𝑐 → ∀𝑐 ∈ 𝐵 𝐶 = 𝑐)) |
27 | 26 | rexlimdva 3203 |
. . . . . . 7
⊢ (𝜑 → (∃𝑎 ∈ 𝐵 ∀𝑐 ∈ 𝐵 (𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐) = 𝑐 → ∀𝑐 ∈ 𝐵 𝐶 = 𝑐)) |
28 | 27 | con3d 155 |
. . . . . 6
⊢ (𝜑 → (¬ ∀𝑐 ∈ 𝐵 𝐶 = 𝑐 → ¬ ∃𝑎 ∈ 𝐵 ∀𝑐 ∈ 𝐵 (𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐) = 𝑐)) |
29 | | rexnal 3160 |
. . . . . . . . 9
⊢
(∃𝑐 ∈
𝐵 ¬ (𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐) = 𝑐 ↔ ¬ ∀𝑐 ∈ 𝐵 (𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐) = 𝑐) |
30 | 29 | bicomi 227 |
. . . . . . . 8
⊢ (¬
∀𝑐 ∈ 𝐵 (𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐) = 𝑐 ↔ ∃𝑐 ∈ 𝐵 ¬ (𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐) = 𝑐) |
31 | 30 | ralbii 3088 |
. . . . . . 7
⊢
(∀𝑎 ∈
𝐵 ¬ ∀𝑐 ∈ 𝐵 (𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐) = 𝑐 ↔ ∀𝑎 ∈ 𝐵 ∃𝑐 ∈ 𝐵 ¬ (𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐) = 𝑐) |
32 | | ralnex 3158 |
. . . . . . 7
⊢
(∀𝑎 ∈
𝐵 ¬ ∀𝑐 ∈ 𝐵 (𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐) = 𝑐 ↔ ¬ ∃𝑎 ∈ 𝐵 ∀𝑐 ∈ 𝐵 (𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐) = 𝑐) |
33 | | df-ne 2941 |
. . . . . . . . . 10
⊢ ((𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐) ≠ 𝑐 ↔ ¬ (𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐) = 𝑐) |
34 | 33 | bicomi 227 |
. . . . . . . . 9
⊢ (¬
(𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐) = 𝑐 ↔ (𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐) ≠ 𝑐) |
35 | 34 | rexbii 3170 |
. . . . . . . 8
⊢
(∃𝑐 ∈
𝐵 ¬ (𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐) = 𝑐 ↔ ∃𝑐 ∈ 𝐵 (𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐) ≠ 𝑐) |
36 | 35 | ralbii 3088 |
. . . . . . 7
⊢
(∀𝑎 ∈
𝐵 ∃𝑐 ∈ 𝐵 ¬ (𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐) = 𝑐 ↔ ∀𝑎 ∈ 𝐵 ∃𝑐 ∈ 𝐵 (𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐) ≠ 𝑐) |
37 | 31, 32, 36 | 3bitr3i 304 |
. . . . . 6
⊢ (¬
∃𝑎 ∈ 𝐵 ∀𝑐 ∈ 𝐵 (𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐) = 𝑐 ↔ ∀𝑎 ∈ 𝐵 ∃𝑐 ∈ 𝐵 (𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐) ≠ 𝑐) |
38 | 28, 37 | syl6ib 254 |
. . . . 5
⊢ (𝜑 → (¬ ∀𝑐 ∈ 𝐵 𝐶 = 𝑐 → ∀𝑎 ∈ 𝐵 ∃𝑐 ∈ 𝐵 (𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐) ≠ 𝑐)) |
39 | 13, 38 | syl5bi 245 |
. . . 4
⊢ (𝜑 → (∃𝑐 ∈ 𝐵 𝐶 ≠ 𝑐 → ∀𝑎 ∈ 𝐵 ∃𝑐 ∈ 𝐵 (𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐) ≠ 𝑐)) |
40 | 9, 39 | syl5 34 |
. . 3
⊢ (𝜑 → ((𝐶 ∈ 𝐵 ∧ 1 < (♯‘𝐵)) → ∀𝑎 ∈ 𝐵 ∃𝑐 ∈ 𝐵 (𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐) ≠ 𝑐)) |
41 | 1, 2, 40 | mp2and 699 |
. 2
⊢ (𝜑 → ∀𝑎 ∈ 𝐵 ∃𝑐 ∈ 𝐵 (𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐) ≠ 𝑐) |
42 | | copisnmnd.p |
. . . 4
⊢
(+g‘𝑀) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶) |
43 | 42 | eqcomi 2746 |
. . 3
⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶) = (+g‘𝑀) |
44 | 3, 43 | isnmnd 18177 |
. 2
⊢
(∀𝑎 ∈
𝐵 ∃𝑐 ∈ 𝐵 (𝑎(𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ 𝐶)𝑐) ≠ 𝑐 → 𝑀 ∉ Mnd) |
45 | 41, 44 | syl 17 |
1
⊢ (𝜑 → 𝑀 ∉ Mnd) |