tfrlem14

Description: Lemma for transfinite recursion. Assuming ax-rep , dom recs e.V <-> recs e. V , so since dom recs is an ordinal, it must be equal to On . (Contributed by NM, 14-Aug-1994) (Revised by Mario Carneiro, 9-May-2015)

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

Proof

Step	Hyp	Ref	Expression
1		tfrlem.1	⊢ 𝐴 = { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) }
2	1	tfrlem13	⊢ ¬ recs ( 𝐹 ) ∈ V
3	1	tfrlem7	⊢ Fun recs ( 𝐹 )
4		funex	⊢ ( ( Fun recs ( 𝐹 ) ∧ dom recs ( 𝐹 ) ∈ On ) → recs ( 𝐹 ) ∈ V )
5	3 4	mpan	⊢ ( dom recs ( 𝐹 ) ∈ On → recs ( 𝐹 ) ∈ V )
6	2 5	mto	⊢ ¬ dom recs ( 𝐹 ) ∈ On
7	1	tfrlem8	⊢ Ord dom recs ( 𝐹 )
8		ordeleqon	⊢ ( Ord dom recs ( 𝐹 ) ↔ ( dom recs ( 𝐹 ) ∈ On ∨ dom recs ( 𝐹 ) = On ) )
9	7 8	mpbi	⊢ ( dom recs ( 𝐹 ) ∈ On ∨ dom recs ( 𝐹 ) = On )
10	6 9	mtpor	⊢ dom recs ( 𝐹 ) = On

Metamath Proof Explorer

Theorem tfrlem14

Proof