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 ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝐹 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )

Proof

Step Hyp Ref Expression
1 vex ⊢ 𝑖 ∈ V
2 1 sucid ⊢ 𝑖 ∈ suc 𝑖
3 2 n0ii ⊢ ¬ suc 𝑖 = ∅
4 df-suc ⊢ suc 𝑖 = ( 𝑖 ∪ { 𝑖 } )
5 df-un ⊢ ( 𝑖 ∪ { 𝑖 } ) = { 𝑥 ∣ ( 𝑥 ∈ 𝑖 ∨ 𝑥 ∈ { 𝑖 } ) }
6 4 5 eqtri ⊢ suc 𝑖 = { 𝑥 ∣ ( 𝑥 ∈ 𝑖 ∨ 𝑥 ∈ { 𝑖 } ) }
7 df1o2 ⊢ 1o = { ∅ }
8 6 7 eleq12i ⊢ ( suc 𝑖 ∈ 1o ↔ { 𝑥 ∣ ( 𝑥 ∈ 𝑖 ∨ 𝑥 ∈ { 𝑖 } ) } ∈ { ∅ } )
9 elsni ⊢ ( { 𝑥 ∣ ( 𝑥 ∈ 𝑖 ∨ 𝑥 ∈ { 𝑖 } ) } ∈ { ∅ } → { 𝑥 ∣ ( 𝑥 ∈ 𝑖 ∨ 𝑥 ∈ { 𝑖 } ) } = ∅ )
10 8 9 sylbi ⊢ ( suc 𝑖 ∈ 1o → { 𝑥 ∣ ( 𝑥 ∈ 𝑖 ∨ 𝑥 ∈ { 𝑖 } ) } = ∅ )
11 6 10 eqtrid ⊢ ( suc 𝑖 ∈ 1o → suc 𝑖 = ∅ )
12 3 11 mto ⊢ ¬ suc 𝑖 ∈ 1o
13 12 pm2.21i ⊢ ( suc 𝑖 ∈ 1o → ( 𝐹 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
14 13 rgenw ⊢ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝐹 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )