Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Jonathan Ben-Naim
Well founded induction and recursion
bnj589
Metamath Proof Explorer
Description: Technical lemma for bnj852 . This lemma may no longer be used or have
become an indirect lemma of the theorem in question (i.e. a lemma of a
lemma... of the theorem). (Contributed by Jonathan Ben-Naim , 3-Jun-2011) (New usage is discouraged.)
Ref
Expression
Hypothesis
bnj589.1
⊢ ψ ↔ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R
Assertion
bnj589
⊢ ψ ↔ ∀ k ∈ ω suc ⁡ k ∈ n → f ⁡ suc ⁡ k = ⋃ y ∈ f ⁡ k pred y A R
Proof
Step
Hyp
Ref
Expression
1
bnj589.1
⊢ ψ ↔ ∀ i ∈ ω suc ⁡ i ∈ n → f ⁡ suc ⁡ i = ⋃ y ∈ f ⁡ i pred y A R
2
1
bnj222
⊢ ψ ↔ ∀ k ∈ ω suc ⁡ k ∈ n → f ⁡ suc ⁡ k = ⋃ y ∈ f ⁡ k pred y A R