Theorem rdglem1

Description: Lemma used with the recursive definition generator. This is a trivial lemma that just changes bound variables for later use. (Contributed by NM, 9-Apr-1995)

	Ref	Expression
Assertion	rdglem1	⊢ { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ 𝑦 ) ) ) } = { 𝑔 ∣ ∃ 𝑧 ∈ On ( 𝑔 Fn 𝑧 ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝐺 ‘ ( 𝑔 ↾ 𝑤 ) ) ) }

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ 𝑦 ) ) ) } = { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ 𝑦 ) ) ) }
2	1	tfrlem3	⊢ { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ 𝑦 ) ) ) } = { 𝑔 ∣ ∃ 𝑧 ∈ On ( 𝑔 Fn 𝑧 ∧ ∀ 𝑣 ∈ 𝑧 ( 𝑔 ‘ 𝑣 ) = ( 𝐺 ‘ ( 𝑔 ↾ 𝑣 ) ) ) }
3		fveq2	⊢ ( 𝑣 = 𝑤 → ( 𝑔 ‘ 𝑣 ) = ( 𝑔 ‘ 𝑤 ) )
4		reseq2	⊢ ( 𝑣 = 𝑤 → ( 𝑔 ↾ 𝑣 ) = ( 𝑔 ↾ 𝑤 ) )
5	4	fveq2d	⊢ ( 𝑣 = 𝑤 → ( 𝐺 ‘ ( 𝑔 ↾ 𝑣 ) ) = ( 𝐺 ‘ ( 𝑔 ↾ 𝑤 ) ) )
6	3 5	eqeq12d	⊢ ( 𝑣 = 𝑤 → ( ( 𝑔 ‘ 𝑣 ) = ( 𝐺 ‘ ( 𝑔 ↾ 𝑣 ) ) ↔ ( 𝑔 ‘ 𝑤 ) = ( 𝐺 ‘ ( 𝑔 ↾ 𝑤 ) ) ) )
7	6	cbvralvw	⊢ ( ∀ 𝑣 ∈ 𝑧 ( 𝑔 ‘ 𝑣 ) = ( 𝐺 ‘ ( 𝑔 ↾ 𝑣 ) ) ↔ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝐺 ‘ ( 𝑔 ↾ 𝑤 ) ) )
8	7	anbi2i	⊢ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑣 ∈ 𝑧 ( 𝑔 ‘ 𝑣 ) = ( 𝐺 ‘ ( 𝑔 ↾ 𝑣 ) ) ) ↔ ( 𝑔 Fn 𝑧 ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝐺 ‘ ( 𝑔 ↾ 𝑤 ) ) ) )
9	8	rexbii	⊢ ( ∃ 𝑧 ∈ On ( 𝑔 Fn 𝑧 ∧ ∀ 𝑣 ∈ 𝑧 ( 𝑔 ‘ 𝑣 ) = ( 𝐺 ‘ ( 𝑔 ↾ 𝑣 ) ) ) ↔ ∃ 𝑧 ∈ On ( 𝑔 Fn 𝑧 ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝐺 ‘ ( 𝑔 ↾ 𝑤 ) ) ) )
10	9	abbii	⊢ { 𝑔 ∣ ∃ 𝑧 ∈ On ( 𝑔 Fn 𝑧 ∧ ∀ 𝑣 ∈ 𝑧 ( 𝑔 ‘ 𝑣 ) = ( 𝐺 ‘ ( 𝑔 ↾ 𝑣 ) ) ) } = { 𝑔 ∣ ∃ 𝑧 ∈ On ( 𝑔 Fn 𝑧 ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝐺 ‘ ( 𝑔 ↾ 𝑤 ) ) ) }
11	2 10	eqtri	⊢ { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑓 ↾ 𝑦 ) ) ) } = { 𝑔 ∣ ∃ 𝑧 ∈ On ( 𝑔 Fn 𝑧 ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝐺 ‘ ( 𝑔 ↾ 𝑤 ) ) ) }