Metamath Proof Explorer

Theorem subsubrg2

Description: The set of subrings of a subring are the smaller subrings. (Contributed by Stefan O'Rear, 9-Mar-2015)

Ref Expression
Hypothesis subsubrg.s ⊢ S = R ↾ 𝑠 A
Assertion subsubrg2 ⊢ A ∈ SubRing ⁡ R → SubRing ⁡ S = SubRing ⁡ R ∩ 𝒫 A

Proof

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