| Step | Hyp | Ref
| Expression |
| 1 | | simpr 484 |
. 2
⊢ ((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) → (𝑀 ↾s 𝐴) ∈ Mnd) |
| 2 | | omndtos 33082 |
. . . 4
⊢ (𝑀 ∈ oMnd → 𝑀 ∈ Toset) |
| 3 | 2 | adantr 480 |
. . 3
⊢ ((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) → 𝑀 ∈ Toset) |
| 4 | | reldmress 17276 |
. . . . . . . 8
⊢ Rel dom
↾s |
| 5 | 4 | ovprc2 7471 |
. . . . . . 7
⊢ (¬
𝐴 ∈ V → (𝑀 ↾s 𝐴) = ∅) |
| 6 | 5 | fveq2d 6910 |
. . . . . 6
⊢ (¬
𝐴 ∈ V →
(Base‘(𝑀
↾s 𝐴)) =
(Base‘∅)) |
| 7 | 6 | adantl 481 |
. . . . 5
⊢ (((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ ¬ 𝐴 ∈ V) →
(Base‘(𝑀
↾s 𝐴)) =
(Base‘∅)) |
| 8 | | base0 17252 |
. . . . 5
⊢ ∅ =
(Base‘∅) |
| 9 | 7, 8 | eqtr4di 2795 |
. . . 4
⊢ (((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ ¬ 𝐴 ∈ V) →
(Base‘(𝑀
↾s 𝐴)) =
∅) |
| 10 | | eqid 2737 |
. . . . . . . 8
⊢
(Base‘(𝑀
↾s 𝐴)) =
(Base‘(𝑀
↾s 𝐴)) |
| 11 | | eqid 2737 |
. . . . . . . 8
⊢
(0g‘(𝑀 ↾s 𝐴)) = (0g‘(𝑀 ↾s 𝐴)) |
| 12 | 10, 11 | mndidcl 18762 |
. . . . . . 7
⊢ ((𝑀 ↾s 𝐴) ∈ Mnd →
(0g‘(𝑀
↾s 𝐴))
∈ (Base‘(𝑀
↾s 𝐴))) |
| 13 | 12 | ne0d 4342 |
. . . . . 6
⊢ ((𝑀 ↾s 𝐴) ∈ Mnd →
(Base‘(𝑀
↾s 𝐴))
≠ ∅) |
| 14 | 13 | ad2antlr 727 |
. . . . 5
⊢ (((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ ¬ 𝐴 ∈ V) →
(Base‘(𝑀
↾s 𝐴))
≠ ∅) |
| 15 | 14 | neneqd 2945 |
. . . 4
⊢ (((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ ¬ 𝐴 ∈ V) → ¬
(Base‘(𝑀
↾s 𝐴)) =
∅) |
| 16 | 9, 15 | condan 818 |
. . 3
⊢ ((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) → 𝐴 ∈ V) |
| 17 | | resstos 32957 |
. . 3
⊢ ((𝑀 ∈ Toset ∧ 𝐴 ∈ V) → (𝑀 ↾s 𝐴) ∈ Toset) |
| 18 | 3, 16, 17 | syl2anc 584 |
. 2
⊢ ((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) → (𝑀 ↾s 𝐴) ∈ Toset) |
| 19 | | simplll 775 |
. . . . . 6
⊢ ((((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) ∧ 𝑎(le‘(𝑀 ↾s 𝐴))𝑏) → 𝑀 ∈ oMnd) |
| 20 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝑀 ↾s 𝐴) = (𝑀 ↾s 𝐴) |
| 21 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(Base‘𝑀) =
(Base‘𝑀) |
| 22 | 20, 21 | ressbas 17280 |
. . . . . . . . . 10
⊢ (𝐴 ∈ V → (𝐴 ∩ (Base‘𝑀)) = (Base‘(𝑀 ↾s 𝐴))) |
| 23 | | inss2 4238 |
. . . . . . . . . 10
⊢ (𝐴 ∩ (Base‘𝑀)) ⊆ (Base‘𝑀) |
| 24 | 22, 23 | eqsstrrdi 4029 |
. . . . . . . . 9
⊢ (𝐴 ∈ V →
(Base‘(𝑀
↾s 𝐴))
⊆ (Base‘𝑀)) |
| 25 | 16, 24 | syl 17 |
. . . . . . . 8
⊢ ((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) →
(Base‘(𝑀
↾s 𝐴))
⊆ (Base‘𝑀)) |
| 26 | 25 | ad2antrr 726 |
. . . . . . 7
⊢ ((((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) ∧ 𝑎(le‘(𝑀 ↾s 𝐴))𝑏) → (Base‘(𝑀 ↾s 𝐴)) ⊆ (Base‘𝑀)) |
| 27 | | simplr1 1216 |
. . . . . . 7
⊢ ((((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) ∧ 𝑎(le‘(𝑀 ↾s 𝐴))𝑏) → 𝑎 ∈ (Base‘(𝑀 ↾s 𝐴))) |
| 28 | 26, 27 | sseldd 3984 |
. . . . . 6
⊢ ((((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) ∧ 𝑎(le‘(𝑀 ↾s 𝐴))𝑏) → 𝑎 ∈ (Base‘𝑀)) |
| 29 | | simplr2 1217 |
. . . . . . 7
⊢ ((((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) ∧ 𝑎(le‘(𝑀 ↾s 𝐴))𝑏) → 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴))) |
| 30 | 26, 29 | sseldd 3984 |
. . . . . 6
⊢ ((((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) ∧ 𝑎(le‘(𝑀 ↾s 𝐴))𝑏) → 𝑏 ∈ (Base‘𝑀)) |
| 31 | | simplr3 1218 |
. . . . . . 7
⊢ ((((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) ∧ 𝑎(le‘(𝑀 ↾s 𝐴))𝑏) → 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴))) |
| 32 | 26, 31 | sseldd 3984 |
. . . . . 6
⊢ ((((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) ∧ 𝑎(le‘(𝑀 ↾s 𝐴))𝑏) → 𝑐 ∈ (Base‘𝑀)) |
| 33 | | eqid 2737 |
. . . . . . . . . . 11
⊢
(le‘𝑀) =
(le‘𝑀) |
| 34 | 20, 33 | ressle 17424 |
. . . . . . . . . 10
⊢ (𝐴 ∈ V → (le‘𝑀) = (le‘(𝑀 ↾s 𝐴))) |
| 35 | 16, 34 | syl 17 |
. . . . . . . . 9
⊢ ((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) →
(le‘𝑀) =
(le‘(𝑀
↾s 𝐴))) |
| 36 | 35 | adantr 480 |
. . . . . . . 8
⊢ (((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) → (le‘𝑀) = (le‘(𝑀 ↾s 𝐴))) |
| 37 | 36 | breqd 5154 |
. . . . . . 7
⊢ (((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) → (𝑎(le‘𝑀)𝑏 ↔ 𝑎(le‘(𝑀 ↾s 𝐴))𝑏)) |
| 38 | 37 | biimpar 477 |
. . . . . 6
⊢ ((((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) ∧ 𝑎(le‘(𝑀 ↾s 𝐴))𝑏) → 𝑎(le‘𝑀)𝑏) |
| 39 | | eqid 2737 |
. . . . . . 7
⊢
(+g‘𝑀) = (+g‘𝑀) |
| 40 | 21, 33, 39 | omndadd 33083 |
. . . . . 6
⊢ ((𝑀 ∈ oMnd ∧ (𝑎 ∈ (Base‘𝑀) ∧ 𝑏 ∈ (Base‘𝑀) ∧ 𝑐 ∈ (Base‘𝑀)) ∧ 𝑎(le‘𝑀)𝑏) → (𝑎(+g‘𝑀)𝑐)(le‘𝑀)(𝑏(+g‘𝑀)𝑐)) |
| 41 | 19, 28, 30, 32, 38, 40 | syl131anc 1385 |
. . . . 5
⊢ ((((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) ∧ 𝑎(le‘(𝑀 ↾s 𝐴))𝑏) → (𝑎(+g‘𝑀)𝑐)(le‘𝑀)(𝑏(+g‘𝑀)𝑐)) |
| 42 | 16 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) → 𝐴 ∈ V) |
| 43 | 20, 39 | ressplusg 17334 |
. . . . . . . . 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 7448 |
. . . . . . 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 7448 |
. . . . . . 7
⊢ (((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) → (𝑏(+g‘𝑀)𝑐) = (𝑏(+g‘(𝑀 ↾s 𝐴))𝑐)) |
| 48 | 45, 46, 47 | breq123d 5157 |
. . . . . 6
⊢ (((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) → ((𝑎(+g‘𝑀)𝑐)(le‘𝑀)(𝑏(+g‘𝑀)𝑐) ↔ (𝑎(+g‘(𝑀 ↾s 𝐴))𝑐)(le‘(𝑀 ↾s 𝐴))(𝑏(+g‘(𝑀 ↾s 𝐴))𝑐))) |
| 49 | 48 | adantr 480 |
. . . . 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 232 |
. . . 4
⊢ ((((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) ∧ 𝑎(le‘(𝑀 ↾s 𝐴))𝑏) → (𝑎(+g‘(𝑀 ↾s 𝐴))𝑐)(le‘(𝑀 ↾s 𝐴))(𝑏(+g‘(𝑀 ↾s 𝐴))𝑐)) |
| 51 | 50 | ex 412 |
. . 3
⊢ (((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) ∧ (𝑎 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑏 ∈ (Base‘(𝑀 ↾s 𝐴)) ∧ 𝑐 ∈ (Base‘(𝑀 ↾s 𝐴)))) → (𝑎(le‘(𝑀 ↾s 𝐴))𝑏 → (𝑎(+g‘(𝑀 ↾s 𝐴))𝑐)(le‘(𝑀 ↾s 𝐴))(𝑏(+g‘(𝑀 ↾s 𝐴))𝑐))) |
| 52 | 51 | ralrimivvva 3205 |
. 2
⊢ ((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) →
∀𝑎 ∈
(Base‘(𝑀
↾s 𝐴))∀𝑏 ∈ (Base‘(𝑀 ↾s 𝐴))∀𝑐 ∈ (Base‘(𝑀 ↾s 𝐴))(𝑎(le‘(𝑀 ↾s 𝐴))𝑏 → (𝑎(+g‘(𝑀 ↾s 𝐴))𝑐)(le‘(𝑀 ↾s 𝐴))(𝑏(+g‘(𝑀 ↾s 𝐴))𝑐))) |
| 53 | | eqid 2737 |
. . 3
⊢
(+g‘(𝑀 ↾s 𝐴)) = (+g‘(𝑀 ↾s 𝐴)) |
| 54 | | eqid 2737 |
. . 3
⊢
(le‘(𝑀
↾s 𝐴)) =
(le‘(𝑀
↾s 𝐴)) |
| 55 | 10, 53, 54 | isomnd 33078 |
. 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 1344 |
1
⊢ ((𝑀 ∈ oMnd ∧ (𝑀 ↾s 𝐴) ∈ Mnd) → (𝑀 ↾s 𝐴) ∈ oMnd) |