Metamath Proof Explorer

Theorem subsubrng2

Description: The set of subrings of a subring are the smaller subrings. (Contributed by AV, 15-Feb-2025)

Ref Expression
Hypothesis subsubrng.s ⊢ S = R ↾ 𝑠 A
Assertion subsubrng2 ⊢ A ∈ SubRng ⁡ R → SubRng ⁡ S = SubRng ⁡ R ∩ 𝒫 A

Proof

Step Hyp Ref Expression
1 subsubrng.s ⊢ S = R ↾ 𝑠 A
2 1 subsubrng ⊢ A ∈ SubRng ⁡ R → a ∈ SubRng ⁡ S ↔ a ∈ SubRng ⁡ R ∧ a ⊆ A
3 elin ⊢ a ∈ SubRng ⁡ R ∩ 𝒫 A ↔ a ∈ SubRng ⁡ R ∧ a ∈ 𝒫 A
4 velpw ⊢ a ∈ 𝒫 A ↔ a ⊆ A
5 4 anbi2i ⊢ a ∈ SubRng ⁡ R ∧ a ∈ 𝒫 A ↔ a ∈ SubRng ⁡ R ∧ a ⊆ A
6 3 5 bitr2i ⊢ a ∈ SubRng ⁡ R ∧ a ⊆ A ↔ a ∈ SubRng ⁡ R ∩ 𝒫 A
7 2 6 bitrdi ⊢ A ∈ SubRng ⁡ R → a ∈ SubRng ⁡ S ↔ a ∈ SubRng ⁡ R ∩ 𝒫 A
8 7 eqrdv ⊢ A ∈ SubRng ⁡ R → SubRng ⁡ S = SubRng ⁡ R ∩ 𝒫 A