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

Theorem constr3trllem2 21674
Description: Lemma for constr3trl 21682. (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 21673 . . . . 5
4 wrdf 11788 . . . . 5
53, 4syl 16 . . . 4
61, 2constr3lem2 21669 . . . . 5
7 usgraf1o 21418 . . . . . . . . . . . 12
8 3cycl3dv 21665 . . . . . . . . . . . . . 14
9 usgraedgrnv 21433 . . . . . . . . . . . . . . . . . . . 20
109ex 425 . . . . . . . . . . . . . . . . . . 19
11 usgraedgrnv 21433 . . . . . . . . . . . . . . . . . . . 20
1211ex 425 . . . . . . . . . . . . . . . . . . 19
1310, 12anim12d 548 . . . . . . . . . . . . . . . . . 18
1413com12 30 . . . . . . . . . . . . . . . . 17
15143adant2 977 . . . . . . . . . . . . . . . 16
1615impcom 421 . . . . . . . . . . . . . . 15
171, 2constr3lem5 21671 . . . . . . . . . . . . . . . . 17
1817jctl 527 . . . . . . . . . . . . . . . 16
1918exp31 589 . . . . . . . . . . . . . . 15
2016, 19mpancom 652 . . . . . . . . . . . . . 14
218, 20mpd 15 . . . . . . . . . . . . 13
2221ex 425 . . . . . . . . . . . 12
237, 22mpid 40 . . . . . . . . . . 11
2423imp 420 . . . . . . . . . 10
2524adantl 454 . . . . . . . . 9
26 c0ex 9140 . . . . . . . . . . 11
27 1ex 9141 . . . . . . . . . . 11
28 2z 10367 . . . . . . . . . . 11
2926, 27, 283pm3.2i 1133 . . . . . . . . . 10
30 eqidd 2448 . . . . . . . . . . . . . . 15
3130a1i 11 . . . . . . . . . . . . . 14
32 f1of1 5724 . . . . . . . . . . . . . . . . . . 19
3332adantl 454 . . . . . . . . . . . . . . . . . 18
34 3simpa 955 . . . . . . . . . . . . . . . . . . . 20
3534adantl 454 . . . . . . . . . . . . . . . . . . 19
3635ad3antlr 713 . . . . . . . . . . . . . . . . . 18
37 f1ocnvfvrneq 6071 . . . . . . . . . . . . . . . . . 18
3833, 36, 37syl2anc 644 . . . . . . . . . . . . . . . . 17
39 simpl 445 . . . . . . . . . . . . . . . . . . . . . . 23
40 simpr 449 . . . . . . . . . . . . . . . . . . . . . . . 24
41 simpl 445 . . . . . . . . . . . . . . . . . . . . . . . 24
4240, 41anim12i 551 . . . . . . . . . . . . . . . . . . . . . . 23
43 preq12bg 4009 . . . . . . . . . . . . . . . . . . . . . . 23
4439, 42, 43syl2anc 644 . . . . . . . . . . . . . . . . . . . . . 22
45 df-ne 2612 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
46 pm2.21 103 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
4745, 46sylbi 189 . . . . . . . . . . . . . . . . . . . . . . . . . 26
48473ad2ant1 979 . . . . . . . . . . . . . . . . . . . . . . . . 25
4948com12 30 . . . . . . . . . . . . . . . . . . . . . . . 24
5049adantr 453 . . . . . . . . . . . . . . . . . . . . . . 23
51 df-ne 2612 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
52 pm2.21 103 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
5351, 52sylbi 189 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
54533ad2ant3 981 . . . . . . . . . . . . . . . . . . . . . . . . . 26
5554com12 30 . . . . . . . . . . . . . . . . . . . . . . . . 25
5655eqcoms 2450 . . . . . . . . . . . . . . . . . . . . . . . 24
5756adantr 453 . . . . . . . . . . . . . . . . . . . . . . 23
5850, 57jaoi 370 . . . . . . . . . . . . . . . . . . . . . 22
5944, 58syl6bi 221 . . . . . . . . . . . . . . . . . . . . 21
6059com23 75 . . . . . . . . . . . . . . . . . . . 20
6160adantr 453 . . . . . . . . . . . . . . . . . . 19
6261imp 420 . . . . . . . . . . . . . . . . . 18
6362adantr 453 . . . . . . . . . . . . . . . . 17
6438, 63syld 43 . . . . . . . . . . . . . . . 16
6564adantl 454 . . . . . . . . . . . . . . 15
66 eqeq12 2459 . . . . . . . . . . . . . . . . . 18
67663adant3 978 . . . . . . . . . . . . . . . . 17
6867imbi1d 310 . . . . . . . . . . . . . . . 16
6968adantr 453 . . . . . . . . . . . . . . 15
7065, 69mpbird 225 . . . . . . . . . . . . . 14
71 3simpb 956 . . . . . . . . . . . . . . . . . . . 20
7271adantl 454 . . . . . . . . . . . . . . . . . . 19
7372ad3antlr 713 . . . . . . . . . . . . . . . . . 18
74 f1ocnvfvrneq 6071 . . . . . . . . . . . . . . . . . 18
7533, 73, 74syl2anc 644 . . . . . . . . . . . . . . . . 17
76 preq12bg 4009 . . . . . . . . . . . . . . . . . . . . . 22
77 pm2.21 103 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
7845, 77sylbi 189 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
79783ad2ant1 979 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8079com12 30 . . . . . . . . . . . . . . . . . . . . . . . . 25
8180eqcoms 2450 . . . . . . . . . . . . . . . . . . . . . . . 24
8281adantl 454 . . . . . . . . . . . . . . . . . . . . . . 23
83 df-ne 2612 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
84 pm2.21 103 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
8583, 84sylbi 189 . . . . . . . . . . . . . . . . . . . . . . . . . 26
86853ad2ant2 980 . . . . . . . . . . . . . . . . . . . . . . . . 25
8786com12 30 . . . . . . . . . . . . . . . . . . . . . . . 24
8887adantl 454 . . . . . . . . . . . . . . . . . . . . . . 23
8982, 88jaoi 370 . . . . . . . . . . . . . . . . . . . . . 22
9076, 89syl6bi 221 . . . . . . . . . . . . . . . . . . . . 21
9190com23 75 . . . . . . . . . . . . . . . . . . . 20
9291adantr 453 . . . . . . . . . . . . . . . . . . 19
9392imp 420 . . . . . . . . . . . . . . . . . 18
9493adantr 453 . . . . . . . . . . . . . . . . 17
9575, 94syld 43 . . . . . . . . . . . . . . . 16
9695adantl 454 . . . . . . . . . . . . . . 15
97 eqeq12 2459 . . . . . . . . . . . . . . . . . 18
98973adant2 977 . . . . . . . . . . . . . . . . 17
9998imbi1d 310 . . . . . . . . . . . . . . . 16
10099adantr 453 . . . . . . . . . . . . . . 15
10196, 100mpbird 225 . . . . . . . . . . . . . 14
10231, 70, 1013jca 1135 . . . . . . . . . . . . 13
103102adantl 454 . . . . . . . . . . . 12