Mathbox for Drahflow < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  relexpindlem Unicode version

Theorem relexpindlem 24036
 Description: Principle of transitive induction, finite and non-class version. The first three hypotheses give various existences, the next three give necessary substitutions and the last two are the basis and the induction hypothesis. (Contributed by Drahflow, 12-Nov-2015.)
Hypotheses
Ref Expression
relexpindlem.1
relexpindlem.2
relexpindlem.3
relexpindlem.4
relexpindlem.5
relexpindlem.6
relexpindlem.7
relexpindlem.8
Assertion
Ref Expression
relexpindlem
Distinct variable groups:   ,   ,   ,   ,,   ,,,   ,,   ,,   ,,   ,   ,   ,,
Allowed substitution hints:   (,)   (,)   (,,)   (,,)   ()   ()   ()

Proof of Theorem relexpindlem
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpr 447 . . . 4
2 eleq1 2343 . . . . . . 7
32anbi2d 684 . . . . . 6
4 oveq2 5866 . . . . . . . . 9
54breqd 4034 . . . . . . . 8
65imbi1d 308 . . . . . . 7
76albidv 1611 . . . . . 6
83, 7imbi12d 311 . . . . 5
9 eleq1 2343 . . . . . . 7
109anbi2d 684 . . . . . 6
11 oveq2 5866 . . . . . . . . 9
1211breqd 4034 . . . . . . . 8
1312imbi1d 308 . . . . . . 7
1413albidv 1611 . . . . . 6
1510, 14imbi12d 311 . . . . 5
16 eleq1 2343 . . . . . . 7
1716anbi2d 684 . . . . . 6
18 oveq2 5866 . . . . . . . . 9
1918breqd 4034 . . . . . . . 8
2019imbi1d 308 . . . . . . 7
2120albidv 1611 . . . . . 6
2217, 21imbi12d 311 . . . . 5
23 eleq1 2343 . . . . . . 7
2423anbi2d 684 . . . . . 6
25 oveq2 5866 . . . . . . . . 9
2625breqd 4034 . . . . . . . 8
2726imbi1d 308 . . . . . . 7
2827albidv 1611 . . . . . 6
2924, 28imbi12d 311 . . . . 5
30 relexpindlem.1 . . . . . . . . 9
31 relexpindlem.2 . . . . . . . . 9
3230, 31relexp0 24025 . . . . . . . 8
3332adantr 451 . . . . . . 7
34 relexpindlem.7 . . . . . . . . . . 11
3534adantr 451 . . . . . . . . . 10
36 simpl 443 . . . . . . . . . 10
37 relexpindlem.3 . . . . . . . . . . . 12
3837adantl 452 . . . . . . . . . . 11
3934ad2antrl 708 . . . . . . . . . . . . . . . . . . 19
40 simprl 732 . . . . . . . . . . . . . . . . . . 19
4139, 40jca 518 . . . . . . . . . . . . . . . . . 18
4241expcom 424 . . . . . . . . . . . . . . . . 17
4342expcom 424 . . . . . . . . . . . . . . . 16
4443expcom 424 . . . . . . . . . . . . . . 15
45443imp1 1164 . . . . . . . . . . . . . 14
4645expcom 424 . . . . . . . . . . . . 13
47 simpr 447 . . . . . . . . . . . . . . . . 17
4847adantl 452 . . . . . . . . . . . . . . . 16
49 relexpindlem.4 . . . . . . . . . . . . . . . . . . 19
5049ad2antll 709 . . . . . . . . . . . . . . . . . 18
5150bicomd 192 . . . . . . . . . . . . . . . . 17
52 anbi1 687 . . . . . . . . . . . . . . . . . 18
53 simpl 443 . . . . . . . . . . . . . . . . . 18
5452, 53syl6bi 219 . . . . . . . . . . . . . . . . 17
5551, 54mpcom 32 . . . . . . . . . . . . . . . 16
56 simprl 732 . . . . . . . . . . . . . . . 16
5748, 55, 563jca 1132 . . . . . . . . . . . . . . 15
5857anassrs 629 . . . . . . . . . . . . . 14
5958expcom 424 . . . . . . . . . . . . 13
6046, 59impbid 183 . . . . . . . . . . . 12
6160spcegv 2869 . . . . . . . . . . 11
6238, 61mpcom 32 . . . . . . . . . 10
6335, 36, 62syl2anc 642 . . . . . . . . 9
64 simpl 443 . . . . . . . . . . . . . 14
65 df-br 4024 . . . . . . . . . . . . . 14
6664, 65sylib 188 . . . . . . . . . . . . 13
67 vex 2791 . . . . . . . . . . . . . 14
6867opelres 4960 . . . . . . . . . . . . 13
6966, 68sylib 188 . . . . . . . . . . . 12
70 simpll 730 . . . . . . . . . . . . . 14
71 df-br 4024 . . . . . . . . . . . . . 14
7270, 71sylibr 203 . . . . . . . . . . . . 13
7367ideq 4836 . . . . . . . . . . . . 13
7472, 73sylib 188 . . . . . . . . . . . 12
7569, 74mpancom 650 . . . . . . . . . . 11
76 breq1 4026 . . . . . . . . . . . . 13
77 eqeq2 2292 . . . . . . . . . . . . . . . 16
78773anbi1d 1256 . . . . . . . . . . . . . . 15
7978exbidv 1612 . . . . . . . . . . . . . 14
8079anbi1d 685 . . . . . . . . . . . . 13
8176, 80anbi12d 691 . . . . . . . . . . . 12
82 simprl 732 . . . . . . . . . . . . . . . . . 18
83 relexpindlem.5 . . . . . . . . . . . . . . . . . . 19
8483ad2antll 709 . . . . . . . . . . . . . . . . . 18
8582, 84mpbid 201 . . . . . . . . . . . . . . . . 17
8685expcom 424 . . . . . . . . . . . . . . . 16
8786expcom 424 . . . . . . . . . . . . . . 15
88873imp 1145 . . . . . . . . . . . . . 14
8988exlimiv 1666 . . . . . . . . . . . . 13
9089ad2antrl 708 . . . . . . . . . . . 12
9181, 90syl6bi 219 . . . . . . . . . . 11
9275, 91mpcom 32 . . . . . . . . . 10
9392expcom 424 . . . . . . . . 9
9463, 93mpancom 650 . . . . . . . 8
95 breq 4025 . . . . . . . . 9
9695imbi1d 308 . . . . . . . 8
9794, 96syl5ibr 212 . . . . . . 7
9833, 97mpcom 32 . . . . . 6
9998alrimiv 1617 . . . . 5
100 breq2 4027 . . . . . . . . . . . 12
101100, 83imbi12d 311 . . . . . . . . . . 11
102101cbvalv 1942 . . . . . . . . . 10
103102bicomi 193 . . . . . . . . 9
104 imbi2 314 . . . . . . . . . . . . 13
105104anbi1d 685 . . . . . . . . . . . 12
106105anbi2d 684 . . . . . . . . . . 11
107106anbi2d 684 . . . . . . . . . 10
108 simpl 443 . . . . . . . . . . . . 13
109 simprrr 741 . . . . . . . . . . . . 13
11030, 31relexpsucl 24028 . . . . . . . . . . . . 13
111108, 109, 110sylc 56 . . . . . . . . . . . 12
112 simpl 443 . . . . . . . . . . . . . . . 16
11337ad2antrl 708 . . . . . . . . . . . . . . . . 17
114 brcog 4850 . . . . . . . . . . . . . . . . 17
115113, 67, 114sylancl 643 . . . . . . . . . . . . . . . 16
116112, 115mpbid 201 . . . . . . . . . . . . . . 15
117 simprl 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
118 simprrl 740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
119118ad2antll 709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
120117, 119jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
121 simprl 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
122121ad2antll 709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
123120, 122mpd 14 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
124 simprrl 740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
125 simprrr 741 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
126125ad2antll 709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
127126ad2antll 709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
128 breq2 4027 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
129 relexpindlem.6 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
130128, 129imbi12d 311 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
131130cbvalv 1942 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
132 id 19 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
133 imbi2 314 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36
134133anbi1d 685 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35
135134anbi2d 684 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
136135anbi2d 684 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
137136anbi2d 684 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
138132, 137anbi12d 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
139 simprrl 740 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
140139ad2antll 709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
141140ad2antll 709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
142 sp 1716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
143142adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
144141, 143mpd 14 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
145138, 144syl6bi 219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
146131, 145ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
147 relexpindlem.8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
148124, 127, 146, 147syl3c 57 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
149123, 148mpancom 650 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
150149expcom 424 . . . . . . . . . . . . . . . . . . . . . . . . . 26
151150expcom 424 . . . . . . . . . . . . . . . . . . . . . . . . 25
152151expcom 424 . . . . . . . . . . . . . . . . . . . . . . . 24
153152anassrs 629 . . . . . . . . . . . . . . . . . . . . . . 23
154153impcom 419 . . . . . . . . . . . . . . . . . . . . . 22
155154anassrs 629 . . . . . . . . . . . . . . . . . . . . 21
156155impcom 419 . . . . . . . . . . . . . . . . . . . 20
157156anassrs 629 . . . . . . . . . . . . . . . . . . 19
158157impcom 419 . . . . . . . . . . . . . . . . . 18
159158anassrs 629 . . . . . . . . . . . . . . . . 17
160159expcom 424 . . . . . . . . . . . . . . . 16
161160exlimiv 1666 . . . . . . . . . . . . . . 15
162116, 161mpcom 32 . . . . . . . . . . . . . 14
163162expcom 424 . . . . . . . . . . . . 13
164 breq 4025 . . . . . . . . . . . . . 14
165164imbi1d 308 . . . . . . . . . . . . 13
166163, 165syl5ibr 212 . . . . . . . . . . . 12
167111, 166mpcom 32 . . . . . . . . . . 11
168167alrimiv 1617 . . . . . . . . . 10
169107, 168syl6bi 219 . . . . . . . . 9
170103, 169ax-mp 8 . . . . . . . 8
171170anassrs 629 . . . . . . 7
172171expcom 424 . . . . . 6
173172expcom 424 . . . . 5
1748, 15, 22, 29, 99, 173nn0ind 10108 . . . 4
1751, 174mpcom 32 . . 3
17617519.21bi 1794 . 2
177176ex 423 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 176   wa 358   w3a 934  wal 1527  wex 1528   wceq 1623   wcel 1684  cvv 2788  cop 3643  cuni 3827   class class class wbr 4023   cid 4304   cres 4691   ccom 4693   wrel 4694  (class class class)co 5858  cc0 8737  c1 8738   caddc 8740  cn0 9965  crelexp 24023 This theorem is referenced by:  relexpind  24037 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512  ax-cnex 8793  ax-resscn 8794  ax-1cn 8795  ax-icn 8796  ax-addcl 8797  ax-addrcl 8798  ax-mulcl 8799  ax-mulrcl 8800  ax-mulcom 8801  ax-addass 8802  ax-mulass 8803  ax-distr 8804  ax-i2m1 8805  ax-1ne0 8806  ax-1rid 8807  ax-rnegex 8808  ax-rrecex 8809  ax-cnre 8810  ax-pre-lttri 8811  ax-pre-lttrn 8812  ax-pre-ltadd 8813  ax-pre-mulgt0 8814 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-nel 2449  df-ral 2548  df-rex 2549  df-reu 2550  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pss 3168  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-tp 3648  df-op 3649  df-uni 3828  df-iun 3907  df-br 4024  df-opab 4078  df-mpt 4079  df-tr 4114  df-eprel 4305  df-id 4309  df-po 4314  df-so 4315  df-fr 4352  df-we 4354  df-ord 4395  df-on 4396  df-lim 4397  df-suc 4398  df-om 4657  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-ov 5861  df-oprab 5862  df-mpt2 5863  df-2nd 6123  df-riota 6304  df-recs 6388  df-rdg 6423  df-er 6660  df-en 6864  df-dom 6865  df-sdom 6866  df-pnf 8869  df-mnf 8870  df-xr 8871  df-ltxr 8872  df-le 8873  df-sub 9039  df-neg 9040  df-nn 9747  df-n0 9966  df-z 10025  df-uz 10231  df-seq 11047  df-relexp 24024
 Copyright terms: Public domain W3C validator