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

Theorem tfrlem1 5864
Description: A technical lemma for transfinite recursion. Compare Lemma 1 of [TakeutiZaring] p. 47. (Contributed by NM, 23-Mar-1995.) (Revised by Mario Carneiro, 24-May-2019.)
Hypotheses
Ref Expression
tfrlem1.1  On
tfrlem1.2  Fun  F  C_  dom  F
tfrlem1.3  Fun  G  C_  dom  G
tfrlem1.4  F `  `  F  |`
tfrlem1.5  G `  `  G  |`
Assertion
Ref Expression
tfrlem1  F `  G `
Distinct variable groups:   ,   ,   , F   , G
Allowed substitution hint:   ()

Proof of Theorem tfrlem1
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssid 2958 . 2  C_
2 tfrlem1.1 . . 3  On
3 sseq1 2960 . . . . . 6  C_  C_
4 raleq 2499 . . . . . 6  F `  G `  F `  G `
53, 4imbi12d 223 . . . . 5  C_  F `  G ` 
C_  F `  G `
65imbi2d 219 . . . 4 
C_  F `  G `  C_  F `  G `
7 sseq1 2960 . . . . . . 7  C_  C_
8 raleq 2499 . . . . . . 7  F `  G `  F `  G `
97, 8imbi12d 223 . . . . . 6  C_  F `  G ` 
C_  F `  G `
109imbi2d 219 . . . . 5 
C_  F `  G `  C_  F `  G `
11 r19.21v 2390 . . . . . 6  C_  F `  G `  C_  F `  G `
12 simplll 485 . . . . . . . . . . . . . . . . . . 19  On  C_  F `  G `  C_
1312adantr 261 . . . . . . . . . . . . . . . . . 18  On  C_  F `  G `  C_
14 tfrlem1.2 . . . . . . . . . . . . . . . . . 18  Fun  F  C_  dom  F
1513, 14syl 14 . . . . . . . . . . . . . . . . 17  On  C_  F `  G `  C_  Fun  F  C_  dom  F
1615simpld 105 . . . . . . . . . . . . . . . 16  On  C_  F `  G `  C_  Fun  F
17 funfn 4874 . . . . . . . . . . . . . . . 16  Fun 
F  F  Fn  dom  F
1816, 17sylib 127 . . . . . . . . . . . . . . 15  On  C_  F `  G `  C_  F  Fn  dom  F
19 simpllr 486 . . . . . . . . . . . . . . . . . . 19  On  C_  F `  G `  C_  On
20 eloni 4078 . . . . . . . . . . . . . . . . . . 19  On  Ord
2119, 20syl 14 . . . . . . . . . . . . . . . . . 18  On  C_  F `  G `  C_  Ord
22 ordelss 4082 . . . . . . . . . . . . . . . . . 18  Ord  C_
2321, 22sylan 267 . . . . . . . . . . . . . . . . 17  On  C_  F `  G `  C_  C_
24 simplr 482 . . . . . . . . . . . . . . . . 17  On  C_  F `  G `  C_  C_
2523, 24sstrd 2949 . . . . . . . . . . . . . . . 16  On  C_  F `  G `  C_  C_
2615simprd 107 . . . . . . . . . . . . . . . 16  On  C_  F `  G `  C_  C_  dom  F
2725, 26sstrd 2949 . . . . . . . . . . . . . . 15  On  C_  F `  G `  C_  C_  dom  F
28 fnssres 4955 . . . . . . . . . . . . . . 15  F  Fn  dom  F  C_  dom  F  F  |`  Fn
2918, 27, 28syl2anc 391 . . . . . . . . . . . . . 14  On  C_  F `  G `  C_  F  |`  Fn
30 tfrlem1.3 . . . . . . . . . . . . . . . . . 18  Fun  G  C_  dom  G
3113, 30syl 14 . . . . . . . . . . . . . . . . 17  On  C_  F `  G `  C_  Fun  G  C_  dom  G
3231simpld 105 . . . . . . . . . . . . . . . 16  On  C_  F `  G `  C_  Fun  G
33 funfn 4874 . . . . . . . . . . . . . . . 16  Fun 
G  G  Fn  dom  G
3432, 33sylib 127 . . . . . . . . . . . . . . 15  On  C_  F `  G `  C_  G  Fn  dom  G
3531simprd 107 . . . . . . . . . . . . . . . 16  On  C_  F `  G `  C_  C_  dom  G
3625, 35sstrd 2949 . . . . . . . . . . . . . . 15  On  C_  F `  G `  C_  C_  dom  G
37 fnssres 4955 . . . . . . . . . . . . . . 15  G  Fn  dom  G  C_  dom  G  G  |`  Fn
3834, 36, 37syl2anc 391 . . . . . . . . . . . . . 14  On  C_  F `  G `  C_  G  |`  Fn
39 simpr 103 . . . . . . . . . . . . . . . 16  On  C_  F `  G `  C_
40 simplr 482 . . . . . . . . . . . . . . . . 17  On  C_  F `  G `  C_
41 simplr 482 . . . . . . . . . . . . . . . . . 18  On  C_  F `  G `  C_  C_  F `  G `
4241ad2antrr 457 . . . . . . . . . . . . . . . . 17  On  C_  F `  G `  C_  C_  F `  G `
4325adantr 261 . . . . . . . . . . . . . . . . 17  On  C_  F `  G `  C_  C_
44 sseq1 2960 . . . . . . . . . . . . . . . . . . 19  C_  C_
45 raleq 2499 . . . . . . . . . . . . . . . . . . 19  F `  G `  F `  G `
4644, 45imbi12d 223 . . . . . . . . . . . . . . . . . 18  C_  F `  G ` 
C_  F `  G `
4746rspcv 2646 . . . . . . . . . . . . . . . . 17  C_  F `  G `  C_  F `  G `
4840, 42, 43, 47syl3c 57 . . . . . . . . . . . . . . . 16  On  C_  F `  G `  C_  F `  G `
49 fveq2 5121 . . . . . . . . . . . . . . . . . 18  F `  F `
50 fveq2 5121 . . . . . . . . . . . . . . . . . 18  G `  G `
5149, 50eqeq12d 2051 . . . . . . . . . . . . . . . . 17  F `  G `  F `  G `
5251rspcv 2646 . . . . . . . . . . . . . . . 16  F `  G `  F `  G `
5339, 48, 52sylc 56 . . . . . . . . . . . . . . 15  On  C_  F `  G `  C_  F `  G `
54 fvres 5141 . . . . . . . . . . . . . . . 16  F  |`  `
 F `
5554adantl 262 . . . . . . . . . . . . . . 15  On  C_  F `  G `  C_  F  |`  `
 F `
