This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑧 ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝐺 ‘ ( 𝑔 ↾ 𝑤 ) ) ) }