Metamath Proof Explorer


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 F = frecs R A G
Assertion frr1 R Fr A R Se A F Fn A

Proof

Step Hyp Ref Expression
1 frr.1 F = frecs R A G
2 eqid a | b a Fn b b A c b Pred R A c b c b a c = c G a Pred R A c = a | b a Fn b b A c b Pred R A c b c b a c = c G a Pred R A c
3 2 frrlem1 a | b a Fn b b A c b Pred R A c b c b a c = c G a Pred R A c = f | x f Fn x x A y x Pred R A y x y x f y = y G f Pred R A y
4 3 1 frrlem15 R Fr A R Se A g a | b a Fn b b A c b Pred R A c b c b a c = c G a Pred R A c h a | b a Fn b b A c b Pred R A c b c b a c = c G a Pred R A c x g u x h v u = v
5 3 1 4 frrlem9 R Fr A R Se A Fun F
6 eqid F Pred t++ R A A z z z G F Pred R A z = F Pred t++ R A A z z z G F Pred R A z
7 simpl R Fr A R Se A R Fr A
8 predres Pred R A z = Pred R A A z
9 relres Rel R A
10 ssttrcl Rel R A R A t++ R A
11 predrelss R A t++ R A Pred R A A z Pred t++ R A A z
12 9 10 11 mp2b Pred R A A z Pred t++ R A A z
13 8 12 eqsstri Pred R A z Pred t++ R A A z
14 13 a1i R Fr A R Se A z A Pred R A z Pred t++ R A A z
15 frrlem16 R Fr A R Se A z A a Pred t++ R A A z Pred R A a Pred t++ R A A z
16 ttrclse R Se A t++ R A Se A
17 setlikespec z A t++ R A Se A Pred t++ R A A z V
18 17 ancoms t++ R A Se A z A Pred t++ R A A z V
19 16 18 sylan R Se A z A Pred t++ R A A z V
20 19 adantll R Fr A R Se A z A Pred t++ R A A z V
21 predss Pred t++ R A A z A
22 21 a1i R Fr A R Se A z A Pred t++ R A A z A
23 difss A dom F A
24 frmin R Fr A R Se A A dom F A A dom F z A dom F Pred R A dom F z =
25 23 24 mpanr1 R Fr A R Se A A dom F z A dom F Pred R A dom F z =
26 3 1 4 6 7 14 15 20 22 25 frrlem14 R Fr A R Se A dom F = A
27 df-fn F Fn A Fun F dom F = A
28 5 26 27 sylanbrc R Fr A R Se A F Fn A