frrdmcl

Description: Show without using the axiom of replacement that for a "function" defined by well-founded recursion, the predecessor class of an element of its domain is a subclass of its domain. (Contributed by Scott Fenton, 21-Apr-2011) (Proof shortened by Scott Fenton, 17-Nov-2024)

		Ref	Expression
	Hypothesis	frrrel.1	⊢ 𝐹 = frecs ( 𝑅 , 𝐴 , 𝐺 )
	Assertion	frrdmcl	⊢ ( 𝑋 ∈ dom 𝐹 → Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ dom 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		frrrel.1	⊢ 𝐹 = frecs ( 𝑅 , 𝐴 , 𝐺 )
2		predeq3	⊢ ( 𝑧 = 𝑋 → Pred ( 𝑅 , 𝐴 , 𝑧 ) = Pred ( 𝑅 , 𝐴 , 𝑋 ) )
3	2	sseq1d	⊢ ( 𝑧 = 𝑋 → ( Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ dom 𝐹 ↔ Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ dom 𝐹 ) )
4		eqid	⊢ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } = { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }
5	4 1	frrlem8	⊢ ( 𝑧 ∈ dom 𝐹 → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ dom 𝐹 )
6	3 5	vtoclga	⊢ ( 𝑋 ∈ dom 𝐹 → Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ dom 𝐹 )

Metamath Proof Explorer

Theorem frrdmcl

Proof