---

Step * 1 of Lemma princ_ideal_wf


1. r : Rng
2. a : |r|
⊢ (a)r ∈ Ideal(r){i}
BY
{ TACTIC:MemTypeCD }

1
1. r : Rng
2. a : |r|
⊢ (a)r ∈ |r| ⟶ ℙ

2
.....set predicate..... 
1. r : Rng
2. a : |r|
⊢ (a)r Ideal of r

3
.....wf..... 
1. r : Rng
2. a : |r|
3. p : |r| ⟶ ℙ
⊢ istype(p Ideal of r)

---

Latex:

---

Latex:

1.  r  :  Rng
2.  a  :  |r|
\mvdash{}  (a)r  \mmember{}  Ideal(r)\{i\}


By

---

Latex:
TACTIC:MemTypeCD

---

Home Index