Description: The domain of the well-ordered recursion generator is a subclass of A . Avoids the axiom of replacement. (Contributed by Scott Fenton, 21-Apr-2011) (Proof shortened by Scott Fenton, 17-Nov-2024)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | wfrrel.1 | ⊢ 𝐹 = wrecs ( 𝑅 , 𝐴 , 𝐺 ) | |
| Assertion | wfrdmss | ⊢ dom 𝐹 ⊆ 𝐴 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | wfrrel.1 | ⊢ 𝐹 = wrecs ( 𝑅 , 𝐴 , 𝐺 ) | |
| 2 | df-wrecs | ⊢ wrecs ( 𝑅 , 𝐴 , 𝐺 ) = frecs ( 𝑅 , 𝐴 , ( 𝐺 ∘ 2nd ) ) | |
| 3 | 1 2 | eqtri | ⊢ 𝐹 = frecs ( 𝑅 , 𝐴 , ( 𝐺 ∘ 2nd ) ) |
| 4 | 3 | frrdmss | ⊢ dom 𝐹 ⊆ 𝐴 |