Theorem bnj953

Description: Technical lemma for bnj69 . 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	bnj953.1	⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
	bnj953.2	⊢ ( ( 𝐺 ‘ 𝑖 ) = ( 𝑓 ‘ 𝑖 ) → ∀ 𝑦 ( 𝐺 ‘ 𝑖 ) = ( 𝑓 ‘ 𝑖 ) )
Assertion	bnj953	⊢ ( ( ( 𝐺 ‘ 𝑖 ) = ( 𝑓 ‘ 𝑖 ) ∧ ( 𝐺 ‘ suc 𝑖 ) = ( 𝑓 ‘ suc 𝑖 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ) ∧ 𝜓 ) → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		bnj953.1	⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
2		bnj953.2	⊢ ( ( 𝐺 ‘ 𝑖 ) = ( 𝑓 ‘ 𝑖 ) → ∀ 𝑦 ( 𝐺 ‘ 𝑖 ) = ( 𝑓 ‘ 𝑖 ) )
3		bnj312	⊢ ( ( ( 𝐺 ‘ 𝑖 ) = ( 𝑓 ‘ 𝑖 ) ∧ ( 𝐺 ‘ suc 𝑖 ) = ( 𝑓 ‘ suc 𝑖 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ) ∧ 𝜓 ) ↔ ( ( 𝐺 ‘ suc 𝑖 ) = ( 𝑓 ‘ suc 𝑖 ) ∧ ( 𝐺 ‘ 𝑖 ) = ( 𝑓 ‘ 𝑖 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ) ∧ 𝜓 ) )
4		bnj251	⊢ ( ( ( 𝐺 ‘ suc 𝑖 ) = ( 𝑓 ‘ suc 𝑖 ) ∧ ( 𝐺 ‘ 𝑖 ) = ( 𝑓 ‘ 𝑖 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ) ∧ 𝜓 ) ↔ ( ( 𝐺 ‘ suc 𝑖 ) = ( 𝑓 ‘ suc 𝑖 ) ∧ ( ( 𝐺 ‘ 𝑖 ) = ( 𝑓 ‘ 𝑖 ) ∧ ( ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ) ∧ 𝜓 ) ) ) )
5	3 4	bitri	⊢ ( ( ( 𝐺 ‘ 𝑖 ) = ( 𝑓 ‘ 𝑖 ) ∧ ( 𝐺 ‘ suc 𝑖 ) = ( 𝑓 ‘ suc 𝑖 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ) ∧ 𝜓 ) ↔ ( ( 𝐺 ‘ suc 𝑖 ) = ( 𝑓 ‘ suc 𝑖 ) ∧ ( ( 𝐺 ‘ 𝑖 ) = ( 𝑓 ‘ 𝑖 ) ∧ ( ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ) ∧ 𝜓 ) ) ) )
6	1	bnj115	⊢ ( 𝜓 ↔ ∀ 𝑖 ( ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ) → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
7		sp	⊢ ( ∀ 𝑖 ( ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ) → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) → ( ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ) → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
8	7	impcom	⊢ ( ( ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ) ∧ ∀ 𝑖 ( ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ) → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) ) → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
9	6 8	sylan2b	⊢ ( ( ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ) ∧ 𝜓 ) → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
10	2	bnj956	⊢ ( ( 𝐺 ‘ 𝑖 ) = ( 𝑓 ‘ 𝑖 ) → ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
11		eqtr3	⊢ ( ( ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ∧ ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
12	9 10 11	syl2anr	⊢ ( ( ( 𝐺 ‘ 𝑖 ) = ( 𝑓 ‘ 𝑖 ) ∧ ( ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ) ∧ 𝜓 ) ) → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
13		eqtr	⊢ ( ( ( 𝐺 ‘ suc 𝑖 ) = ( 𝑓 ‘ suc 𝑖 ) ∧ ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
14	12 13	sylan2	⊢ ( ( ( 𝐺 ‘ suc 𝑖 ) = ( 𝑓 ‘ suc 𝑖 ) ∧ ( ( 𝐺 ‘ 𝑖 ) = ( 𝑓 ‘ 𝑖 ) ∧ ( ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ) ∧ 𝜓 ) ) ) → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )
15	5 14	sylbi	⊢ ( ( ( 𝐺 ‘ 𝑖 ) = ( 𝑓 ‘ 𝑖 ) ∧ ( 𝐺 ‘ suc 𝑖 ) = ( 𝑓 ‘ suc 𝑖 ) ∧ ( 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑛 ) ∧ 𝜓 ) → ( 𝐺 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝐺 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) )