Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  frecuzrdgcl Unicode version

Theorem frecuzrdgcl 9199
 Description: Closure law for the recursive definition generator on upper integers. See comment in frec2uz0d 9185 for the description of as the mapping from to . (Contributed by Jim Kingdon, 31-May-2020.)
Hypotheses
Ref Expression
frec2uz.1
frec2uz.2 frec
uzrdg.s
uzrdg.a
uzrdg.f
uzrdg.2 frec
frecuzrdgfn.3
Assertion
Ref Expression
frecuzrdgcl
Distinct variable groups:   ,   ,,   ,   ,,   ,,   ,,   ,,
Allowed substitution hints:   ()   (,)   (,)   ()   (,)

Proof of Theorem frecuzrdgcl
StepHypRef Expression
1 frec2uz.1 . . . . . 6
21adantr 261 . . . . 5
3 frec2uz.2 . . . . 5 frec
4 uzrdg.s . . . . . 6
54adantr 261 . . . . 5
6 uzrdg.a . . . . . 6
76adantr 261 . . . . 5
8 uzrdg.f . . . . . 6
98adantlr 446 . . . . 5
10 uzrdg.2 . . . . 5 frec
11 simpr 103 . . . . 5
122, 3, 5, 7, 9, 10, 11frecuzrdglem 9197 . . . 4
13 frecuzrdgfn.3 . . . . 5
1413adantr 261 . . . 4
1512, 14eleqtrrd 2117 . . 3
161, 3, 4, 6, 8, 10, 13frecuzrdgfn 9198 . . . . 5
17 fnfun 4996 . . . . 5
18 funopfv 5213 . . . . 5
1916, 17, 183syl 17 . . . 4