| Step | Hyp | Ref
| Expression |
| 1 | | df-subrng 20546 |
. . 3
⊢ SubRng =
(𝑤 ∈ Rng ↦
{𝑠 ∈ 𝒫
(Base‘𝑤) ∣
(𝑤 ↾s
𝑠) ∈
Rng}) |
| 2 | 1 | mptrcl 7025 |
. 2
⊢ (𝐴 ∈ (SubRng‘𝑅) → 𝑅 ∈ Rng) |
| 3 | | simp1 1137 |
. 2
⊢ ((𝑅 ∈ Rng ∧ (𝑅 ↾s 𝐴) ∈ Rng ∧ 𝐴 ⊆ 𝐵) → 𝑅 ∈ Rng) |
| 4 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅)) |
| 5 | 4 | pweqd 4617 |
. . . . . 6
⊢ (𝑟 = 𝑅 → 𝒫 (Base‘𝑟) = 𝒫 (Base‘𝑅)) |
| 6 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑟 = 𝑅 → (𝑟 ↾s 𝑠) = (𝑅 ↾s 𝑠)) |
| 7 | 6 | eleq1d 2826 |
. . . . . 6
⊢ (𝑟 = 𝑅 → ((𝑟 ↾s 𝑠) ∈ Rng ↔ (𝑅 ↾s 𝑠) ∈ Rng)) |
| 8 | 5, 7 | rabeqbidv 3455 |
. . . . 5
⊢ (𝑟 = 𝑅 → {𝑠 ∈ 𝒫 (Base‘𝑟) ∣ (𝑟 ↾s 𝑠) ∈ Rng} = {𝑠 ∈ 𝒫 (Base‘𝑅) ∣ (𝑅 ↾s 𝑠) ∈ Rng}) |
| 9 | | df-subrng 20546 |
. . . . 5
⊢ SubRng =
(𝑟 ∈ Rng ↦
{𝑠 ∈ 𝒫
(Base‘𝑟) ∣
(𝑟 ↾s
𝑠) ∈
Rng}) |
| 10 | | fvex 6919 |
. . . . . . 7
⊢
(Base‘𝑅)
∈ V |
| 11 | 10 | pwex 5380 |
. . . . . 6
⊢ 𝒫
(Base‘𝑅) ∈
V |
| 12 | 11 | rabex 5339 |
. . . . 5
⊢ {𝑠 ∈ 𝒫
(Base‘𝑅) ∣
(𝑅 ↾s
𝑠) ∈ Rng} ∈
V |
| 13 | 8, 9, 12 | fvmpt 7016 |
. . . 4
⊢ (𝑅 ∈ Rng →
(SubRng‘𝑅) = {𝑠 ∈ 𝒫
(Base‘𝑅) ∣
(𝑅 ↾s
𝑠) ∈
Rng}) |
| 14 | 13 | eleq2d 2827 |
. . 3
⊢ (𝑅 ∈ Rng → (𝐴 ∈ (SubRng‘𝑅) ↔ 𝐴 ∈ {𝑠 ∈ 𝒫 (Base‘𝑅) ∣ (𝑅 ↾s 𝑠) ∈ Rng})) |
| 15 | | oveq2 7439 |
. . . . . 6
⊢ (𝑠 = 𝐴 → (𝑅 ↾s 𝑠) = (𝑅 ↾s 𝐴)) |
| 16 | 15 | eleq1d 2826 |
. . . . 5
⊢ (𝑠 = 𝐴 → ((𝑅 ↾s 𝑠) ∈ Rng ↔ (𝑅 ↾s 𝐴) ∈ Rng)) |
| 17 | 16 | elrab 3692 |
. . . 4
⊢ (𝐴 ∈ {𝑠 ∈ 𝒫 (Base‘𝑅) ∣ (𝑅 ↾s 𝑠) ∈ Rng} ↔ (𝐴 ∈ 𝒫 (Base‘𝑅) ∧ (𝑅 ↾s 𝐴) ∈ Rng)) |
| 18 | | issubrng.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝑅) |
| 19 | 18 | eqcomi 2746 |
. . . . . . . 8
⊢
(Base‘𝑅) =
𝐵 |
| 20 | 19 | sseq2i 4013 |
. . . . . . 7
⊢ (𝐴 ⊆ (Base‘𝑅) ↔ 𝐴 ⊆ 𝐵) |
| 21 | 20 | anbi2i 623 |
. . . . . 6
⊢ (((𝑅 ↾s 𝐴) ∈ Rng ∧ 𝐴 ⊆ (Base‘𝑅)) ↔ ((𝑅 ↾s 𝐴) ∈ Rng ∧ 𝐴 ⊆ 𝐵)) |
| 22 | | ibar 528 |
. . . . . 6
⊢ (𝑅 ∈ Rng → (((𝑅 ↾s 𝐴) ∈ Rng ∧ 𝐴 ⊆ 𝐵) ↔ (𝑅 ∈ Rng ∧ ((𝑅 ↾s 𝐴) ∈ Rng ∧ 𝐴 ⊆ 𝐵)))) |
| 23 | 21, 22 | bitrid 283 |
. . . . 5
⊢ (𝑅 ∈ Rng → (((𝑅 ↾s 𝐴) ∈ Rng ∧ 𝐴 ⊆ (Base‘𝑅)) ↔ (𝑅 ∈ Rng ∧ ((𝑅 ↾s 𝐴) ∈ Rng ∧ 𝐴 ⊆ 𝐵)))) |
| 24 | 10 | elpw2 5334 |
. . . . . 6
⊢ (𝐴 ∈ 𝒫
(Base‘𝑅) ↔ 𝐴 ⊆ (Base‘𝑅)) |
| 25 | 24 | anbi2ci 625 |
. . . . 5
⊢ ((𝐴 ∈ 𝒫
(Base‘𝑅) ∧ (𝑅 ↾s 𝐴) ∈ Rng) ↔ ((𝑅 ↾s 𝐴) ∈ Rng ∧ 𝐴 ⊆ (Base‘𝑅))) |
| 26 | | 3anass 1095 |
. . . . 5
⊢ ((𝑅 ∈ Rng ∧ (𝑅 ↾s 𝐴) ∈ Rng ∧ 𝐴 ⊆ 𝐵) ↔ (𝑅 ∈ Rng ∧ ((𝑅 ↾s 𝐴) ∈ Rng ∧ 𝐴 ⊆ 𝐵))) |
| 27 | 23, 25, 26 | 3bitr4g 314 |
. . . 4
⊢ (𝑅 ∈ Rng → ((𝐴 ∈ 𝒫
(Base‘𝑅) ∧ (𝑅 ↾s 𝐴) ∈ Rng) ↔ (𝑅 ∈ Rng ∧ (𝑅 ↾s 𝐴) ∈ Rng ∧ 𝐴 ⊆ 𝐵))) |
| 28 | 17, 27 | bitrid 283 |
. . 3
⊢ (𝑅 ∈ Rng → (𝐴 ∈ {𝑠 ∈ 𝒫 (Base‘𝑅) ∣ (𝑅 ↾s 𝑠) ∈ Rng} ↔ (𝑅 ∈ Rng ∧ (𝑅 ↾s 𝐴) ∈ Rng ∧ 𝐴 ⊆ 𝐵))) |
| 29 | 14, 28 | bitrd 279 |
. 2
⊢ (𝑅 ∈ Rng → (𝐴 ∈ (SubRng‘𝑅) ↔ (𝑅 ∈ Rng ∧ (𝑅 ↾s 𝐴) ∈ Rng ∧ 𝐴 ⊆ 𝐵))) |
| 30 | 2, 3, 29 | pm5.21nii 378 |
1
⊢ (𝐴 ∈ (SubRng‘𝑅) ↔ (𝑅 ∈ Rng ∧ (𝑅 ↾s 𝐴) ∈ Rng ∧ 𝐴 ⊆ 𝐵)) |