Step | Hyp | Ref
| Expression |
1 | | simpr 487 |
. 2
⊢ ((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) → (𝑀 ↾s 𝐴) ∈ Mnd) |
2 | | omndtos 30701 |
. . . 4
⊢ (𝑀 ∈ oMnd → 𝑀 ∈ Toset) |
3 | 2 | adantr 483 |
. . 3
⊢ ((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) → 𝑀 ∈ Toset) |
4 | | reldmress 16544 |
. . . . . . . 8
⊢ Rel dom
↾s |
5 | 4 | ovprc2 7190 |
. . . . . . 7
⊢ (¬
𝐴 ∈ V → (𝑀 ↾s 𝐴) = ∅) |
6 | 5 | fveq2d 6669 |
. . . . . 6
⊢ (¬
𝐴 ∈ V →
(Base‘(𝑀
↾s 𝐴)) =
(Base‘∅)) |
7 | 6 | adantl 484 |
. . . . 5
⊢ (((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ ¬ 𝐴 ∈ V) →
(Base‘(𝑀
↾s 𝐴)) =
(Base‘∅)) |
8 | | base0 16530 |
. . . . 5
⊢ ∅ =
(Base‘∅) |
9 | 7, 8 | syl6eqr 2874 |
. . . 4
⊢ (((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ ¬ 𝐴 ∈ V) →
(Base‘(𝑀
↾s 𝐴)) =
∅) |
10 | | eqid 2821 |
. . . . . . . 8
⊢
(Base‘(𝑀
↾s 𝐴)) =
(Base‘(𝑀
↾s 𝐴)) |
11 | | eqid 2821 |
. . . . . . . 8
⊢
(0g‘(𝑀 ↾s 𝐴)) = (0g‘(𝑀 ↾s 𝐴)) |
12 | 10, 11 | mndidcl 17920 |
. . . . . . 7
⊢ ((𝑀 ↾s 𝐴) ∈ Mnd →
(0g‘(𝑀
↾s 𝐴))
∈ (Base‘(𝑀
↾s 𝐴))) |
13 | 12 | ne0d 4301 |
. . . . . 6
⊢ ((𝑀 ↾s 𝐴) ∈ Mnd →
(Base‘(𝑀
↾s 𝐴))
≠ ∅) |
14 | 13 | ad2antlr 725 |
. . . . 5
⊢ (((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ ¬ 𝐴 ∈ V) →
(Base‘(𝑀
↾s 𝐴))
≠ ∅) |
15 | 14 | neneqd 3021 |
. . . 4
⊢ (((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ ¬ 𝐴 ∈ V) → ¬
(Base‘(𝑀
↾s 𝐴)) =
∅) |
16 | 9, 15 | condan 816 |
. . 3
⊢ ((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) → 𝐴 ∈ V) |
17 | | resstos 30642 |
. . 3
⊢ ((𝑀 ∈ Toset ∧ 𝐴 ∈ V) → (𝑀 ↾s 𝐴) ∈ Toset) |
18 | 3, 16, 17 | syl2anc 586 |
. 2
⊢ ((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) → (𝑀 ↾s 𝐴) ∈ Toset) |
19 | | simplll 773 |
. . . . . 6
⊢ ((((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) ∧ 𝑎(le‘(𝑀 ↾s 𝐴))𝑏) → 𝑀 ∈ oMnd) |
20 | | eqid 2821 |
. . . . . . . . . . 11
⊢ (𝑀 ↾s 𝐴) = (𝑀 ↾s 𝐴) |
21 | | eqid 2821 |
. . . . . . . . . . 11
⊢
(Base‘𝑀) =
(Base‘𝑀) |
22 | 20, 21 | ressbas 16548 |
. . . . . . . . . 10
⊢ (𝐴 ∈ V → (𝐴 ∩ (Base‘𝑀)) = (Base‘(𝑀 ↾s 𝐴))) |
23 | | inss2 4206 |
. . . . . . . . . 10
⊢ (𝐴 ∩ (Base‘𝑀)) ⊆ (Base‘𝑀) |
24 | 22, 23 | eqsstrrdi 4022 |
. . . . . . . . 9
⊢ (𝐴 ∈ V →
(Base‘(𝑀
↾s 𝐴))
⊆ (Base‘𝑀)) |
25 | 16, 24 | syl 17 |
. . . . . . . 8
⊢ ((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) →
(Base‘(𝑀
↾s 𝐴))
⊆ (Base‘𝑀)) |
26 | 25 | ad2antrr 724 |
. . . . . . 7
⊢ ((((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) ∧ 𝑎(le‘(𝑀 ↾s 𝐴))𝑏) → (Base‘(𝑀 ↾s 𝐴)) ⊆ (Base‘𝑀)) |
27 | | simplr1 1211 |
. . . . . . 7
⊢ ((((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) ∧ 𝑎(le‘(𝑀 ↾s 𝐴))𝑏) → 𝑎 ∈ (Base‘(𝑀 ↾s 𝐴))) |
28 | 26, 27 | sseldd 3968 |
. . . . . 6
⊢ ((((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) ∧ 𝑎(le‘(𝑀 ↾s 𝐴))𝑏) → 𝑎 ∈ (Base‘𝑀)) |
29 | | simplr2 1212 |
. . . . . . 7
⊢ ((((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) ∧ 𝑎(le‘(𝑀 ↾s 𝐴))𝑏) → 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴))) |
30 | 26, 29 | sseldd 3968 |
. . . . . 6
⊢ ((((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) ∧ 𝑎(le‘(𝑀 ↾s 𝐴))𝑏) → 𝑏 ∈ (Base‘𝑀)) |
31 | | simplr3 1213 |
. . . . . . 7
⊢ ((((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) ∧ 𝑎(le‘(𝑀 ↾s 𝐴))𝑏) → 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴))) |
32 | 26, 31 | sseldd 3968 |
. . . . . 6
⊢ ((((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) ∧ 𝑎(le‘(𝑀 ↾s 𝐴))𝑏) → 𝑐 ∈ (Base‘𝑀)) |
33 | | eqid 2821 |
. . . . . . . . . . 11
⊢
(le‘𝑀) =
(le‘𝑀) |
34 | 20, 33 | ressle 16666 |
. . . . . . . . . 10
⊢ (𝐴 ∈ V → (le‘𝑀) = (le‘(𝑀 ↾s 𝐴))) |
35 | 16, 34 | syl 17 |
. . . . . . . . 9
⊢ ((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) →
(le‘𝑀) =
(le‘(𝑀
↾s 𝐴))) |
36 | 35 | adantr 483 |
. . . . . . . 8
⊢ (((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) → (le‘𝑀) = (le‘(𝑀 ↾s 𝐴))) |
37 | 36 | breqd 5070 |
. . . . . . 7
⊢ (((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) → (𝑎(le‘𝑀)𝑏 ↔ 𝑎(le‘(𝑀 ↾s 𝐴))𝑏)) |
38 | 37 | biimpar 480 |
. . . . . 6
⊢ ((((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) ∧ 𝑎(le‘(𝑀 ↾s 𝐴))𝑏) → 𝑎(le‘𝑀)𝑏) |
39 | | eqid 2821 |
. . . . . . 7
⊢
(+g‘𝑀) = (+g‘𝑀) |
40 | 21, 33, 39 | omndadd 30702 |
. . . . . 6
⊢ ((𝑀 ∈ oMnd ∧ (𝑎 ∈ (Base‘𝑀) ∧ 𝑏 ∈ (Base‘𝑀) ∧ 𝑐 ∈ (Base‘𝑀)) ∧ 𝑎(le‘𝑀)𝑏) → (𝑎(+g‘𝑀)𝑐)(le‘𝑀)(𝑏(+g‘𝑀)𝑐)) |
41 | 19, 28, 30, 32, 38, 40 | syl131anc 1379 |
. . . . 5
⊢ ((((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) ∧ 𝑎(le‘(𝑀 ↾s 𝐴))𝑏) → (𝑎(+g‘𝑀)𝑐)(le‘𝑀)(𝑏(+g‘𝑀)𝑐)) |
42 | 16 | adantr 483 |
. . . . . . . . 9
⊢ (((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) → 𝐴 ∈ V) |
43 | 20, 39 | ressplusg 16606 |
. . . . . . . . 9
⊢ (𝐴 ∈ V →
(+g‘𝑀) =
(+g‘(𝑀
↾s 𝐴))) |
44 | 42, 43 | syl 17 |
. . . . . . . 8
⊢ (((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) → (+g‘𝑀) = (+g‘(𝑀 ↾s 𝐴))) |
45 | 44 | oveqd 7167 |
. . . . . . 7
⊢ (((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) → (𝑎(+g‘𝑀)𝑐) = (𝑎(+g‘(𝑀 ↾s 𝐴))𝑐)) |
46 | 42, 34 | syl 17 |
. . . . . . 7
⊢ (((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) → (le‘𝑀) = (le‘(𝑀 ↾s 𝐴))) |
47 | 44 | oveqd 7167 |
. . . . . . 7
⊢ (((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) → (𝑏(+g‘𝑀)𝑐) = (𝑏(+g‘(𝑀 ↾s 𝐴))𝑐)) |
48 | 45, 46, 47 | breq123d 5073 |
. . . . . 6
⊢ (((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) → ((𝑎(+g‘𝑀)𝑐)(le‘𝑀)(𝑏(+g‘𝑀)𝑐) ↔ (𝑎(+g‘(𝑀 ↾s 𝐴))𝑐)(le‘(𝑀 ↾s 𝐴))(𝑏(+g‘(𝑀 ↾s 𝐴))𝑐))) |
49 | 48 | adantr 483 |
. . . . 5
⊢ ((((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) ∧ 𝑎(le‘(𝑀 ↾s 𝐴))𝑏) → ((𝑎(+g‘𝑀)𝑐)(le‘𝑀)(𝑏(+g‘𝑀)𝑐) ↔ (𝑎(+g‘(𝑀 ↾s 𝐴))𝑐)(le‘(𝑀 ↾s 𝐴))(𝑏(+g‘(𝑀 ↾s 𝐴))𝑐))) |
50 | 41, 49 | mpbid 234 |
. . . 4
⊢ ((((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) ∧ 𝑎(le‘(𝑀 ↾s 𝐴))𝑏) → (𝑎(+g‘(𝑀 ↾s 𝐴))𝑐)(le‘(𝑀 ↾s 𝐴))(𝑏(+g‘(𝑀 ↾s 𝐴))𝑐)) |
51 | 50 | ex 415 |
. . 3
⊢ (((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) → (𝑎(le‘(𝑀 ↾s 𝐴))𝑏 → (𝑎(+g‘(𝑀 ↾s 𝐴))𝑐)(le‘(𝑀 ↾s 𝐴))(𝑏(+g‘(𝑀 ↾s 𝐴))𝑐))) |
52 | 51 | ralrimivvva 3192 |
. 2
⊢ ((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) →
∀𝑎 ∈
(Base‘(𝑀
↾s 𝐴))∀𝑏 ∈ (Base‘(𝑀 ↾s 𝐴))∀𝑐 ∈ (Base‘(𝑀 ↾s 𝐴))(𝑎(le‘(𝑀 ↾s 𝐴))𝑏 → (𝑎(+g‘(𝑀 ↾s 𝐴))𝑐)(le‘(𝑀 ↾s 𝐴))(𝑏(+g‘(𝑀 ↾s 𝐴))𝑐))) |
53 | | eqid 2821 |
. . 3
⊢
(+g‘(𝑀 ↾s 𝐴)) = (+g‘(𝑀 ↾s 𝐴)) |
54 | | eqid 2821 |
. . 3
⊢
(le‘(𝑀
↾s 𝐴)) =
(le‘(𝑀
↾s 𝐴)) |
55 | 10, 53, 54 | isomnd 30697 |
. 2
⊢ ((𝑀 ↾s 𝐴) ∈ oMnd ↔ ((𝑀 ↾s 𝐴) ∈ Mnd ∧ (𝑀 ↾s 𝐴) ∈ Toset ∧
∀𝑎 ∈
(Base‘(𝑀
↾s 𝐴))∀𝑏 ∈ (Base‘(𝑀 ↾s 𝐴))∀𝑐 ∈ (Base‘(𝑀 ↾s 𝐴))(𝑎(le‘(𝑀 ↾s 𝐴))𝑏 → (𝑎(+g‘(𝑀 ↾s 𝐴))𝑐)(le‘(𝑀 ↾s 𝐴))(𝑏(+g‘(𝑀 ↾s 𝐴))𝑐)))) |
56 | 1, 18, 52, 55 | syl3anbrc 1339 |
1
⊢ ((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) → (𝑀 ↾s 𝐴) ∈ oMnd) |