This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-frecs

Description: This is the definition for the well-founded recursion generator. Similar to df-wrecs and df-recs , it is a direct definition form of normally recursive relationships. Unlike the former two definitions, it only requires a well-founded set-like relationship for its properties, not a well-ordered relationship. This proof requires either a partial order or the axiom of infinity. We develop the theorems twice, once with a partial order and once without. The second development occurs later in the database, after ax-inf has been introduced. (Contributed by Scott Fenton, 23-Dec-2021)

Ref Expression
Assertion df-frecs frecs ( 𝑅 , 𝐴 , 𝐹 ) = ∪ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cR ⊢ 𝑅
1 cA ⊢ 𝐴
2 cF ⊢ 𝐹
3 1 0 2 cfrecs ⊢ frecs ( 𝑅 , 𝐴 , 𝐹 )
4 vf ⊢ 𝑓
5 vx ⊢ 𝑥
6 4 cv ⊢ 𝑓
7 5 cv ⊢ 𝑥
8 6 7 wfn ⊢ 𝑓 Fn 𝑥
9 7 1 wss ⊢ 𝑥 ⊆ 𝐴
10 vy ⊢ 𝑦
11 10 cv ⊢ 𝑦
12 1 0 11 cpred ⊢ Pred ( 𝑅 , 𝐴 , 𝑦 )
13 12 7 wss ⊢ Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥
14 13 10 7 wral ⊢ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥
15 9 14 wa ⊢ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 )
16 11 6 cfv ⊢ ( 𝑓 ‘ 𝑦 )
17 6 12 cres ⊢ ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) )
18 11 17 2 co ⊢ ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) )
19 16 18 wceq ⊢ ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) )
20 19 10 7 wral ⊢ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) )
21 8 15 20 w3a ⊢ ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) )
22 21 5 wex ⊢ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) )
23 22 4 cab ⊢ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }
24 23 cuni ⊢ ∪ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }
25 3 24 wceq ⊢ frecs ( 𝑅 , 𝐴 , 𝐹 ) = ∪ { 𝑓 ∣ ∃ 𝑥 ( 𝑓 Fn 𝑥 ∧ ( 𝑥 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝑥 Pred ( 𝑅 , 𝐴 , 𝑦 ) ⊆ 𝑥 ) ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝑦 𝐹 ( 𝑓 ↾ Pred ( 𝑅 , 𝐴 , 𝑦 ) ) ) ) }