Theorem bnj579

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	bnj579.1	⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
	bnj579.2	⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
	bnj579.3	⊢ 𝐷 = ( ω ∖ { ∅ } )
Assertion	bnj579	⊢ ( 𝑛 ∈ 𝐷 → ∃* 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		bnj579.1	⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑥 , 𝐴 , 𝑅 ) )
2		bnj579.2	⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
3		bnj579.3	⊢ 𝐷 = ( ω ∖ { ∅ } )
4		biid	⊢ ( ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ↔ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
5		biid	⊢ ( [ 𝑔 / 𝑓 ] 𝜑 ↔ [ 𝑔 / 𝑓 ] 𝜑 )
6		biid	⊢ ( [ 𝑔 / 𝑓 ] 𝜓 ↔ [ 𝑔 / 𝑓 ] 𝜓 )
7		biid	⊢ ( [ 𝑔 / 𝑓 ] ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ↔ [ 𝑔 / 𝑓 ] ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
8		biid	⊢ ( ( ( 𝑛 ∈ 𝐷 ∧ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ∧ [ 𝑔 / 𝑓 ] ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) → ( 𝑓 ‘ 𝑗 ) = ( 𝑔 ‘ 𝑗 ) ) ↔ ( ( 𝑛 ∈ 𝐷 ∧ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ∧ [ 𝑔 / 𝑓 ] ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) → ( 𝑓 ‘ 𝑗 ) = ( 𝑔 ‘ 𝑗 ) ) )
9		biid	⊢ ( ∀ 𝑘 ∈ 𝑛 ( 𝑘 E 𝑗 → [ 𝑘 / 𝑗 ] ( ( 𝑛 ∈ 𝐷 ∧ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ∧ [ 𝑔 / 𝑓 ] ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) → ( 𝑓 ‘ 𝑗 ) = ( 𝑔 ‘ 𝑗 ) ) ) ↔ ∀ 𝑘 ∈ 𝑛 ( 𝑘 E 𝑗 → [ 𝑘 / 𝑗 ] ( ( 𝑛 ∈ 𝐷 ∧ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ∧ [ 𝑔 / 𝑓 ] ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) ) → ( 𝑓 ‘ 𝑗 ) = ( 𝑔 ‘ 𝑗 ) ) ) )
10	1 2 4 5 6 7 3 8 9	bnj580	⊢ ( 𝑛 ∈ 𝐷 → ∃* 𝑓 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )