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

Theorem constr3trllem2 21630
Description: Lemma for constr3trl 21638. (Contributed by Alexander van der Vekens, 12-Nov-2017.)
Hypotheses
Ref Expression
constr3cycl.f
constr3cycl.p
Assertion
Ref Expression
constr3trllem2

Proof of Theorem constr3trllem2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 constr3cycl.f . . . . . 6
2 constr3cycl.p . . . . . 6
31, 2constr3trllem1 21629 . . . . 5
4 wrdf 11725 . . . . 5
53, 4syl 16 . . . 4
61, 2constr3lem2 21625 . . . . 5
7 usgraf1o 21374 . . . . . . . . . . . 12
8 3cycl3dv 21621 . . . . . . . . . . . . . 14
9 usgraedgrnv 21389 . . . . . . . . . . . . . . . . . . . 20
109ex 424 . . . . . . . . . . . . . . . . . . 19
11 usgraedgrnv 21389 . . . . . . . . . . . . . . . . . . . 20
1211ex 424 . . . . . . . . . . . . . . . . . . 19
1310, 12anim12d 547 . . . . . . . . . . . . . . . . . 18
1413com12 29 . . . . . . . . . . . . . . . . 17
15143adant2 976 . . . . . . . . . . . . . . . 16
1615impcom 420 . . . . . . . . . . . . . . 15
171, 2constr3lem5 21627 . . . . . . . . . . . . . . . . 17
1817jctl 526 . . . . . . . . . . . . . . . 16
1918exp31 588 . . . . . . . . . . . . . . 15
2016, 19mpancom 651 . . . . . . . . . . . . . 14
218, 20mpd 15 . . . . . . . . . . . . 13
2221ex 424 . . . . . . . . . . . 12
237, 22mpid 39 . . . . . . . . . . 11
2423imp 419 . . . . . . . . . 10
2524adantl 453 . . . . . . . . 9
26 c0ex 9077 . . . . . . . . . . 11
27 1ex 9078 . . . . . . . . . . 11
28 2z 10304 . . . . . . . . . . 11
2926, 27, 283pm3.2i 1132 . . . . . . . . . 10
30 eqidd 2436 . . . . . . . . . . . . . . 15
3130a1i 11 . . . . . . . . . . . . . 14
32 f1of1 5665 . . . . . . . . . . . . . . . . . . 19
3332adantl 453 . . . . . . . . . . . . . . . . . 18
34 3simpa 954 . . . . . . . . . . . . . . . . . . . 20
3534adantl 453 . . . . . . . . . . . . . . . . . . 19
3635ad3antlr 712 . . . . . . . . . . . . . . . . . 18
37 f1ocnvfvrneq 6011 . . . . . . . . . . . . . . . . . 18
3833, 36, 37syl2anc 643 . . . . . . . . . . . . . . . . 17
39 simpl 444 . . . . . . . . . . . . . . . . . . . . . . 23
40 simpr 448 . . . . . . . . . . . . . . . . . . . . . . . 24
41 simpl 444 . . . . . . . . . . . . . . . . . . . . . . . 24
4240, 41anim12i 550 . . . . . . . . . . . . . . . . . . . . . . 23
43 preq12bg 3969 . . . . . . . . . . . . . . . . . . . . . . 23
4439, 42, 43syl2anc 643 . . . . . . . . . . . . . . . . . . . . . 22
45 df-ne 2600 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
46 pm2.21 102 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
4745, 46sylbi 188 . . . . . . . . . . . . . . . . . . . . . . . . . 26
48473ad2ant1 978 . . . . . . . . . . . . . . . . . . . . . . . . 25
4948com12 29 . . . . . . . . . . . . . . . . . . . . . . . 24
5049adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23
51 df-ne 2600 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
52 pm2.21 102 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
5351, 52sylbi 188 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
54533ad2ant3 980 . . . . . . . . . . . . . . . . . . . . . . . . . 26
5554com12 29 . . . . . . . . . . . . . . . . . . . . . . . . 25
5655eqcoms 2438 . . . . . . . . . . . . . . . . . . . . . . . 24
5756adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23
5850, 57jaoi 369 . . . . . . . . . . . . . . . . . . . . . 22
5944, 58syl6bi 220 . . . . . . . . . . . . . . . . . . . . 21
6059com23 74 . . . . . . . . . . . . . . . . . . . 20
6160adantr 452 . . . . . . . . . . . . . . . . . . 19
6261imp 419 . . . . . . . . . . . . . . . . . 18
6362adantr 452 . . . . . . . . . . . . . . . . 17
6438, 63syld 42 . . . . . . . . . . . . . . . 16
6564adantl 453 . . . . . . . . . . . . . . 15
66 eqeq12 2447 . . . . . . . . . . . . . . . . . 18
67663adant3 977 . . . . . . . . . . . . . . . . 17
6867imbi1d 309 . . . . . . . . . . . . . . . 16
6968adantr 452 . . . . . . . . . . . . . . 15
7065, 69mpbird 224 . . . . . . . . . . . . . 14
71 3simpb 955 . . . . . . . . . . . . . . . . . . . 20
7271adantl 453 . . . . . . . . . . . . . . . . . . 19
7372ad3antlr 712 . . . . . . . . . . . . . . . . . 18
74 f1ocnvfvrneq 6011 . . . . . . . . . . . . . . . . . 18
7533, 73, 74syl2anc 643 . . . . . . . . . . . . . . . . 17
76 preq12bg 3969 . . . . . . . . . . . . . . . . . . . . . 22
77 pm2.21 102 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
7845, 77sylbi 188 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
79783ad2ant1 978 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8079com12 29 . . . . . . . . . . . . . . . . . . . . . . . . 25
8180eqcoms 2438 . . . . . . . . . . . . . . . . . . . . . . . 24
8281adantl 453 . . . . . . . . . . . . . . . . . . . . . . 23
83 df-ne 2600 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
84 pm2.21 102 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
8583, 84sylbi 188 . . . . . . . . . . . . . . . . . . . . . . . . . 26
86853ad2ant2 979 . . . . . . . . . . . . . . . . . . . . . . . . 25
8786com12 29 . . . . . . . . . . . . . . . . . . . . . . . 24
8887adantl 453 . . . . . . . . . . . . . . . . . . . . . . 23
8982, 88jaoi 369 . . . . . . . . . . . . . . . . . . . . . 22
9076, 89syl6bi 220 . . . . . . . . . . . . . . . . . . . . 21
9190com23 74 . . . . . . . . . . . . . . . . . . . 20
9291adantr 452 . . . . . . . . . . . . . . . . . . 19
9392imp 419 . . . . . . . . . . . . . . . . . 18
9493adantr 452 . . . . . . . . . . . . . . . . 17
9575, 94syld 42 . . . . . . . . . . . . . . . 16
9695adantl 453 . . . . . . . . . . . . . . 15
97 eqeq12 2447 . . . . . . . . . . . . . . . . . 18
98973adant2 976 . . . . . . . . . . . . . . . . 17
9998imbi1d 309 . . . . . . . . . . . . . . . 16
10099adantr 452 . . . . . . . . . . . . . . 15
10196, 100mpbird 224 . . . . . . . . . . . . . 14
10231, 70, 1013jca 1134 . . . . . . . . . . . . 13
103102adantl 453 . . . . . . . . . . . 12