Step | Hyp | Ref
| Expression |
1 | | simpr 476 |
. 2
⊢ ((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) → (𝑀 ↾s 𝐴) ∈ Mnd) |
2 | | omndtos 29036 |
. . . 4
⊢ (𝑀 ∈ oMnd → 𝑀 ∈ Toset) |
3 | 2 | adantr 480 |
. . 3
⊢ ((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) → 𝑀 ∈ Toset) |
4 | | reldmress 15753 |
. . . . . . . 8
⊢ Rel dom
↾s |
5 | 4 | ovprc2 6583 |
. . . . . . 7
⊢ (¬
𝐴 ∈ V → (𝑀 ↾s 𝐴) = ∅) |
6 | 5 | fveq2d 6107 |
. . . . . 6
⊢ (¬
𝐴 ∈ V →
(Base‘(𝑀
↾s 𝐴)) =
(Base‘∅)) |
7 | 6 | adantl 481 |
. . . . 5
⊢ (((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ ¬ 𝐴 ∈ V) →
(Base‘(𝑀
↾s 𝐴)) =
(Base‘∅)) |
8 | | base0 15740 |
. . . . 5
⊢ ∅ =
(Base‘∅) |
9 | 7, 8 | syl6eqr 2662 |
. . . 4
⊢ (((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ ¬ 𝐴 ∈ V) →
(Base‘(𝑀
↾s 𝐴)) =
∅) |
10 | | eqid 2610 |
. . . . . . . 8
⊢
(Base‘(𝑀
↾s 𝐴)) =
(Base‘(𝑀
↾s 𝐴)) |
11 | | eqid 2610 |
. . . . . . . 8
⊢
(0g‘(𝑀 ↾s 𝐴)) = (0g‘(𝑀 ↾s 𝐴)) |
12 | 10, 11 | mndidcl 17131 |
. . . . . . 7
⊢ ((𝑀 ↾s 𝐴) ∈ Mnd →
(0g‘(𝑀
↾s 𝐴))
∈ (Base‘(𝑀
↾s 𝐴))) |
13 | | ne0i 3880 |
. . . . . . 7
⊢
((0g‘(𝑀 ↾s 𝐴)) ∈ (Base‘(𝑀 ↾s 𝐴)) → (Base‘(𝑀 ↾s 𝐴)) ≠ ∅) |
14 | 12, 13 | syl 17 |
. . . . . 6
⊢ ((𝑀 ↾s 𝐴) ∈ Mnd →
(Base‘(𝑀
↾s 𝐴))
≠ ∅) |
15 | 14 | ad2antlr 759 |
. . . . 5
⊢ (((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ ¬ 𝐴 ∈ V) →
(Base‘(𝑀
↾s 𝐴))
≠ ∅) |
16 | 15 | neneqd 2787 |
. . . 4
⊢ (((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ ¬ 𝐴 ∈ V) → ¬
(Base‘(𝑀
↾s 𝐴)) =
∅) |
17 | 9, 16 | condan 831 |
. . 3
⊢ ((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) → 𝐴 ∈ V) |
18 | | resstos 28991 |
. . 3
⊢ ((𝑀 ∈ Toset ∧ 𝐴 ∈ V) → (𝑀 ↾s 𝐴) ∈ Toset) |
19 | 3, 17, 18 | syl2anc 691 |
. 2
⊢ ((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) → (𝑀 ↾s 𝐴) ∈ Toset) |
20 | | simplll 794 |
. . . . . 6
⊢ ((((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) ∧ 𝑎(le‘(𝑀 ↾s 𝐴))𝑏) → 𝑀 ∈ oMnd) |
21 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑀 ↾s 𝐴) = (𝑀 ↾s 𝐴) |
22 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(Base‘𝑀) =
(Base‘𝑀) |
23 | 21, 22 | ressbas 15757 |
. . . . . . . . . 10
⊢ (𝐴 ∈ V → (𝐴 ∩ (Base‘𝑀)) = (Base‘(𝑀 ↾s 𝐴))) |
24 | | inss2 3796 |
. . . . . . . . . 10
⊢ (𝐴 ∩ (Base‘𝑀)) ⊆ (Base‘𝑀) |
25 | 23, 24 | syl6eqssr 3619 |
. . . . . . . . 9
⊢ (𝐴 ∈ V →
(Base‘(𝑀
↾s 𝐴))
⊆ (Base‘𝑀)) |
26 | 17, 25 | syl 17 |
. . . . . . . 8
⊢ ((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) →
(Base‘(𝑀
↾s 𝐴))
⊆ (Base‘𝑀)) |
27 | 26 | ad2antrr 758 |
. . . . . . 7
⊢ ((((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) ∧ 𝑎(le‘(𝑀 ↾s 𝐴))𝑏) → (Base‘(𝑀 ↾s 𝐴)) ⊆ (Base‘𝑀)) |
28 | | simplr1 1096 |
. . . . . . 7
⊢ ((((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) ∧ 𝑎(le‘(𝑀 ↾s 𝐴))𝑏) → 𝑎 ∈ (Base‘(𝑀 ↾s 𝐴))) |
29 | 27, 28 | sseldd 3569 |
. . . . . 6
⊢ ((((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) ∧ 𝑎(le‘(𝑀 ↾s 𝐴))𝑏) → 𝑎 ∈ (Base‘𝑀)) |
30 | | simplr2 1097 |
. . . . . . 7
⊢ ((((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) ∧ 𝑎(le‘(𝑀 ↾s 𝐴))𝑏) → 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴))) |
31 | 27, 30 | sseldd 3569 |
. . . . . 6
⊢ ((((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) ∧ 𝑎(le‘(𝑀 ↾s 𝐴))𝑏) → 𝑏 ∈ (Base‘𝑀)) |
32 | | simplr3 1098 |
. . . . . . 7
⊢ ((((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) ∧ 𝑎(le‘(𝑀 ↾s 𝐴))𝑏) → 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴))) |
33 | 27, 32 | sseldd 3569 |
. . . . . 6
⊢ ((((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) ∧ 𝑎(le‘(𝑀 ↾s 𝐴))𝑏) → 𝑐 ∈ (Base‘𝑀)) |
34 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(le‘𝑀) =
(le‘𝑀) |
35 | 21, 34 | ressle 15882 |
. . . . . . . . . 10
⊢ (𝐴 ∈ V → (le‘𝑀) = (le‘(𝑀 ↾s 𝐴))) |
36 | 17, 35 | syl 17 |
. . . . . . . . 9
⊢ ((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) →
(le‘𝑀) =
(le‘(𝑀
↾s 𝐴))) |
37 | 36 | adantr 480 |
. . . . . . . 8
⊢ (((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) → (le‘𝑀) = (le‘(𝑀 ↾s 𝐴))) |
38 | 37 | breqd 4594 |
. . . . . . 7
⊢ (((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) → (𝑎(le‘𝑀)𝑏 ↔ 𝑎(le‘(𝑀 ↾s 𝐴))𝑏)) |
39 | 38 | biimpar 501 |
. . . . . 6
⊢ ((((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) ∧ 𝑎(le‘(𝑀 ↾s 𝐴))𝑏) → 𝑎(le‘𝑀)𝑏) |
40 | | eqid 2610 |
. . . . . . 7
⊢
(+g‘𝑀) = (+g‘𝑀) |
41 | 22, 34, 40 | omndadd 29037 |
. . . . . 6
⊢ ((𝑀 ∈ oMnd ∧ (𝑎 ∈ (Base‘𝑀) ∧ 𝑏 ∈ (Base‘𝑀) ∧ 𝑐 ∈ (Base‘𝑀)) ∧ 𝑎(le‘𝑀)𝑏) → (𝑎(+g‘𝑀)𝑐)(le‘𝑀)(𝑏(+g‘𝑀)𝑐)) |
42 | 20, 29, 31, 33, 39, 41 | syl131anc 1331 |
. . . . 5
⊢ ((((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) ∧ 𝑎(le‘(𝑀 ↾s 𝐴))𝑏) → (𝑎(+g‘𝑀)𝑐)(le‘𝑀)(𝑏(+g‘𝑀)𝑐)) |
43 | 17 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) → 𝐴 ∈ V) |
44 | 21, 40 | ressplusg 15818 |
. . . . . . . . 9
⊢ (𝐴 ∈ V →
(+g‘𝑀) =
(+g‘(𝑀
↾s 𝐴))) |
45 | 43, 44 | syl 17 |
. . . . . . . 8
⊢ (((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) → (+g‘𝑀) = (+g‘(𝑀 ↾s 𝐴))) |
46 | 45 | oveqd 6566 |
. . . . . . 7
⊢ (((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) → (𝑎(+g‘𝑀)𝑐) = (𝑎(+g‘(𝑀 ↾s 𝐴))𝑐)) |
47 | 43, 35 | syl 17 |
. . . . . . 7
⊢ (((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) → (le‘𝑀) = (le‘(𝑀 ↾s 𝐴))) |
48 | 45 | oveqd 6566 |
. . . . . . 7
⊢ (((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) → (𝑏(+g‘𝑀)𝑐) = (𝑏(+g‘(𝑀 ↾s 𝐴))𝑐)) |
49 | 46, 47, 48 | breq123d 4597 |
. . . . . 6
⊢ (((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) → ((𝑎(+g‘𝑀)𝑐)(le‘𝑀)(𝑏(+g‘𝑀)𝑐) ↔ (𝑎(+g‘(𝑀 ↾s 𝐴))𝑐)(le‘(𝑀 ↾s 𝐴))(𝑏(+g‘(𝑀 ↾s 𝐴))𝑐))) |
50 | 49 | adantr 480 |
. . . . 5
⊢ ((((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) ∧ 𝑎(le‘(𝑀 ↾s 𝐴))𝑏) → ((𝑎(+g‘𝑀)𝑐)(le‘𝑀)(𝑏(+g‘𝑀)𝑐) ↔ (𝑎(+g‘(𝑀 ↾s 𝐴))𝑐)(le‘(𝑀 ↾s 𝐴))(𝑏(+g‘(𝑀 ↾s 𝐴))𝑐))) |
51 | 42, 50 | mpbid 221 |
. . . 4
⊢ ((((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) ∧ 𝑎(le‘(𝑀 ↾s 𝐴))𝑏) → (𝑎(+g‘(𝑀 ↾s 𝐴))𝑐)(le‘(𝑀 ↾s 𝐴))(𝑏(+g‘(𝑀 ↾s 𝐴))𝑐)) |
52 | 51 | ex 449 |
. . 3
⊢ (((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) → (𝑎(le‘(𝑀 ↾s 𝐴))𝑏 → (𝑎(+g‘(𝑀 ↾s 𝐴))𝑐)(le‘(𝑀 ↾s 𝐴))(𝑏(+g‘(𝑀 ↾s 𝐴))𝑐))) |
53 | 52 | ralrimivvva 2955 |
. 2
⊢ ((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) →
∀𝑎 ∈
(Base‘(𝑀
↾s 𝐴))∀𝑏 ∈ (Base‘(𝑀 ↾s 𝐴))∀𝑐 ∈ (Base‘(𝑀 ↾s 𝐴))(𝑎(le‘(𝑀 ↾s 𝐴))𝑏 → (𝑎(+g‘(𝑀 ↾s 𝐴))𝑐)(le‘(𝑀 ↾s 𝐴))(𝑏(+g‘(𝑀 ↾s 𝐴))𝑐))) |
54 | | eqid 2610 |
. . 3
⊢
(+g‘(𝑀 ↾s 𝐴)) = (+g‘(𝑀 ↾s 𝐴)) |
55 | | eqid 2610 |
. . 3
⊢
(le‘(𝑀
↾s 𝐴)) =
(le‘(𝑀
↾s 𝐴)) |
56 | 10, 54, 55 | isomnd 29032 |
. 2
⊢ ((𝑀 ↾s 𝐴) ∈ oMnd ↔ ((𝑀 ↾s 𝐴) ∈ Mnd ∧ (𝑀 ↾s 𝐴) ∈ Toset ∧
∀𝑎 ∈
(Base‘(𝑀
↾s 𝐴))∀𝑏 ∈ (Base‘(𝑀 ↾s 𝐴))∀𝑐 ∈ (Base‘(𝑀 ↾s 𝐴))(𝑎(le‘(𝑀 ↾s 𝐴))𝑏 → (𝑎(+g‘(𝑀 ↾s 𝐴))𝑐)(le‘(𝑀 ↾s 𝐴))(𝑏(+g‘(𝑀 ↾s 𝐴))𝑐)))) |
57 | 1, 19, 53, 56 | syl3anbrc 1239 |
1
⊢ ((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) → (𝑀 ↾s 𝐴) ∈ oMnd) |