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