Theorem bnj539

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
Hypotheses	bnj539.1	⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝐹 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
	bnj539.2	⊢ ( 𝜓′ ↔ [ 𝑀 / 𝑛 ] 𝜓 )
	bnj539.3	⊢ 𝑀 ∈ V
Assertion	bnj539	⊢ ( 𝜓′ ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑀 → ( 𝐹 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )

Proof

Step	Hyp	Ref	Expression
1		bnj539.1	⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝐹 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
2		bnj539.2	⊢ ( 𝜓′ ↔ [ 𝑀 / 𝑛 ] 𝜓 )
3		bnj539.3	⊢ 𝑀 ∈ V
4	1	sbcbii	⊢ ( [ 𝑀 / 𝑛 ] 𝜓 ↔ [ 𝑀 / 𝑛 ] ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝐹 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
5	3	bnj538	⊢ ( [ 𝑀 / 𝑛 ] ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝐹 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ∀ 𝑖 ∈ ω [ 𝑀 / 𝑛 ] ( suc 𝑖 ∈ 𝑛 → ( 𝐹 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
6		sbcimg	⊢ ( 𝑀 ∈ V → ( [ 𝑀 / 𝑛 ] ( suc 𝑖 ∈ 𝑛 → ( 𝐹 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ( [ 𝑀 / 𝑛 ] suc 𝑖 ∈ 𝑛 → [ 𝑀 / 𝑛 ] ( 𝐹 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) )
7	3 6	ax-mp	⊢ ( [ 𝑀 / 𝑛 ] ( suc 𝑖 ∈ 𝑛 → ( 𝐹 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ( [ 𝑀 / 𝑛 ] suc 𝑖 ∈ 𝑛 → [ 𝑀 / 𝑛 ] ( 𝐹 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
8		sbcel2gv	⊢ ( 𝑀 ∈ V → ( [ 𝑀 / 𝑛 ] suc 𝑖 ∈ 𝑛 ↔ suc 𝑖 ∈ 𝑀 ) )
9	3 8	ax-mp	⊢ ( [ 𝑀 / 𝑛 ] suc 𝑖 ∈ 𝑛 ↔ suc 𝑖 ∈ 𝑀 )
10	3	bnj525	⊢ ( [ 𝑀 / 𝑛 ] ( 𝐹 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ↔ ( 𝐹 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
11	9 10	imbi12i	⊢ ( ( [ 𝑀 / 𝑛 ] suc 𝑖 ∈ 𝑛 → [ 𝑀 / 𝑛 ] ( 𝐹 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ( suc 𝑖 ∈ 𝑀 → ( 𝐹 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
12	7 11	bitri	⊢ ( [ 𝑀 / 𝑛 ] ( suc 𝑖 ∈ 𝑛 → ( 𝐹 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ( suc 𝑖 ∈ 𝑀 → ( 𝐹 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
13	12	ralbii	⊢ ( ∀ 𝑖 ∈ ω [ 𝑀 / 𝑛 ] ( suc 𝑖 ∈ 𝑛 → ( 𝐹 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑀 → ( 𝐹 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
14	5 13	bitri	⊢ ( [ 𝑀 / 𝑛 ] ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝐹 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑀 → ( 𝐹 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
15	4 14	bitri	⊢ ( [ 𝑀 / 𝑛 ] 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑀 → ( 𝐹 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
16	2 15	bitri	⊢ ( 𝜓′ ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑀 → ( 𝐹 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐹 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )