Theorem tfrlem10

Description: Lemma for transfinite recursion. We define class C by extending recs with one ordered pair. We will assume, falsely, that domain of recs is a member of, and thus not equal to, On . Using this assumption we will prove facts about C that will lead to a contradiction in tfrlem14 , thus showing the domain of recs does in fact equal On . Here we show (under the false assumption) that C is a function extending the domain of recs ( F ) by one. (Contributed by NM, 14-Aug-1994) (Revised by Mario Carneiro, 9-May-2015)

	Ref	Expression
Hypotheses	tfrlem.1	⊢ 𝐴 = { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) }
	tfrlem.3	⊢ 𝐶 = ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } )
Assertion	tfrlem10	⊢ ( dom recs ( 𝐹 ) ∈ On → 𝐶 Fn suc dom recs ( 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		tfrlem.1	⊢ 𝐴 = { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) }
2		tfrlem.3	⊢ 𝐶 = ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } )
3		fvex	⊢ ( 𝐹 ‘ recs ( 𝐹 ) ) ∈ V
4		funsng	⊢ ( ( dom recs ( 𝐹 ) ∈ On ∧ ( 𝐹 ‘ recs ( 𝐹 ) ) ∈ V ) → Fun { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } )
5	3 4	mpan2	⊢ ( dom recs ( 𝐹 ) ∈ On → Fun { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } )
6	1	tfrlem7	⊢ Fun recs ( 𝐹 )
7	5 6	jctil	⊢ ( dom recs ( 𝐹 ) ∈ On → ( Fun recs ( 𝐹 ) ∧ Fun { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) )
8	3	dmsnop	⊢ dom { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } = { dom recs ( 𝐹 ) }
9	8	ineq2i	⊢ ( dom recs ( 𝐹 ) ∩ dom { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) = ( dom recs ( 𝐹 ) ∩ { dom recs ( 𝐹 ) } )
10	1	tfrlem8	⊢ Ord dom recs ( 𝐹 )
11		orddisj	⊢ ( Ord dom recs ( 𝐹 ) → ( dom recs ( 𝐹 ) ∩ { dom recs ( 𝐹 ) } ) = ∅ )
12	10 11	ax-mp	⊢ ( dom recs ( 𝐹 ) ∩ { dom recs ( 𝐹 ) } ) = ∅
13	9 12	eqtri	⊢ ( dom recs ( 𝐹 ) ∩ dom { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) = ∅
14		funun	⊢ ( ( ( Fun recs ( 𝐹 ) ∧ Fun { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) ∧ ( dom recs ( 𝐹 ) ∩ dom { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) = ∅ ) → Fun ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) )
15	7 13 14	sylancl	⊢ ( dom recs ( 𝐹 ) ∈ On → Fun ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) )
16	8	uneq2i	⊢ ( dom recs ( 𝐹 ) ∪ dom { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) = ( dom recs ( 𝐹 ) ∪ { dom recs ( 𝐹 ) } )
17		dmun	⊢ dom ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) = ( dom recs ( 𝐹 ) ∪ dom { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } )
18		df-suc	⊢ suc dom recs ( 𝐹 ) = ( dom recs ( 𝐹 ) ∪ { dom recs ( 𝐹 ) } )
19	16 17 18	3eqtr4i	⊢ dom ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) = suc dom recs ( 𝐹 )
20		df-fn	⊢ ( ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) Fn suc dom recs ( 𝐹 ) ↔ ( Fun ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) ∧ dom ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) = suc dom recs ( 𝐹 ) ) )
21	15 19 20	sylanblrc	⊢ ( dom recs ( 𝐹 ) ∈ On → ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) Fn suc dom recs ( 𝐹 ) )
22	2	fneq1i	⊢ ( 𝐶 Fn suc dom recs ( 𝐹 ) ↔ ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) Fn suc dom recs ( 𝐹 ) )
23	21 22	sylibr	⊢ ( dom recs ( 𝐹 ) ∈ On → 𝐶 Fn suc dom recs ( 𝐹 ) )