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

Theorem eupap1 24668
 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 EulPaths
eupap1.n
eupap1.f
eupap1.h
eupap1.q
Assertion
Ref Expression
eupap1 EulPaths

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 4689 . . . . . 6
4 f1osng 5853 . . . . . 6
52, 3, 4sylancl 662 . . . . 5
6 f1ofn 5816 . . . . 5
75, 6syl 16 . . . 4
8 eupap1.d . . . . 5
9 disjsn 4088 . . . . 5
108, 9sylibr 212 . . . 4
11 eupap1.g . . . . 5 EulPaths
12 eupagra 24658 . . . . 5 EulPaths UMGrph
1311, 12syl 16 . . . 4 UMGrph
14 relumgra 24006 . . . . . . 7 UMGrph
1514brrelexi 5039 . . . . . 6 UMGrph
1613, 15syl 16 . . . . 5
17 eupapf 24664 . . . . . . 7 EulPaths
1811, 17syl 16 . . . . . 6
19 eupap1.n . . . . . . . . . 10
20 eupacl 24661 . . . . . . . . . . 11 EulPaths
2111, 20syl 16 . . . . . . . . . 10
2219, 21eqeltrd 2555 . . . . . . . . 9
23 nn0uz 11115 . . . . . . . . 9
2422, 23syl6eleq 2565 . . . . . . . 8
25 eluzfz2 11693 . . . . . . . 8
2624, 25syl 16 . . . . . . 7
2719oveq2d 6299 . . . . . . 7
2826, 27eleqtrd 2557 . . . . . 6
2918, 28ffvelrnd 6021 . . . . 5
30 eupap1.c . . . . 5
31 umgra1 24018 . . . . 5 UMGrph
3216, 2, 29, 30, 31syl22anc 1229 . . . 4 UMGrph
331, 7, 10, 13, 32umgraun 24020 . . 3 UMGrph
34 eupap1.f . . 3
3533, 34syl6breqr 4487 . 2 UMGrph
36 peano2nn0 10835 . . . 4
3722, 36syl 16 . . 3
38 eupaf1o 24662 . . . . . . . 8 EulPaths
3911, 1, 38syl2anc 661 . . . . . . 7
4019oveq2d 6299 . . . . . . . 8
41 f1oeq2 5807 . . . . . . . 8
4240, 41syl 16 . . . . . . 7
4339, 42mpbird 232 . . . . . 6
44 f1osng 5853 . . . . . . 7
4537, 2, 44syl2anc 661 . . . . . 6
46 fzp1disj 11737 . . . . . . 7
4746a1i 11 . . . . . 6
48 f1oun 5834 . . . . . 6
4943, 45, 47, 10, 48syl22anc 1229 . . . . 5
50 eupap1.h . . . . . 6
51 f1oeq1 5806 . . . . . 6
5250, 51ax-mp 5 . . . . 5
5349, 52sylibr 212 . . . 4
54 1z 10893 . . . . . 6
55 1m1e0 10603 . . . . . . . 8
5655fveq2i 5868 . . . . . . 7
5724, 56syl6eleqr 2566 . . . . . 6
58 fzsuc2 11736 . . . . . 6
5954, 57, 58sylancr 663 . . . . 5
60 f1oeq2 5807 . . . . 5
6159, 60syl 16 . . . 4
6253, 61mpbird 232 . . 3
6327feq2d 5717 . . . . . 6
6418, 63mpbird 232 . . . . 5
65 f1osng 5853 . . . . . . . 8
6637, 30, 65syl2anc 661 . . . . . . 7
67 f1of 5815 . . . . . . 7
6866, 67syl 16 . . . . . 6
6930snssd 4172 . . . . . 6
70 fss 5738 . . . . . 6
7168, 69, 70syl2anc 661 . . . . 5
72 fzp1disj 11737 . . . . . 6
7372a1i 11 . . . . 5
74 fun2 5748 . . . . 5
7564, 71, 73, 74syl21anc 1227 . . . 4
76 eupap1.q . . . . . 6
7776a1i 11 . . . . 5
78 fzsuc 11726 . . . . . 6
7924, 78syl 16 . . . . 5
8077, 79feq12d 5719 . . . 4
8175, 80mpbird 232 . . 3
8234fveq1i 5866 . . . . . . . 8
83 f1of 5815 . . . . . . . . . . . . 13
8443, 83syl 16 . . . . . . . . . . . 12
8584ffvelrnda 6020 . . . . . . . . . . 11
868adantr 465 . . . . . . . . . . 11
87 nelne2 2797 . . . . . . . . . . 11
8885, 86, 87syl2anc 661 . . . . . . . . . 10
8988necomd 2738 . . . . . . . . 9
90 fvunsn 6092 . . . . . . . . 9
9189, 90syl 16 . . . . . . . 8
9282, 91syl5eq 2520 . . . . . . 7
9350fveq1i 5866 . . . . . . . . 9
94 elfznn 11713 . . . . . . . . . . . . 13
9594adantl 466 . . . . . . . . . . . 12
9695nnred 10550 . . . . . . . . . . 11
9722nn0red 10852 . . . . . . . . . . . . 13
9897adantr 465 . . . . . . . . . . . 12
9937nn0red 10852 . . . . . . . . . . . . 13
10099adantr 465 . . . . . . . . . . . 12
101 elfzle2 11689 . . . . . . . . . . . . 13
102101adantl 466 . . . . . . . . . . . 12
10397ltp1d 10475 . . . . . . . . . . . . 13
104103adantr 465 . . . . . . . . . . . 12
10596, 98, 100, 102, 104lelttrd 9738 . . . . . . . . . . 11
10696, 105gtned 9718 . . . . . . . . . 10
107 fvunsn 6092 . . . . . . . . . 10
108106, 107syl 16 . . . . . . . . 9
10993, 108syl5eq 2520 . . . . . . . 8
110109fveq2d 5869 . . . . . . 7
11176fveq1i 5866 . . . . . . . . . 10
112 peano2rem 9885 . . . . . . . . . . . . 13
11396, 112syl 16 . . . . . . . . . . . 12
11496ltm1d 10477 . . . . . . . . . . . . 13
115113, 96, 100, 114, 105lttrd 9741 . . . . . . . . . . . 12
116113, 115gtned 9718 . . . . . . . . . . 11
117 fvunsn 6092 . . . . . . . . . . 11
118116, 117syl 16 . . . . . . . . . 10
119111, 118syl5eq 2520 . . . . . . . . 9
12076fveq1i 5866 . . . . . . . . . 10
121 fvunsn 6092 . . . . . . . . . . 11
122106, 121syl 16 . . . . . . . . . 10
123120, 122syl5eq 2520 . . . . . . . . 9
124119, 123preq12d 4114 . . . . . . . 8
12511adantr 465 . . . . . . . . 9 EulPaths
12640eleq2d 2537 . . . . . . . . . 10
127126biimpa 484 . . . . . . . . 9
128 eupaseg 24665 . . . . . . . . 9 EulPaths
129125, 127, 128syl2anc 661 . . . . . . . 8
130124, 129eqtr4d 2511 . . . . . . 7
13192, 110, 1303eqtr4d 2518 . . . . . 6
132131ralrimiva 2878 . . . . 5
13334fveq1i 5866 . . . . . . . . . 10
134 fnun 5686 . . . . . . . . . . . . 13
1351, 7, 10, 134syl21anc 1227 . . . . . . . . . . . 12
136 fnfun 5677 . . . . . . . . . . . 12
137135, 136syl 16 . . . . . . . . . . 11
138 ssun2 3668 . . . . . . . . . . . 12
139138a1i 11 . . . . . . . . . . 11
140 snidg 4053 . . . . . . . . . . . . 13
1412, 140syl 16 . . . . . . . . . . . 12
1423dmsnop 5481 . . . . . . . . . . . 12
143141, 142syl6eleqr 2566 . . . . . . . . . . 11
144 funssfv 5880 . . . . . . . . . . 11
145137, 139, 143, 144syl3anc 1228 . . . . . . . . . 10
146133, 145syl5eq 2520 . . . . . . . . 9
147 fvsng 6094 . . . . . . . . . 10
1482, 3, 147sylancl 662 . . . . . . . . 9
149146, 148eqtrd 2508 . . . . . . . 8
15050fveq1i 5866 . . . . . . . . . . 11
151 f1ofun 5817 . . . . . . . . . . . . 13
15249, 151syl 16 . . . . . . . . . . . 12
153 ssun2 3668 . . . . . . . . . . . . 13
154153a1i 11 . . . . . . . . . . . 12
155 snidg 4053 . . . . . . . . . . . . . 14
15637, 155syl 16 . . . . . . . . . . . . 13
157 dmsnopg 5478 . . . . . . . . . . . . . 14
1582, 157syl 16 . . . . . . . . . . . . 13
159156, 158eleqtrrd 2558 . . . . . . . . . . . 12
160 funssfv 5880 . . . . . . . . . . . 12
161152, 154, 159, 160syl3anc 1228 . . . . . . . . . . 11
162150, 161syl5eq 2520 . . . . . . . . . 10
163 fvsng 6094 . . . . . . . . . . 11
16437, 2, 163syl2anc 661 . . . . . . . . . 10
165162, 164eqtrd 2508 . . . . . . . . 9
166165fveq2d 5869 . . . . . . . 8
16797recnd 9621 . . . . . . . . . . . 12
168 ax-1cn 9549 . . . . . . . . . . . 12
169 pncan 9825 . . . . . . . . . . . 12
170167, 168, 169sylancl 662 . . . . . . . . . . 11
171170fveq2d 5869 . . . . . . . . . 10
17276fveq1i 5866 . . . . . . . . . . 11
17397, 103gtned 9718 . . . . . . . . . . . 12
174 fvunsn 6092 . . . . . . . . . . . 12
175173, 174syl 16 . . . . . . . . . . 11
176172, 175syl5eq 2520 . . . . . . . . . 10
177171, 176eqtrd 2508 . . . . . . . . 9
17876fveq1i 5866 . . . . . . . . . . 11
179 ffun 5732 . . . . . . . . . . . . 13
18075, 179syl 16 . . . . . . . . . . . 12
181 ssun2 3668 . . . . . . . . . . . . 13
182181a1i 11 . . . . . . . . . . . 12
183 dmsnopg 5478 . . . . . . . . . . . . . 14
18430, 183syl 16 . . . . . . . . . . . . 13
185156, 184eleqtrrd 2558 . . . . . . . . . . . 12
186 funssfv 5880 . . . . . . . . . . . 12
187180, 182, 185, 186syl3anc 1228 . . . . . . . . . . 11
188178, 187syl5eq 2520 . . . . . . . . . 10
189 fvsng 6094 . . . . . . . . . . 11
19037, 30, 189syl2anc 661 . . . . . . . . . 10
191188, 190eqtrd 2508 . . . . . . . . 9
192177, 191preq12d 4114 . . . . . . . 8
193149, 166, 1923eqtr4d 2518 . . . . . . 7
194 elsni 4052 . . . . . . . . . 10
195194fveq2d 5869 . . . . . . . . 9
196195fveq2d 5869 . . . . . . . 8
197194oveq1d 6298 . . . . . . . . . 10
198197fveq2d 5869 . . . . . . . . 9
199194fveq2d 5869 . . . . . . . . 9
200198, 199preq12d 4114 . . . . . . . 8
201196, 200eqeq12d 2489 . . . . . . 7
202193, 201syl5ibrcom 222 . . . . . 6
203202ralrimiv 2876 . . . . 5
204 ralun 3686 . . . . 5
205132, 203, 204syl2anc 661 . . . 4
20659raleqdv 3064 . . . 4
207205, 206mpbird 232 . . 3
208 oveq2 6291 . . . . . 6
209 f1oeq2 5807 . . . . . 6
210208, 209syl 16 . . . . 5
211 oveq2 6291 . . . . . 6
212211feq2d 5717 . . . . 5
213208raleqdv 3064 . . . . 5
214210, 212, 2133anbi123d 1299 . . . 4
215214rspcev 3214 . . 3
21637, 62, 81, 207, 215syl13anc 1230 . 2
21734fneq1i 5674 . . . . 5
218135, 217sylibr 212 . . . 4
219 fndm 5679 . . . 4
220218, 219syl 16 . . 3
221 iseupa 24657 . . 3 EulPaths UMGrph
222220, 221syl 16 . 2 EulPaths UMGrph
22335, 216, 222mpbir2and 920 1 EulPaths
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 184   wa 369   w3a 973   wceq 1379   wcel 1767   wne 2662  wral 2814  wrex 2815  cvv 3113   cun 3474   cin 3475   wss 3476  c0 3785  csn 4027  cpr 4029  cop 4033   class class class wbr 4447   cdm 4999   wfun 5581   wfn 5582  wf 5583  wf1o 5586  cfv 5587  (class class class)co 6283  cfn 7516  cc 9489  cr 9490  cc0 9491  c1 9492   caddc 9494   clt 9627   cle 9628   cmin 9804  cn 10535  cn0 10794  cz 10863  cuz 11081  cfz 11671  chash 12372   UMGrph cumg 24004   EulPaths ceup 24654 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-rep 4558  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686  ax-un 6575  ax-cnex 9547  ax-resscn 9548  ax-1cn 9549  ax-icn 9550  ax-addcl 9551  ax-addrcl 9552  ax-mulcl 9553  ax-mulrcl 9554  ax-mulcom 9555  ax-addass 9556  ax-mulass 9557  ax-distr 9558  ax-i2m1 9559  ax-1ne0 9560  ax-1rid 9561  ax-rnegex 9562  ax-rrecex 9563  ax-cnre 9564  ax-pre-lttri 9565  ax-pre-lttrn 9566  ax-pre-ltadd 9567  ax-pre-mulgt0 9568 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2819  df-rex 2820  df-reu 2821  df-rmo 2822  df-rab 2823  df-v 3115  df-sbc 3332  df-csb 3436  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-pw 4012  df-sn 4028  df-pr 4030  df-tp 4032  df-op 4034  df-uni 4246  df-int 4283  df-iun 4327  df-br 4448  df-opab 4506  df-mpt 4507  df-tr 4541  df-eprel 4791  df-id 4795  df-po 4800  df-so 4801  df-fr 4838  df-we 4840  df-ord 4881  df-on 4882  df-lim 4883  df-suc 4884  df-xp 5005  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-res 5011  df-ima 5012  df-iota 5550  df-fun 5589  df-fn 5590  df-f 5591  df-f1 5592  df-fo 5593  df-f1o 5594  df-fv 5595  df-riota 6244  df-ov 6286  df-oprab 6287  df-mpt2 6288  df-om 6680  df-1st 6784  df-2nd 6785  df-recs 7042  df-rdg 7076  df-1o 7130  df-oadd 7134  df-er 7311  df-pm 7423  df-en 7517  df-dom 7518  df-sdom 7519  df-fin 7520  df-card 8319  df-cda 8547  df-pnf 9629  df-mnf 9630  df-xr 9631  df-ltxr 9632  df-le 9633  df-sub 9806  df-neg 9807  df-nn 10536  df-2 10593  df-n0 10795  df-z 10864  df-uz 11082  df-fz 11672  df-hash 12373  df-umgra 24005  df-eupa 24655 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator