Theorem bnj126

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
Hypotheses	bnj126.1	⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
	bnj126.2	⊢ ( 𝜓′ ↔ [ 1o / 𝑛 ] 𝜓 )
	bnj126.3	⊢ ( 𝜓″ ↔ [ 𝐹 / 𝑓 ] 𝜓′ )
	bnj126.4	⊢ 𝐹 = { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ }
Assertion	bnj126	⊢ ( 𝜓″ ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝐹 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )

Proof

Step	Hyp	Ref	Expression
1		bnj126.1	⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
2		bnj126.2	⊢ ( 𝜓′ ↔ [ 1o / 𝑛 ] 𝜓 )
3		bnj126.3	⊢ ( 𝜓″ ↔ [ 𝐹 / 𝑓 ] 𝜓′ )
4		bnj126.4	⊢ 𝐹 = { ⟨ ∅ , pred ( 𝑥 , 𝐴 , 𝑅 ) ⟩ }
5	2	sbcbii	⊢ ( [ 𝐹 / 𝑓 ] 𝜓′ ↔ [ 𝐹 / 𝑓 ] [ 1o / 𝑛 ] 𝜓 )
6	4	bnj95	⊢ 𝐹 ∈ V
7	1 6	bnj106	⊢ ( [ 𝐹 / 𝑓 ] [ 1o / 𝑛 ] 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝐹 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
8	3 5 7	3bitri	⊢ ( 𝜓″ ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 1o → ( 𝐹 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )