tfrlem6

Description: Lemma for transfinite recursion. The union of all acceptable functions is a relation. (Contributed by NM, 8-Aug-1994) (Revised by Mario Carneiro, 9-May-2015)

		Ref	Expression
	Hypothesis	tfrlem.1	⊢ 𝐴 = { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) }
	Assertion	tfrlem6	⊢ Rel recs ( 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		tfrlem.1	⊢ 𝐴 = { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) }
2		reluni	⊢ ( Rel ∪ 𝐴 ↔ ∀ 𝑔 ∈ 𝐴 Rel 𝑔 )
3	1	tfrlem4	⊢ ( 𝑔 ∈ 𝐴 → Fun 𝑔 )
4		funrel	⊢ ( Fun 𝑔 → Rel 𝑔 )
5	3 4	syl	⊢ ( 𝑔 ∈ 𝐴 → Rel 𝑔 )
6	2 5	mprgbir	⊢ Rel ∪ 𝐴
7	1	recsfval	⊢ recs ( 𝐹 ) = ∪ 𝐴
8	7	releqi	⊢ ( Rel recs ( 𝐹 ) ↔ Rel ∪ 𝐴 )
9	6 8	mpbir	⊢ Rel recs ( 𝐹 )

Metamath Proof Explorer

Theorem tfrlem6

Proof