MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eupap1 Unicode version

Theorem eupap1 23276
Description: Append one path segment to an Eulerian path (enlarging the graph to add the new edge). (Contributed by Mario Carneiro, 7-Apr-2015.)
Hypotheses
Ref Expression
eupap1.e
eupap1.a
eupap1.b
eupap1.c
eupap1.d
eupap1.g
eupap1.n
eupap1.f
eupap1.h
eupap1.q
Assertion
Ref Expression
eupap1

Proof of Theorem eupap1
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eupap1.e . . . 4
2 eupap1.b . . . . . 6
3 prex 4506 . . . . . 6
4 f1osng 5649 . . . . . 6
52, 3, 4sylancl 647 . . . . 5
6 f1ofn 5612 . . . . 5
75, 6syl 16 . . . 4
8 eupap1.d . . . . 5
9 disjsn 3913 . . . . 5
108, 9sylibr 206 . . . 4
11 eupap1.g . . . . 5
12 eupagra 23266 . . . . 5
1311, 12syl 16 . . . 4
14 relumgra 22927 . . . . . . 7
1514brrelexi 4850 . . . . . 6
1613, 15syl 16 . . . . 5
17 eupapf 23272 . . . . . . 7
1811, 17syl 16 . . . . . 6
19 eupap1.n . . . . . . . . . 10
20 eupacl 23269 . . . . . . . . . . 11
2111, 20syl 16 . . . . . . . . . 10
2219, 21eqeltrd 2496 . . . . . . . . 9
23 nn0uz 10840 . . . . . . . . 9
2422, 23syl6eleq 2512 . . . . . . . 8
25 eluzfz2 11403 . . . . . . . 8
2624, 25syl 16 . . . . . . 7
2719oveq2d 6077 . . . . . . 7
2826, 27eleqtrd 2498 . . . . . 6
2918, 28ffvelrnd 5814 . . . . 5
30 eupap1.c . . . . 5
31 umgra1 22939 . . . . 5
3216, 2, 29, 30, 31syl22anc 1204 . . . 4
331, 7, 10, 13, 32umgraun 22941 . . 3
34 eupap1.f . . 3
3533, 34syl6breqr 4307 . 2
36 peano2nn0 10566 . . . 4
3722, 36syl 16 . . 3
38 eupaf1o 23270 . . . . . . . 8
3911, 1, 38syl2anc 646 . . . . . . 7
4019oveq2d 6077 . . . . . . . 8
41 f1oeq2 5603 . . . . . . . 8
4240, 41syl 16 . . . . . . 7
4339, 42mpbird 226 . . . . . 6
44 f1osng 5649 . . . . . . 7
4537, 2, 44syl2anc 646 . . . . . 6
46 fzp1disj 11457 . . . . . . 7
4746a1i 11 . . . . . 6
48 f1oun 5630 . . . . . 6
4943, 45, 47, 10, 48syl22anc 1204 . . . . 5
50 eupap1.h . . . . . 6
51 f1oeq1 5602 . . . . . 6
5250, 51ax-mp 5 . . . . 5
5349, 52sylibr 206 . . . 4
54 1z 10621 . . . . . 6
55 1m1e0 10336 . . . . . . . 8
5655fveq2i 5664 . . . . . . 7
5724, 56syl6eleqr 2513 . . . . . 6
58 fzsuc2 11456 . . . . . 6
5954, 57, 58sylancr 648 . . . . 5
60 f1oeq2 5603 . . . . 5
6159, 60syl 16 . . . 4
6253, 61mpbird 226 . . 3
6327feq2d 5517 . . . . . 6
6418, 63mpbird 226 . . . . 5
65 f1osng 5649 . . . . . . . 8
6637, 30, 65syl2anc 646 . . . . . . 7
67 f1of 5611 . . . . . . 7
6866, 67syl 16 . . . . . 6
6930snssd 3993 . . . . . 6
70 fss 5537 . . . . . 6
7168, 69, 70syl2anc 646 . . . . 5
72 fzp1disj 11457 . . . . . 6
7372a1i 11 . . . . 5
74 fun2 5546 . . . . 5
7564, 71, 73, 74syl21anc 1202 . . . 4
76 eupap1.q . . . . . 6
7776a1i 11 . . . . 5
78 fzsuc 11446 . . . . . 6
7924, 78syl 16 . . . . 5
8077, 79feq12d 5518 . . . 4
8175, 80mpbird 226 . . 3
8234fveq1i 5662 . . . . . . . 8
83 f1of 5611 . . . . . . . . . . . . 13
8443, 83syl 16 . . . . . . . . . . . 12
8584ffvelrnda 5813 . . . . . . . . . . 11
868adantr 455 . . . . . . . . . . 11
87 nelne2 2681 . . . . . . . . . . 11
8885, 86, 87syl2anc 646 . . . . . . . . . 10
8988necomd 2674 . . . . . . . . 9
90 fvunsn 5879 . . . . . . . . 9
9189, 90syl 16 . . . . . . . 8
9282, 91syl5eq 2466 . . . . . . 7
9350fveq1i 5662 . . . . . . . . 9
94 elfznn 11422 . . . . . . . . . . . . 13
9594adantl 456 . . . . . . . . . . . 12
9695nnred 10283 . . . . . . . . . . 11
9722nn0red 10582 . . . . . . . . . . . . 13
9897adantr 455 . . . . . . . . . . . 12
9937nn0red 10582 . . . . . . . . . . . . 13
10099adantr 455 . . . . . . . . . . . 12
101 elfzle2 11399 . . . . . . . . . . . . 13
102101adantl 456 . . . . . . . . . . . 12
10397ltp1d 10209 . . . . . . . . . . . . 13
104103adantr 455 . . . . . . . . . . . 12
10596, 98, 100, 102, 104lelttrd 9475 . . . . . . . . . . 11
10696, 105gtned 9455 . . . . . . . . . 10
107 fvunsn 5879 . . . . . . . . . 10
108106, 107syl 16 . . . . . . . . 9
10993, 108syl5eq 2466 . . . . . . . 8
110109fveq2d 5665 . . . . . . 7
11176fveq1i 5662 . . . . . . . . . 10
112 peano2rem 9621 . . . . . . . . . . . . 13
11396, 112syl 16 . . . . . . . . . . . 12
11496ltm1d 10211 . . . . . . . . . . . . 13
115113, 96, 100, 114, 105lttrd 9478 . . . . . . . . . . . 12
116113, 115gtned 9455 . . . . . . . . . . 11
117 fvunsn 5879 . . . . . . . . . . 11
118116, 117syl 16 . . . . . . . . . 10
119111, 118syl5eq 2466 . . . . . . . . 9
12076fveq1i 5662 . . . . . . . . . 10
121 fvunsn 5879 . . . . . . . . . . 11
122106, 121syl 16 . . . . . . . . . 10
123120, 122syl5eq 2466 . . . . . . . . 9
124119, 123preq12d 3937 . . . . . . . 8
12511adantr 455 . . . . . . . . 9
12640eleq2d 2489 . . . . . . . . . 10
127126biimpa 474 . . . . . . . . 9
128 eupaseg 23273 . . . . . . . . 9
129125, 127, 128syl2anc 646 . . . . . . . 8
130124, 129eqtr4d 2457 . . . . . . 7
13192, 110, 1303eqtr4d 2464 . . . . . 6
132131ralrimiva 2778 . . . . 5
13334fveq1i 5662 . . . . . . . . . 10
134 fnun 5487 . . . . . . . . . . . . 13
1351, 7, 10, 134syl21anc 1202 . . . . . . . . . . . 12
136 fnfun 5478 . . . . . . . . . . . 12
137135, 136syl 16 . . . . . . . . . . 11
138 ssun2 3497 . . . . . . . . . . . 12
139138a1i 11 . . . . . . . . . . 11
140 snidg 3880 . . . . . . . . . . . . 13
1412, 140syl 16 . . . . . . . . . . . 12
1423dmsnop 5285 . . . . . . . . . . . 12
143141, 142syl6eleqr 2513 . . . . . . . . . . 11
144 funssfv 5675 . . . . . . . . . . 11
145137, 139, 143, 144syl3anc 1203 . . . . . . . . . 10
146133, 145syl5eq 2466 . . . . . . . . 9
147 fvsng 5881 . . . . . . . . . 10
1482, 3, 147sylancl 647 . . . . . . . . 9
149146, 148eqtrd 2454 . . . . . . . 8
15050fveq1i 5662 . . . . . . . . . . 11
151 f1ofun 5613 . . . . . . . . . . . . 13
15249, 151syl 16 . . . . . . . . . . . 12
153 ssun2 3497 . . . . . . . . . . . . 13
154153a1i 11 . . . . . . . . . . . 12
155 snidg 3880 . . . . . . . . . . . . . 14
15637, 155syl 16 . . . . . . . . . . . . 13
157 dmsnopg 5282 . . . . . . . . . . . . . 14
1582, 157syl 16 . . . . . . . . . . . . 13
159156, 158eleqtrrd 2499 . . . . . . . . . . . 12
160 funssfv 5675 . . . . . . . . . . . 12
161152, 154, 159, 160syl3anc 1203 . . . . . . . . . . 11
162150, 161syl5eq 2466 . . . . . . . . . 10
163 fvsng 5881 . . . . . . . . . . 11
16437, 2, 163syl2anc 646 . . . . . . . . . 10
165162, 164eqtrd 2454 . . . . . . . . 9
166165fveq2d 5665 . . . . . . . 8
16797recnd 9358 . . . . . . . . . . . 12
168 ax-1cn 9286 . . . . . . . . . . . 12
169 pncan 9562 . . . . . . . . . . . 12
170167, 168, 169sylancl 647 . . . . . . . . . . 11
171170fveq2d 5665 . . . . . . . . . 10
17276fveq1i 5662 . . . . . . . . . . 11
17397, 103gtned 9455 . . . . . . . . . . . 12
174 fvunsn 5879 . . . . . . . . . . . 12
175173, 174syl 16 . . . . . . . . . . 11
176172, 175syl5eq 2466 . . . . . . . . . 10
177171, 176eqtrd 2454 . . . . . . . . 9
17876fveq1i 5662 . . . . . . . . . . 11
179 ffun 5531 . . . . . . . . . . . . 13
18075, 179syl 16 . . . . . . . . . . . 12
181 ssun2 3497 . . . . . . . . . . . . 13
182181a1i 11 . . . . . . . . . . . 12
183 dmsnopg 5282 . . . . . . . . . . . . . 14
18430, 183syl 16 . . . . . . . . . . . . 13
185156, 184eleqtrrd 2499 . . . . . . . . . . . 12
186 funssfv 5675 . . . . . . . . . . . 12
187180, 182, 185, 186syl3anc 1203 . . . . . . . . . . 11
188178, 187syl5eq 2466 . . . . . . . . . 10
189 fvsng 5881 . . . . . . . . . . 11
19037, 30, 189syl2anc 646 . . . . . . . . . 10
191188, 190eqtrd 2454 . . . . . . . . 9
192177, 191preq12d 3937 . . . . . . . 8
193149, 166, 1923eqtr4d 2464 . . . . . . 7
194 elsni 3879 . . . . . . . . . 10
195194fveq2d 5665 . . . . . . . . 9
196195fveq2d 5665 . . . . . . . 8
197194oveq1d 6076 . . . . . . . . . 10
198197fveq2d 5665 . . . . . . . . 9
199194fveq2d 5665 . . . . . . . . 9
200198, 199preq12d 3937 . . . . . . . 8
201196, 200eqeq12d 2436 . . . . . . 7
202193, 201syl5ibrcom 216 . . . . . 6
203202ralrimiv 2777 . . . . 5
204 ralun 3515 . . . . 5
205132, 203, 204syl2anc 646 . . . 4
20659raleqdv 2902 . . . 4
207205, 206mpbird 226 . . 3
208 oveq2 6069 . . . . . 6
209 f1oeq2 5603 . . . . . 6
210208, 209syl 16 . . . . 5
211 oveq2 6069 . . . . . 6
212211feq2d 5517 . . . . 5
213208raleqdv 2902 . . . . 5
214210, 212, 2133anbi123d 1274 . . . 4
215214rspcev 3051 . . 3
21637, 62, 81, 207, 215syl13anc 1205 . 2
21734fneq1i 5475 . . . . 5
218135, 217sylibr 206 . . . 4
219 fndm 5480 . . . 4
220218, 219syl 16 . . 3
221 iseupa 23265 . . 3
222220, 221syl 16 . 2
22335, 216, 222mpbir2and 898 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  <->wb 178  /\wa 362  /\w3a 950  =wceq 1687  e.wcel 1749  =/=wne 2585  A.wral 2694  E.wrex 2695   cvv 2951  u.cun 3303  i^icin 3304  C_wss 3305   c0 3614  {csn 3853  {cpr 3854  <.cop 3856   class class class wbr 4267  domcdm 4811  Funwfun 5384  Fnwfn 5385  -->wf 5386  -1-1-onto->wf1o 5389  `cfv 5390  (class class class)co 6061   cfn 7269   cc 9226   cr 9227  0cc0 9228  1c1 9229   caddc 9231   clt 9364   cle 9365   cmin 9541   cn 10268   cn0 10525   cz 10591   cuz 10806   cfz 11381   chash 12044   cumg 22925   ceup 23262
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721  ax-8 1751  ax-9 1753  ax-10 1768  ax-11 1773  ax-12 1785  ax-13 1934  ax-ext 2403  ax-rep 4378  ax-sep 4388  ax-nul 4396  ax-pow 4442  ax-pr 4503  ax-un 6342  ax-cnex 9284  ax-resscn 9285  ax-1cn 9286  ax-icn 9287  ax-addcl 9288  ax-addrcl 9289  ax-mulcl 9290  ax-mulrcl 9291  ax-mulcom 9292  ax-addass 9293  ax-mulass 9294  ax-distr 9295  ax-i2m1 9296  ax-1ne0 9297  ax-1rid 9298  ax-rnegex 9299  ax-rrecex 9300  ax-cnre 9301  ax-pre-lttri 9302  ax-pre-lttrn 9303  ax-pre-ltadd 9304  ax-pre-mulgt0 9305
This theorem depends on definitions:  df-bi 179  df-or 363  df-an 364  df-3or 951  df-3an 952  df-tru 1355  df-ex 1582  df-nf 1585  df-sb 1694  df-eu 2248  df-mo 2249  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2547  df-ne 2587  df-nel 2588  df-ral 2699  df-rex 2700  df-reu 2701  df-rmo 2702  df-rab 2703  df-v 2953  df-sbc 3165  df-csb 3266  df-dif 3308  df-un 3310  df-in 3312  df-ss 3319  df-pss 3321  df-nul 3615  df-if 3769  df-pw 3839  df-sn 3859  df-pr 3860  df-tp 3861  df-op 3862  df-uni 4067  df-int 4104  df-iun 4148  df-br 4268  df-opab 4326  df-mpt 4327  df-tr 4361  df-eprel 4603  df-id 4607  df-po 4612  df-so 4613  df-fr 4650  df-we 4652  df-ord 4693  df-on 4694  df-lim 4695  df-suc 4696  df-xp 4817  df-rel 4818  df-cnv 4819  df-co 4820  df-dm 4821  df-rn 4822  df-res 4823  df-ima 4824  df-iota 5353  df-fun 5392  df-fn 5393  df-f 5394  df-f1 5395  df-fo 5396  df-f1o 5397  df-fv 5398  df-riota 6020  df-ov 6064  df-oprab 6065  df-mpt2 6066  df-om 6447  df-1st 6546  df-2nd 6547  df-recs 6791  df-rdg 6825  df-1o 6881  df-oadd 6885  df-er 7062  df-pm 7178  df-en 7270  df-dom 7271  df-sdom 7272  df-fin 7273  df-card 8056  df-cda 8284  df-pnf 9366  df-mnf 9367  df-xr 9368  df-ltxr 9369  df-le 9370  df-sub 9543  df-neg 9544  df-nn 10269  df-2 10326  df-n0 10526  df-z 10592  df-uz 10807  df-fz 11382  df-hash 12045  df-umgra 22926  df-eupa 23263
  Copyright terms: Public domain W3C validator