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

Theorem tfrlem5 5961
 Description: Lemma for transfinite recursion. The values of two acceptable functions are the same within their domains. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 24-May-2019.)
Hypothesis
Ref Expression
tfrlem.1
Assertion
Ref Expression
tfrlem5
Distinct variable groups:   ,,,,,,,   ,,
Allowed substitution hints:   (,,,,)

Proof of Theorem tfrlem5
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 tfrlem.1 . . 3
2 vex 2577 . . 3
31, 2tfrlem3a 5956 . 2
4 vex 2577 . . 3
51, 4tfrlem3a 5956 . 2
6 reeanv 2496 . . 3
7 simp2ll 982 . . . . . . . . . 10
8 simp3l 943 . . . . . . . . . 10
9 fnbr 5029 . . . . . . . . . 10
107, 8, 9syl2anc 397 . . . . . . . . 9
11 simp2rl 984 . . . . . . . . . 10
12 simp3r 944 . . . . . . . . . 10
13 fnbr 5029 . . . . . . . . . 10
1411, 12, 13syl2anc 397 . . . . . . . . 9
15 elin 3154 . . . . . . . . 9
1610, 14, 15sylanbrc 402 . . . . . . . 8
17 onin 4151 . . . . . . . . . 10
18173ad2ant1 936 . . . . . . . . 9
19 fnfun 5024 . . . . . . . . . . 11
207, 19syl 14 . . . . . . . . . 10
21 inss1 3185 . . . . . . . . . . 11
22 fndm 5026 . . . . . . . . . . . 12
237, 22syl 14 . . . . . . . . . . 11
2421, 23syl5sseqr 3022 . . . . . . . . . 10
2520, 24jca 294 . . . . . . . . 9
26 fnfun 5024 . . . . . . . . . . 11
2711, 26syl 14 . . . . . . . . . 10
28 inss2 3186 . . . . . . . . . . 11
29 fndm 5026 . . . . . . . . . . . 12
3011, 29syl 14 . . . . . . . . . . 11
3128, 30syl5sseqr 3022 . . . . . . . . . 10
3227, 31jca 294 . . . . . . . . 9
33 simp2lr 983 . . . . . . . . . 10
34 ssralv 3032 . . . . . . . . . 10
3521, 33, 34mpsyl 63 . . . . . . . . 9
36 simp2rr 985 . . . . . . . . . 10
37 ssralv 3032 . . . . . . . . . 10
3828, 36, 37mpsyl 63 . . . . . . . . 9
3918, 25, 32, 35, 38tfrlem1 5954 . . . . . . . 8
40 fveq2 5206 . . . . . . . . . 10
41 fveq2 5206 . . . . . . . . . 10
4240, 41eqeq12d 2070 . . . . . . . . 9
4342rspcv 2669 . . . . . . . 8
4416, 39, 43sylc 60 . . . . . . 7
45 funbrfv 5240 . . . . . . . 8
4620, 8, 45sylc 60 . . . . . . 7
47 funbrfv 5240 . . . . . . . 8
4827, 12, 47sylc 60 . . . . . . 7
4944, 46, 483eqtr3d 2096 . . . . . 6
50493exp 1114 . . . . 5
5150rexlimdva 2450 . . . 4
5251rexlimiv 2444 . . 3
536, 52sylbir 129 . 2
543, 5, 53syl2anb 279 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 101   w3a 896   wceq 1259   wcel 1409  cab 2042  wral 2323  wrex 2324   cin 2944   wss 2945   class class class wbr 3792  con0 4128   cdm 4373   cres 4375   wfun 4924   wfn 4925  cfv 4930 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-14 1421  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038  ax-sep 3903  ax-pow 3955  ax-pr 3972  ax-setind 4290 This theorem depends on definitions:  df-bi 114  df-3an 898  df-tru 1262  df-nf 1366  df-sb 1662  df-eu 1919  df-mo 1920  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-ral 2328  df-rex 2329  df-rab 2332  df-v 2576  df-sbc 2788  df-csb 2881  df-un 2950  df-in 2952  df-ss 2959  df-pw 3389  df-sn 3409  df-pr 3410  df-op 3412  df-uni 3609  df-br 3793  df-opab 3847  df-mpt 3848  df-tr 3883  df-id 4058  df-iord 4131  df-on 4133  df-xp 4379  df-rel 4380  df-cnv 4381  df-co 4382  df-dm 4383  df-res 4385  df-iota 4895  df-fun 4932  df-fn 4933  df-fv 4938 This theorem is referenced by:  tfrlem7  5964  tfrexlem  5979
 Copyright terms: Public domain W3C validator