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 ( 𝑦 , 𝐴 , 𝑅 ) )