56 fvres 5141 . . . . . . . . . . . . . . . 16  G  |`  `
 G `
5756adantl 262 . . . . . . . . . . . . . . 15  On  C_  F `  G `  C_  G  |`  `
 G `
5853, 55, 573eqtr4d 2079 . . . . . . . . . . . . . 14  On  C_  F `  G `  C_  F  |`  `
 G  |`  `
5929, 38, 58eqfnfvd 5211 . . . . . . . . . . . . 13  On  C_  F `  G `  C_  F  |`  G  |`
6059fveq2d 5125 . . . . . . . . . . . 12  On  C_  F `  G `  C_  `  F  |`  `
 G  |`
61 simpr 103 . . . . . . . . . . . . . 14  On  C_  F `  G `  C_  C_
6261sselda 2939 . . . . . . . . . . . . 13  On  C_  F `  G `  C_
63 tfrlem1.4 . . . . . . . . . . . . . 14  F `  `  F  |`
6413, 63syl 14 . . . . . . . . . . . . 13  On  C_  F `  G `  C_  F `  `  F  |`
65 fveq2 5121 . . . . . . . . . . . . . . 15  F `  F `
66 reseq2 4550 . . . . . . . . . . . . . . . 16  F  |`  F  |`
6766fveq2d 5125 . . . . . . . . . . . . . . 15  `  F  |`  `  F  |`
6865, 67eqeq12d 2051 . . . . . . . . . . . . . 14  F `  `  F  |`  F `  `  F  |`
6968rspcva 2648 . . . . . . . . . . . . 13  F `  `  F  |`  F `  `  F  |`
7062, 64, 69syl2anc 391 . . . . . . . . . . . 12  On  C_  F `  G `  C_  F `  `  F  |`
71 tfrlem1.5 . . . . . . . . . . . . . 14  G `  `  G  |`
7213, 71syl 14 . . . . . . . . . . . . 13  On  C_  F `  G `  C_  G `  `  G  |`
73 fveq2 5121 . . . . . . . . . . . . . . 15  G `  G `
74 reseq2 4550 . . . . . . . . . . . . . . . 16  G  |`  G  |`
7574fveq2d 5125 . . . . . . . . . . . . . . 15  `  G  |`  `  G  |`
7673, 75eqeq12d 2051 . . . . . . . . . . . . . 14  G `  `  G  |`  G `  `  G  |`
7776rspcva 2648 . . . . . . . . . . . . 13  G `  `  G  |`  G `  `  G  |`
7862, 72, 77syl2anc 391 . . . . . . . . . . . 12  On  C_  F `  G `  C_  G `  `  G  |`
7960, 70, 783eqtr4d 2079 . . . . . . . . . . 11  On  C_  F `  G `  C_  F `  G `
8079ralrimiva 2386 . . . . . . . . . 10  On  C_  F `  G `  C_  F `  G `
8165, 73eqeq12d 2051 . . . . . . . . . . 11  F `  G `  F `  G `
8281cbvralv 2527 . . . . . . . . . 10  F `  G `  F `  G `
8380, 82sylibr 137 . . . . . . . . 9  On  C_  F `  G `  C_  F `  G `
8483exp31 346 . . . . . . . 8  On  C_  F `  G ` 
C_  F `  G `
8584expcom 109 . . . . . . 7  On  C_  F `  G ` 
C_  F `  G `
8685a2d 23 . . . . . 6  On  C_  F `  G `  C_  F `  G `
8711, 86syl5bi 141 . . . . 5  On 
C_  F `  G `  C_  F `  G `
8810, 87tfis2 4251 . . . 4  On  C_  F `  G `
896, 88vtoclga 2613 . . 3  On  C_  F `  G `
902, 89mpcom 32 . 2  C_  F `  G `
911, 90mpi 15 1  F `  G `
Colors of variables: wff set class
Syntax hints:   wi 4   wa 97   wceq 1242   wcel 1390  wral 2300    C_ wss 2911   Ord word 4065   Oncon0 4066   dom cdm 4288    |` cres 4290   Fun wfun 4839    Fn wfn 4840   ` cfv 4845
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935  ax-setind 4220
This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-rab 2309  df-v 2553  df-sbc 2759  df-csb 2847  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-br 3756  df-opab 3810  df-mpt 3811  df-tr 3846  df-id 4021  df-iord 4069  df-on 4071  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-res 4300  df-iota 4810  df-fun 4847  df-fn 4848  df-fv 4853
This theorem is referenced by:  tfrlem5  5871
  Copyright terms: Public domain W3C validator