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

Metamath Proof Explorer

Theorem tfrlem3a

Description: Lemma for transfinite recursion. Let A be the class of "acceptable" functions. The final thing we're interested in is the union of all these acceptable functions. This lemma just changes some bound variables in A for later use. (Contributed by NM, 9-Apr-1995)

Ref Expression
Hypotheses tfrlem3.1 ⊢ 𝐴 = { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) }
tfrlem3.2 ⊢ 𝐺 ∈ V
Assertion tfrlem3a ( 𝐺 ∈ 𝐴 ↔ ∃ 𝑧 ∈ On ( 𝐺 Fn 𝑧 ∧ ∀ 𝑤 ∈ 𝑧 ( 𝐺 ‘ 𝑤 ) = ( 𝐹 ‘ ( 𝐺 ↾ 𝑤 ) ) ) )

Proof

Step Hyp Ref Expression
1 tfrlem3.1 ⊢ 𝐴 = { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) }
2 tfrlem3.2 ⊢ 𝐺 ∈ V
3 fneq12 ⊢ ( ( 𝑓 = 𝐺 ∧ 𝑥 = 𝑧 ) → ( 𝑓 Fn 𝑥 ↔ 𝐺 Fn 𝑧 ) )
4 simpll ⊢ ( ( ( 𝑓 = 𝐺 ∧ 𝑥 = 𝑧 ) ∧ 𝑦 = 𝑤 ) → 𝑓 = 𝐺 )
5 simpr ⊢ ( ( ( 𝑓 = 𝐺 ∧ 𝑥 = 𝑧 ) ∧ 𝑦 = 𝑤 ) → 𝑦 = 𝑤 )
6 4 5 fveq12d ⊢ ( ( ( 𝑓 = 𝐺 ∧ 𝑥 = 𝑧 ) ∧ 𝑦 = 𝑤 ) → ( 𝑓 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑤 ) )
7 4 5 reseq12d ⊢ ( ( ( 𝑓 = 𝐺 ∧ 𝑥 = 𝑧 ) ∧ 𝑦 = 𝑤 ) → ( 𝑓 ↾ 𝑦 ) = ( 𝐺 ↾ 𝑤 ) )
8 7 fveq2d ⊢ ( ( ( 𝑓 = 𝐺 ∧ 𝑥 = 𝑧 ) ∧ 𝑦 = 𝑤 ) → ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) = ( 𝐹 ‘ ( 𝐺 ↾ 𝑤 ) ) )
9 6 8 eqeq12d ⊢ ( ( ( 𝑓 = 𝐺 ∧ 𝑥 = 𝑧 ) ∧ 𝑦 = 𝑤 ) → ( ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ↔ ( 𝐺 ‘ 𝑤 ) = ( 𝐹 ‘ ( 𝐺 ↾ 𝑤 ) ) ) )
10 simplr ⊢ ( ( ( 𝑓 = 𝐺 ∧ 𝑥 = 𝑧 ) ∧ 𝑦 = 𝑤 ) → 𝑥 = 𝑧 )
11 9 10 cbvraldva2 ⊢ ( ( 𝑓 = 𝐺 ∧ 𝑥 = 𝑧 ) → ( ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ↔ ∀ 𝑤 ∈ 𝑧 ( 𝐺 ‘ 𝑤 ) = ( 𝐹 ‘ ( 𝐺 ↾ 𝑤 ) ) ) )
12 3 11 anbi12d ⊢ ( ( 𝑓 = 𝐺 ∧ 𝑥 = 𝑧 ) → ( ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) ↔ ( 𝐺 Fn 𝑧 ∧ ∀ 𝑤 ∈ 𝑧 ( 𝐺 ‘ 𝑤 ) = ( 𝐹 ‘ ( 𝐺 ↾ 𝑤 ) ) ) ) )
13 12 cbvrexdva ⊢ ( 𝑓 = 𝐺 → ( ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) ↔ ∃ 𝑧 ∈ On ( 𝐺 Fn 𝑧 ∧ ∀ 𝑤 ∈ 𝑧 ( 𝐺 ‘ 𝑤 ) = ( 𝐹 ‘ ( 𝐺 ↾ 𝑤 ) ) ) ) )
14 2 13 1 elab2 ⊢ ( 𝐺 ∈ 𝐴 ↔ ∃ 𝑧 ∈ On ( 𝐺 Fn 𝑧 ∧ ∀ 𝑤 ∈ 𝑧 ( 𝐺 ‘ 𝑤 ) = ( 𝐹 ‘ ( 𝐺 ↾ 𝑤 ) ) ) )