Theorem tfrlem13

Description: Lemma for transfinite recursion. If recs is a set function, then C is acceptable, and thus a subset of recs , but dom C is bigger than dom recs . This is a contradiction, so recs must be a proper class function. (Contributed by NM, 14-Aug-1994) (Revised by Mario Carneiro, 14-Nov-2014)

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

Proof

Step	Hyp	Ref	Expression
1		tfrlem.1	⊢ 𝐴 = { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) }
2	1	tfrlem8	⊢ Ord dom recs ( 𝐹 )
3		ordirr	⊢ ( Ord dom recs ( 𝐹 ) → ¬ dom recs ( 𝐹 ) ∈ dom recs ( 𝐹 ) )
4	2 3	ax-mp	⊢ ¬ dom recs ( 𝐹 ) ∈ dom recs ( 𝐹 )
5		eqid	⊢ ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) = ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } )
6	1 5	tfrlem12	⊢ ( recs ( 𝐹 ) ∈ V → ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) ∈ 𝐴 )
7		elssuni	⊢ ( ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) ∈ 𝐴 → ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) ⊆ ∪ 𝐴 )
8	1	recsfval	⊢ recs ( 𝐹 ) = ∪ 𝐴
9	7 8	sseqtrrdi	⊢ ( ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) ∈ 𝐴 → ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) ⊆ recs ( 𝐹 ) )
10		dmss	⊢ ( ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) ⊆ recs ( 𝐹 ) → dom ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) ⊆ dom recs ( 𝐹 ) )
11	6 9 10	3syl	⊢ ( recs ( 𝐹 ) ∈ V → dom ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) ⊆ dom recs ( 𝐹 ) )
12	2	a1i	⊢ ( recs ( 𝐹 ) ∈ V → Ord dom recs ( 𝐹 ) )
13		dmexg	⊢ ( recs ( 𝐹 ) ∈ V → dom recs ( 𝐹 ) ∈ V )
14		elon2	⊢ ( dom recs ( 𝐹 ) ∈ On ↔ ( Ord dom recs ( 𝐹 ) ∧ dom recs ( 𝐹 ) ∈ V ) )
15	12 13 14	sylanbrc	⊢ ( recs ( 𝐹 ) ∈ V → dom recs ( 𝐹 ) ∈ On )
16		sucidg	⊢ ( dom recs ( 𝐹 ) ∈ On → dom recs ( 𝐹 ) ∈ suc dom recs ( 𝐹 ) )
17	15 16	syl	⊢ ( recs ( 𝐹 ) ∈ V → dom recs ( 𝐹 ) ∈ suc dom recs ( 𝐹 ) )
18	1 5	tfrlem10	⊢ ( dom recs ( 𝐹 ) ∈ On → ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) Fn suc dom recs ( 𝐹 ) )
19		fndm	⊢ ( ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) Fn suc dom recs ( 𝐹 ) → dom ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) = suc dom recs ( 𝐹 ) )
20	15 18 19	3syl	⊢ ( recs ( 𝐹 ) ∈ V → dom ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) = suc dom recs ( 𝐹 ) )
21	17 20	eleqtrrd	⊢ ( recs ( 𝐹 ) ∈ V → dom recs ( 𝐹 ) ∈ dom ( recs ( 𝐹 ) ∪ { ⟨ dom recs ( 𝐹 ) , ( 𝐹 ‘ recs ( 𝐹 ) ) ⟩ } ) )
22	11 21	sseldd	⊢ ( recs ( 𝐹 ) ∈ V → dom recs ( 𝐹 ) ∈ dom recs ( 𝐹 ) )
23	4 22	mto	⊢ ¬ recs ( 𝐹 ) ∈ V