Metamath Proof Explorer


Theorem fpr1

Description: Law of well-founded recursion over a partial order, part one. Establish the functionality and domain of the recursive function generator. Note that by requiring a partial order we can avoid using the axiom of infinity. (Contributed by Scott Fenton, 11-Sep-2023)

Ref Expression
Hypothesis fprr.1 𝐹 = frecs ( 𝑅 , 𝐴 , 𝐺 )
Assertion fpr1 ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) → 𝐹 Fn 𝐴 )

Proof

Step Hyp Ref Expression
1 fprr.1 𝐹 = frecs ( 𝑅 , 𝐴 , 𝐺 )
2 eqid { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥𝐴 ∧ ∀ 𝑦𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦𝑥 ( 𝑓𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } = { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥𝐴 ∧ ∀ 𝑦𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦𝑥 ( 𝑓𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }
3 2 frrlem1 { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥𝐴 ∧ ∀ 𝑦𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦𝑥 ( 𝑓𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } = { 𝑎 ∣ ∃ 𝑏 ( 𝑎 Fn 𝑏 ∧ ( 𝑏𝐴 ∧ ∀ 𝑐𝑏 Pred ( 𝑅 , 𝐴 , 𝑐 ) ⊆ 𝑏 ) ∧ ∀ 𝑐𝑏 ( 𝑎𝑐 ) = ( 𝑐 𝐺 ( 𝑎 ↾ Pred ( 𝑅 , 𝐴 , 𝑐 ) ) ) ) }
4 3 1 fprlem1 ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ ( 𝑔 ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥𝐴 ∧ ∀ 𝑦𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦𝑥 ( 𝑓𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ∧ ∈ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥𝐴 ∧ ∀ 𝑦𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦𝑥 ( 𝑓𝑦 ) = ( 𝑦 𝐺 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) } ) ) → ( ( 𝑏 𝑔 𝑢𝑏 𝑣 ) → 𝑢 = 𝑣 ) )
5 3 1 4 frrlem9 ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) → Fun 𝐹 )
6 eqid ( ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ∪ { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } ) = ( ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ∪ { ⟨ 𝑧 , ( 𝑧 𝐺 ( 𝐹 ↾ Pred ( 𝑅 , 𝐴 , 𝑧 ) ) ) ⟩ } )
7 simp1 ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) → 𝑅 Fr 𝐴 )
8 ssidd ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ 𝑧𝐴 ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ Pred ( 𝑅 , 𝐴 , 𝑧 ) )
9 fprlem2 ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ 𝑧𝐴 ) → ∀ 𝑦 ∈ Pred ( 𝑅 , 𝐴 , 𝑧 ) Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ Pred ( 𝑅 , 𝐴 , 𝑧 ) )
10 setlikespec ( ( 𝑧𝐴𝑅 Se 𝐴 ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ∈ V )
11 10 ancoms ( ( 𝑅 Se 𝐴𝑧𝐴 ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ∈ V )
12 11 3ad2antl3 ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ 𝑧𝐴 ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ∈ V )
13 predss Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝐴
14 13 a1i ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ 𝑧𝐴 ) → Pred ( 𝑅 , 𝐴 , 𝑧 ) ⊆ 𝐴 )
15 difssd ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ ( 𝐴 ∖ dom 𝐹 ) ≠ ∅ ) → ( 𝐴 ∖ dom 𝐹 ) ⊆ 𝐴 )
16 simpr ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ ( 𝐴 ∖ dom 𝐹 ) ≠ ∅ ) → ( 𝐴 ∖ dom 𝐹 ) ≠ ∅ )
17 15 16 jca ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ ( 𝐴 ∖ dom 𝐹 ) ≠ ∅ ) → ( ( 𝐴 ∖ dom 𝐹 ) ⊆ 𝐴 ∧ ( 𝐴 ∖ dom 𝐹 ) ≠ ∅ ) )
18 frpomin2 ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ ( ( 𝐴 ∖ dom 𝐹 ) ⊆ 𝐴 ∧ ( 𝐴 ∖ dom 𝐹 ) ≠ ∅ ) ) → ∃ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ )
19 17 18 syldan ( ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) ∧ ( 𝐴 ∖ dom 𝐹 ) ≠ ∅ ) → ∃ 𝑧 ∈ ( 𝐴 ∖ dom 𝐹 ) Pred ( 𝑅 , ( 𝐴 ∖ dom 𝐹 ) , 𝑧 ) = ∅ )
20 3 1 4 6 7 8 9 12 14 19 frrlem14 ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) → dom 𝐹 = 𝐴 )
21 df-fn ( 𝐹 Fn 𝐴 ↔ ( Fun 𝐹 ∧ dom 𝐹 = 𝐴 ) )
22 5 20 21 sylanbrc ( ( 𝑅 Fr 𝐴𝑅 Po 𝐴𝑅 Se 𝐴 ) → 𝐹 Fn 𝐴 )