Theorem frr1

Description: Law of general well-founded recursion, part one. This theorem and the following two drop the partial order requirement from fpr1 , fpr2 , and fpr3 , which requires using the axiom of infinity. (Contributed by Scott Fenton, 11-Sep-2023)

	Ref	Expression
Hypothesis	frr.1	⊢ 𝐹 = frecs ( 𝑅 , 𝐴 , 𝐺 )
Assertion	frr1	⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 ) → 𝐹 Fn 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		frr.1	⊢ 𝐹 = frecs ( 𝑅 , 𝐴 , 𝐺 )
2		eqid	⊢ { 𝑎 ∣ ∃ 𝑏 ( 𝑎 Fn 𝑏 ∧ ( 𝑏 ⊆ 𝐴 ∧ ∀ 𝑐 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑐 ) ⊆ 𝑏 ) ∧ ∀ 𝑐 ∈ 𝑏 ( 𝑎 ‘ 𝑐 ) = ( 𝑐 𝐺 ( 𝑎 ↾ Pred ( 𝑅 , 𝐴 , 𝑐 ) ) ) ) } = { 𝑎 ∣ ∃ 𝑏 ( 𝑎 Fn 𝑏 ∧ ( 𝑏 ⊆ 𝐴 ∧ ∀ 𝑐 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑐 ) ⊆ 𝑏 ) ∧ ∀ 𝑐 ∈ 𝑏 ( 𝑎 ‘ 𝑐 ) = ( 𝑐 𝐺 ( 𝑎 ↾ Pred ( 𝑅 , 𝐴 , 𝑐 ) ) ) ) }
3	2	frrlem1	⊢ { 𝑎 ∣ ∃ 𝑏 ( 𝑎 Fn 𝑏 ∧ ( 𝑏 ⊆ 𝐴 ∧ ∀ 𝑐 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑐 ) ⊆ 𝑏 ) ∧ ∀ 𝑐 ∈ 𝑏 ( 𝑎 ‘ 𝑐 ) = ( 𝑐 𝐺 ( 𝑎 ↾ Pred ( 𝑅 , 𝐴 , 𝑐 ) ) ) ) } = { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }
4	3 1	frrlem15	⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝑔 ∈ { 𝑎 ∣ ∃ 𝑏 ( 𝑎 Fn 𝑏 ∧ ( 𝑏 ⊆ 𝐴 ∧ ∀ 𝑐 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑐 ) ⊆ 𝑏 ) ∧ ∀ 𝑐 ∈ 𝑏 ( 𝑎 ‘ 𝑐 ) = ( 𝑐 𝐺 ( 𝑎 ↾ Pred ( 𝑅 , 𝐴 , 𝑐 ) ) ) ) } ∧ ℎ ∈ { 𝑎 ∣ ∃ 𝑏 ( 𝑎 Fn 𝑏 ∧ ( 𝑏 ⊆ 𝐴 ∧ ∀ 𝑐 ∈ 𝑏 Pred ( 𝑅 , 𝐴 , 𝑐 ) ⊆ 𝑏 ) ∧ ∀ 𝑐 ∈ 𝑏 ( 𝑎 ‘ 𝑐 ) = ( 𝑐 𝐺 ( 𝑎 ↾ Pred ( 𝑅 , 𝐴 , 𝑐 ) ) ) ) } ) ) → ( ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) → 𝑢 = 𝑣 ) )
5	3 1 4	frrlem9	⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 ) → Fun 𝐹 )
6		eqid	⊢ ( ( 𝐹 ↾ Pred ( t++ ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑧 ) ) ∪ { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ) = ( ( 𝐹 ↾ Pred ( t++ ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑧 ) ) ∪ { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } )
7		simpl	⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 ) → 𝑅 Fr 𝐴 )
8		predres	⊢ Pred ( 𝑅 , 𝐴 , 𝑧 ) = Pred ( ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑧 )
9		relres	⊢ Rel ( 𝑅 ↾ 𝐴 )
10		ssttrcl	⊢ ( Rel ( 𝑅 ↾ 𝐴 ) → ( 𝑅 ↾ 𝐴 ) ⊆ t++ ( 𝑅 ↾ 𝐴 ) )
11		predrelss	⊢ ( ( 𝑅 ↾ 𝐴 ) ⊆ t++ ( 𝑅 ↾ 𝐴 ) → Pred ( ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑧 ) ⊆ Pred ( t++ ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑧 ) )
12	9 10 11	mp2b	⊢ Pred ( ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑧 ) ⊆ Pred ( t++ ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑧 )
13	8 12	eqsstri	⊢ Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ Pred ( t++ ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑧 )
14	13	a1i	⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ Pred ( t++ ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑧 ) )
15		frrlem16	⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → ∀ 𝑎 ∈ Pred ( t++ ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑧 ) Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ Pred ( t++ ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑧 ) )
16		ttrclse	⊢ ( 𝑅 Se 𝐴 → t++ ( 𝑅 ↾ 𝐴 ) Se 𝐴 )
17		setlikespec	⊢ ( ( 𝑧 ∈ 𝐴 ∧ t++ ( 𝑅 ↾ 𝐴 ) Se 𝐴 ) → Pred ( t++ ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑧 ) ∈ V )
18	17	ancoms	⊢ ( ( t++ ( 𝑅 ↾ 𝐴 ) Se 𝐴 ∧ 𝑧 ∈ 𝐴 ) → Pred ( t++ ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑧 ) ∈ V )
19	16 18	sylan	⊢ ( ( 𝑅 Se 𝐴 ∧ 𝑧 ∈ 𝐴 ) → Pred ( t++ ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑧 ) ∈ V )
20	19	adantll	⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → Pred ( t++ ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑧 ) ∈ V )
21		predss	⊢ Pred ( t++ ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑧 ) ⊆ 𝐴
22	21	a1i	⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ 𝑧 ∈ 𝐴 ) → Pred ( t++ ( 𝑅 ↾ 𝐴 ) , 𝐴 , 𝑧 ) ⊆ 𝐴 )
23		difss	⊢ ( 𝐴 ∖ dom 𝐹 ) ⊆ 𝐴
24		frmin	⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( ( 𝐴 ∖ dom 𝐹 ) ⊆ 𝐴 ∧ ( 𝐴 ∖ dom 𝐹 ) ≠ ∅ ) ) → ∃ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ )
25	23 24	mpanr1	⊢ ( ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 ) ∧ ( 𝐴 ∖ dom 𝐹 ) ≠ ∅ ) → ∃ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ )
26	3 1 4 6 7 14 15 20 22 25	frrlem14	⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 ) → dom 𝐹 = 𝐴 )
27		df-fn	⊢ ( 𝐹 Fn 𝐴 ↔ ( Fun 𝐹 ∧ dom 𝐹 = 𝐴 ) )
28	5 26 27	sylanbrc	⊢ ( ( 𝑅 Fr 𝐴 ∧ 𝑅 Se 𝐴 ) → 𝐹 Fn 𝐴 )