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 ⊢ f | ∃ x ∈ On f Fn x ∧ ∀ y ∈ x f ⁡ y = G ⁡ f ↾ y = g | ∃ z ∈ On g Fn z ∧ ∀ w ∈ z g ⁡ w = G ⁡ g ↾ w

Proof

Step Hyp Ref Expression
1 eqid ⊢ f | ∃ x ∈ On f Fn x ∧ ∀ y ∈ x f ⁡ y = G ⁡ f ↾ y = f | ∃ x ∈ On f Fn x ∧ ∀ y ∈ x f ⁡ y = G ⁡ f ↾ y
2 1 tfrlem3 ⊢ f | ∃ x ∈ On f Fn x ∧ ∀ y ∈ x f ⁡ y = G ⁡ f ↾ y = g | ∃ z ∈ On g Fn z ∧ ∀ v ∈ z g ⁡ v = G ⁡ g ↾ v
3 fveq2 ⊢ v = w → g ⁡ v = g ⁡ w
4 reseq2 ⊢ v = w → g ↾ v = g ↾ w
5 4 fveq2d ⊢ v = w → G ⁡ g ↾ v = G ⁡ g ↾ w
6 3 5 eqeq12d ⊢ v = w → g ⁡ v = G ⁡ g ↾ v ↔ g ⁡ w = G ⁡ g ↾ w
7 6 cbvralvw ⊢ ∀ v ∈ z g ⁡ v = G ⁡ g ↾ v ↔ ∀ w ∈ z g ⁡ w = G ⁡ g ↾ w
8 7 anbi2i ⊢ g Fn z ∧ ∀ v ∈ z g ⁡ v = G ⁡ g ↾ v ↔ g Fn z ∧ ∀ w ∈ z g ⁡ w = G ⁡ g ↾ w
9 8 rexbii ⊢ ∃ z ∈ On g Fn z ∧ ∀ v ∈ z g ⁡ v = G ⁡ g ↾ v ↔ ∃ z ∈ On g Fn z ∧ ∀ w ∈ z g ⁡ w = G ⁡ g ↾ w
10 9 abbii ⊢ g | ∃ z ∈ On g Fn z ∧ ∀ v ∈ z g ⁡ v = G ⁡ g ↾ v = g | ∃ z ∈ On g Fn z ∧ ∀ w ∈ z g ⁡ w = G ⁡ g ↾ w
11 2 10 eqtri ⊢ f | ∃ x ∈ On f Fn x ∧ ∀ y ∈ x f ⁡ y = G ⁡ f ↾ y = g | ∃ z ∈ On g Fn z ∧ ∀ w ∈ z g ⁡ w = G ⁡ g ↾ w