Theorem tfrlem4

Description: Lemma for transfinite recursion. A is the class of all "acceptable" functions, and F is their union. First we show that an acceptable function is in fact a function. (Contributed by NM, 9-Apr-1995)

	Ref	Expression
Hypothesis	tfrlem.1	⊢ 𝐴 = { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) }
Assertion	tfrlem4	⊢ ( 𝑔 ∈ 𝐴 → Fun 𝑔 )

Proof

Step	Hyp	Ref	Expression
1		tfrlem.1	⊢ 𝐴 = { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) }
2	1	tfrlem3	⊢ 𝐴 = { 𝑔 ∣ ∃ 𝑧 ∈ On ( 𝑔 Fn 𝑧 ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑤 ) ) ) }
3	2	abeq2i	⊢ ( 𝑔 ∈ 𝐴 ↔ ∃ 𝑧 ∈ On ( 𝑔 Fn 𝑧 ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑤 ) ) ) )
4		fnfun	⊢ ( 𝑔 Fn 𝑧 → Fun 𝑔 )
5	4	adantr	⊢ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑤 ) ) ) → Fun 𝑔 )
6	5	rexlimivw	⊢ ( ∃ 𝑧 ∈ On ( 𝑔 Fn 𝑧 ∧ ∀ 𝑤 ∈ 𝑧 ( 𝑔 ‘ 𝑤 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑤 ) ) ) → Fun 𝑔 )
7	3 6	sylbi	⊢ ( 𝑔 ∈ 𝐴 → Fun 𝑔 )