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

Theorem eupap1 24066
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 4651 . . . . . 6
4 f1osng 5801 . . . . . 6
52, 3, 4sylancl 662 . . . . 5
6 f1ofn 5764 . . . . 5
75, 6syl 16 . . . 4
8 eupap1.d . . . . 5
9 disjsn 4053 . . . . 5
108, 9sylibr 212 . . . 4
11 eupap1.g . . . . 5
12 eupagra 24056 . . . . 5
1311, 12syl 16 . . . 4
14 relumgra 23717 . . . . . . 7
1514brrelexi 4996 . . . . . 6
1613, 15syl 16 . . . . 5
17 eupapf 24062 . . . . . . 7
1811, 17syl 16 . . . . . 6
19 eupap1.n . . . . . . . . . 10
20 eupacl 24059 . . . . . . . . . . 11
2111, 20syl 16 . . . . . . . . . 10
2219, 21eqeltrd 2542 . . . . . . . . 9
23 nn0uz 11034 . . . . . . . . 9
2422, 23syl6eleq 2552 . . . . . . . 8
25 eluzfz2 11604 . . . . . . . 8
2624, 25syl 16 . . . . . . 7
2719oveq2d 6238 . . . . . . 7
2826, 27eleqtrd 2544 . . . . . 6
2918, 28ffvelrnd 5967 . . . . 5
30 eupap1.c . . . . 5
31 umgra1 23729 . . . . 5
3216, 2, 29, 30, 31syl22anc 1220 . . . 4
331, 7, 10, 13, 32umgraun 23731 . . 3
34 eupap1.f . . 3
3533, 34syl6breqr 4449 . 2
36 peano2nn0 10758 . . . 4
3722, 36syl 16 . . 3
38 eupaf1o 24060 . . . . . . . 8
3911, 1, 38syl2anc 661 . . . . . . 7
4019oveq2d 6238 . . . . . . . 8
41 f1oeq2 5755 . . . . . . . 8
4240, 41syl 16 . . . . . . 7
4339, 42mpbird 232 . . . . . 6
44 f1osng 5801 . . . . . . 7
4537, 2, 44syl2anc 661 . . . . . 6
46 fzp1disj 11660 . . . . . . 7
4746a1i 11 . . . . . 6
48 f1oun 5782 . . . . . 6
4943, 45, 47, 10, 48syl22anc 1220 . . . . 5
50 eupap1.h . . . . . 6
51 f1oeq1 5754 . . . . . 6
5250, 51ax-mp 5 . . . . 5
5349, 52sylibr 212 . . . 4
54 1z 10814 . . . . . 6
55 1m1e0 10528 . . . . . . . 8
5655fveq2i 5816 . . . . . . 7
5724, 56syl6eleqr 2553 . . . . . 6
58 fzsuc2 11659 . . . . . 6
5954, 57, 58sylancr 663 . . . . 5
60 f1oeq2 5755 . . . . 5
6159, 60syl 16 . . . 4
6253, 61mpbird 232 . . 3
6327feq2d 5667 . . . . . 6
6418, 63mpbird 232 . . . . 5
65 f1osng 5801 . . . . . . . 8
6637, 30, 65syl2anc 661 . . . . . . 7
67 f1of 5763 . . . . . . 7
6866, 67syl 16 . . . . . 6
6930snssd 4135 . . . . . 6
70 fss 5687 . . . . . 6
7168, 69, 70syl2anc 661 . . . . 5
72 fzp1disj 11660 . . . . . 6
7372a1i 11 . . . . 5
74 fun2 5697 . . . . 5
7564, 71, 73, 74syl21anc 1218 . . . 4
76 eupap1.q . . . . . 6
7776a1i 11 . . . . 5
78 fzsuc 11647 . . . . . 6
7924, 78syl 16 . . . . 5
8077, 79feq12d 5668 . . . 4
8175, 80mpbird 232 . . 3
8234fveq1i 5814 . . . . . . . 8
83 f1of 5763 . . . . . . . . . . . . 13
8443, 83syl 16 . . . . . . . . . . . 12
8584ffvelrnda 5966 . . . . . . . . . . 11
868adantr 465 . . . . . . . . . . 11
87 nelne2 2783 . . . . . . . . . . 11
8885, 86, 87syl2anc 661 . . . . . . . . . 10
8988necomd 2724 . . . . . . . . 9
90 fvunsn 6035 . . . . . . . . 9
9189, 90syl 16 . . . . . . . 8
9282, 91syl5eq 2507 . . . . . . 7
9350fveq1i 5814 . . . . . . . . 9
94 elfznn 11623 . . . . . . . . . . . . 13
9594adantl 466 . . . . . . . . . . . 12
9695nnred 10475 . . . . . . . . . . 11
9722nn0red 10775 . . . . . . . . . . . . 13
9897adantr 465 . . . . . . . . . . . 12
9937nn0red 10775 . . . . . . . . . . . . 13
10099adantr 465 . . . . . . . . . . . 12
101 elfzle2 11600 . . . . . . . . . . . . 13
102101adantl 466 . . . . . . . . . . . 12
10397ltp1d 10400 . . . . . . . . . . . . 13
104103adantr 465 . . . . . . . . . . . 12
10596, 98, 100, 102, 104lelttrd 9666 . . . . . . . . . . 11
10696, 105gtned 9646 . . . . . . . . . 10
107 fvunsn 6035 . . . . . . . . . 10
108106, 107syl 16 . . . . . . . . 9
10993, 108syl5eq 2507 . . . . . . . 8
110109fveq2d 5817 . . . . . . 7
11176fveq1i 5814 . . . . . . . . . 10
112 peano2rem 9812 . . . . . . . . . . . . 13
11396, 112syl 16 . . . . . . . . . . . 12
11496ltm1d 10402 . . . . . . . . . . . . 13
115113, 96, 100, 114, 105lttrd 9669 . . . . . . . . . . . 12
116113, 115gtned 9646 . . . . . . . . . . 11
117 fvunsn 6035 . . . . . . . . . . 11
118116, 117syl 16 . . . . . . . . . 10
119111, 118syl5eq 2507 . . . . . . . . 9
12076fveq1i 5814 . . . . . . . . . 10
121 fvunsn 6035 . . . . . . . . . . 11
122106, 121syl 16 . . . . . . . . . 10
123120, 122syl5eq 2507 . . . . . . . . 9
124119, 123preq12d 4079 . . . . . . . 8
12511adantr 465 . . . . . . . . 9
12640eleq2d 2524 . . . . . . . . . 10
127126biimpa 484 . . . . . . . . 9
128 eupaseg 24063 . . . . . . . . 9
129125, 127, 128syl2anc 661 . . . . . . . 8
130124, 129eqtr4d 2498 . . . . . . 7
13192, 110, 1303eqtr4d 2505 . . . . . 6
132131ralrimiva 2831 . . . . 5
13334fveq1i 5814 . . . . . . . . . 10
134 fnun 5636 . . . . . . . . . . . . 13
1351, 7, 10, 134syl21anc 1218 . . . . . . . . . . . 12
136 fnfun 5627 . . . . . . . . . . . 12
137135, 136syl 16 . . . . . . . . . . 11
138 ssun2 3634 . . . . . . . . . . . 12
139138a1i 11 . . . . . . . . . . 11
140 snidg 4019 . . . . . . . . . . . . 13
1412, 140syl 16 . . . . . . . . . . . 12
1423dmsnop 5432 . . . . . . . . . . . 12
143141, 142syl6eleqr 2553 . . . . . . . . . . 11
144 funssfv 5828 . . . . . . . . . . 11
145137, 139, 143, 144syl3anc 1219 . . . . . . . . . 10
146133, 145syl5eq 2507 . . . . . . . . 9
147 fvsng 6037 . . . . . . . . . 10
1482, 3, 147sylancl 662 . . . . . . . . 9
149146, 148eqtrd 2495 . . . . . . . 8
15050fveq1i 5814 . . . . . . . . . . 11
151 f1ofun 5765 . . . . . . . . . . . . 13
15249, 151syl 16 . . . . . . . . . . . 12
153 ssun2 3634 . . . . . . . . . . . . 13
154153a1i 11 . . . . . . . . . . . 12
155 snidg 4019 . . . . . . . . . . . . . 14
15637, 155syl 16 . . . . . . . . . . . . 13
157 dmsnopg 5429 . . . . . . . . . . . . . 14
1582, 157syl 16 . . . . . . . . . . . . 13
159156, 158eleqtrrd 2545 . . . . . . . . . . . 12
160 funssfv 5828 . . . . . . . . . . . 12
161152, 154, 159, 160syl3anc 1219 . . . . . . . . . . 11
162150, 161syl5eq 2507 . . . . . . . . . 10
163 fvsng 6037 . . . . . . . . . . 11
16437, 2, 163syl2anc 661 . . . . . . . . . 10
165162, 164eqtrd 2495 . . . . . . . . 9
166165fveq2d 5817 . . . . . . . 8
16797recnd 9549 . . . . . . . . . . . 12
168 ax-1cn 9477 . . . . . . . . . . . 12
169 pncan 9753 . . . . . . . . . . . 12
170167, 168, 169sylancl 662 . . . . . . . . . . 11
171170fveq2d 5817 . . . . . . . . . 10
17276fveq1i 5814 . . . . . . . . . . 11
17397, 103gtned 9646 . . . . . . . . . . . 12
174 fvunsn 6035 . . . . . . . . . . . 12
175173, 174syl 16 . . . . . . . . . . 11
176172, 175syl5eq 2507 . . . . . . . . . 10
177171, 176eqtrd 2495 . . . . . . . . 9
17876fveq1i 5814 . . . . . . . . . . 11
179 ffun 5681 . . . . . . . . . . . . 13
18075, 179syl 16 . . . . . . . . . . . 12
181 ssun2 3634 . . . . . . . . . . . . 13
182181a1i 11 . . . . . . . . . . . 12
183 dmsnopg 5429 . . . . . . . . . . . . . 14
18430, 183syl 16 . . . . . . . . . . . . 13
185156, 184eleqtrrd 2545 . . . . . . . . . . . 12
186 funssfv 5828 . . . . . . . . . . . 12
187180, 182, 185, 186syl3anc 1219 . . . . . . . . . . 11
188178, 187syl5eq 2507 . . . . . . . . . 10
189 fvsng 6037 . . . . . . . . . . 11
19037, 30, 189syl2anc 661 . . . . . . . . . 10
191188, 190eqtrd 2495 . . . . . . . . 9
192177, 191preq12d 4079 . . . . . . . 8
193149, 166, 1923eqtr4d 2505 . . . . . . 7
194 elsni 4018 . . . . . . . . . 10
195194fveq2d 5817 . . . . . . . . 9
196195fveq2d 5817 . . . . . . . 8
197194oveq1d 6237 . . . . . . . . . 10
198197fveq2d 5817 . . . . . . . . 9
199194fveq2d 5817 . . . . . . . . 9
200198, 199preq12d 4079 . . . . . . . 8
201196, 200eqeq12d 2476 . . . . . . 7
202193, 201syl5ibrcom 222 . . . . . 6
203202ralrimiv 2829 . . . . 5
204 ralun 3652 . . . . 5
205132, 203, 204syl2anc 661 . . . 4
20659raleqdv 3032 . . . 4
207205, 206mpbird 232 . . 3
208 oveq2 6230 . . . . . 6
209 f1oeq2 5755 . . . . . 6
210208, 209syl 16 . . . . 5
211 oveq2 6230 . . . . . 6
212211feq2d 5667 . . . . 5
213208raleqdv 3032 . . . . 5
214210, 212, 2133anbi123d 1290 . . . 4
215214rspcev 3182 . . 3
21637, 62, 81, 207, 215syl13anc 1221 . 2
21734fneq1i 5624 . . . . 5
218135, 217sylibr 212 . . . 4
219 fndm 5629 . . . 4
220218, 219syl 16 . . 3
221 iseupa 24055 . . 3
222220, 221syl 16 . 2
22335, 216, 222mpbir2and 913 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  <->wb 184  /\wa 369  /\w3a 965  =wceq 1370  e.wcel 1758  =/=wne 2648  A.wral 2800  E.wrex 2801   cvv 3081  u.cun 3440  i^icin 3441  C_wss 3442   c0 3751  {csn 3993  {cpr 3995  <.cop 3999   class class class wbr 4409  domcdm 4957  Funwfun 5531  Fnwfn 5532  -->wf 5533  -1-1-onto->wf1o 5536  `cfv 5537  (class class class)co 6222   cfn 7444   cc 9417   cr 9418  0cc0 9419  1c1 9420   caddc 9422   clt 9555   cle 9556   cmin 9732   cn 10460   cn0 10717   cz 10784   cuz 11000   cfz 11582   chash 12260   cumg 23715   ceup 24052
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-rep 4520  ax-sep 4530  ax-nul 4538  ax-pow 4587  ax-pr 4648  ax-un 6505  ax-cnex 9475  ax-resscn 9476  ax-1cn 9477  ax-icn 9478  ax-addcl 9479  ax-addrcl 9480  ax-mulcl 9481  ax-mulrcl 9482  ax-mulcom 9483  ax-addass 9484  ax-mulass 9485  ax-distr 9486  ax-i2m1 9487  ax-1ne0 9488  ax-1rid 9489  ax-rnegex 9490  ax-rrecex 9491  ax-cnre 9492  ax-pre-lttri 9493  ax-pre-lttrn 9494  ax-pre-ltadd 9495  ax-pre-mulgt0 9496
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-nel 2651  df-ral 2805  df-rex 2806  df-reu 2807  df-rmo 2808  df-rab 2809  df-v 3083  df-sbc 3298  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-pss 3458  df-nul 3752  df-if 3906  df-pw 3978  df-sn 3994  df-pr 3996  df-tp 3998  df-op 4000  df-uni 4209  df-int 4246  df-iun 4290  df-br 4410  df-opab 4468  df-mpt 4469  df-tr 4503  df-eprel 4749  df-id 4753  df-po 4758  df-so 4759  df-fr 4796  df-we 4798  df-ord 4839  df-on 4840  df-lim 4841  df-suc 4842  df-xp 4963  df-rel 4964  df-cnv 4965  df-co 4966  df-dm 4967  df-rn 4968  df-res 4969  df-ima 4970  df-iota 5500  df-fun 5539  df-fn 5540  df-f 5541  df-f1 5542  df-fo 5543  df-f1o 5544  df-fv 5545  df-riota 6183  df-ov 6225  df-oprab 6226  df-mpt2 6227  df-om 6610  df-1st 6710  df-2nd 6711  df-recs 6966  df-rdg 7000  df-1o 7054  df-oadd 7058  df-er 7235  df-pm 7351  df-en 7445  df-dom 7446  df-sdom 7447  df-fin 7448  df-card 8246  df-cda 8474  df-pnf 9557  df-mnf 9558  df-xr 9559  df-ltxr 9560  df-le 9561  df-sub 9734  df-neg 9735  df-nn 10461  df-2 10518  df-n0 10718  df-z 10785  df-uz 11001  df-fz 11583  df-hash 12261  df-umgra 23716  df-eupa 24053
  Copyright terms: Public domain W3C validator