This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bnj98

Description: Technical lemma for bnj150 . 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
Assertion bnj98 ⊢ ∀ i ∈ ω suc ⁡ i ∈ 1 𝑜 → F ⁡ suc ⁡ i = ⋃ y ∈ F ⁡ i pred y A R

Proof

Step Hyp Ref Expression
1 vex ⊢ i ∈ V
2 1 sucid ⊢ i ∈ suc ⁡ i
3 2 n0ii ⊢ ¬ suc ⁡ i = ∅
4 df-suc ⊢ suc ⁡ i = i ∪ i
5 df-un ⊢ i ∪ i = x | x ∈ i ∨ x ∈ i
6 4 5 eqtri ⊢ suc ⁡ i = x | x ∈ i ∨ x ∈ i
7 df1o2 ⊢ 1 𝑜 = ∅
8 6 7 eleq12i ⊢ suc ⁡ i ∈ 1 𝑜 ↔ x | x ∈ i ∨ x ∈ i ∈ ∅
9 elsni ⊢ x | x ∈ i ∨ x ∈ i ∈ ∅ → x | x ∈ i ∨ x ∈ i = ∅
10 8 9 sylbi ⊢ suc ⁡ i ∈ 1 𝑜 → x | x ∈ i ∨ x ∈ i = ∅
11 6 10 eqtrid ⊢ suc ⁡ i ∈ 1 𝑜 → suc ⁡ i = ∅
12 3 11 mto ⊢ ¬ suc ⁡ i ∈ 1 𝑜
13 12 pm2.21i ⊢ suc ⁡ i ∈ 1 𝑜 → F ⁡ suc ⁡ i = ⋃ y ∈ F ⁡ i pred y A R
14 13 rgenw ⊢ ∀ i ∈ ω suc ⁡ i ∈ 1 𝑜 → F ⁡ suc ⁡ i = ⋃ y ∈ F ⁡ i pred y A R