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

Theorem vcoprnelem 26278
 Description: Lemma for vcoprne 26279. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
Assertion
Ref Expression
vcoprnelem

Proof of Theorem vcoprnelem
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vcrel 26247 . . . . 5
2 df-rel 4846 . . . . 5
31, 2mpbi 213 . . . 4
43sseli 3414 . . 3
5 opelxp1 4872 . . 3
64, 5syl 17 . 2
7 eqid 2471 . . . . . 6
87isvclem 26277 . . . . 5
98anidms 657 . . . 4
109biimpa 492 . . 3
11 simpr 468 . . . . 5
12 ablogrpo 26093 . . . . . . 7
137grpofo 26008 . . . . . . . . . 10
14 fofn 5808 . . . . . . . . . 10
1513, 14syl 17 . . . . . . . . 9
16 ffn 5739 . . . . . . . . 9
17 fndmu 5687 . . . . . . . . 9
1815, 16, 17syl2an 485 . . . . . . . 8
197grpon0 26011 . . . . . . . . . 10
20 xpcan2 5280 . . . . . . . . . 10
2119, 20syl 17 . . . . . . . . 9
2221adantr 472 . . . . . . . 8
2318, 22mpbid 215 . . . . . . 7
2412, 23sylan 479 . . . . . 6
25 xpeq2 4854 . . . . . . . 8
2625feq2d 5725 . . . . . . 7
27 feq3 5722 . . . . . . 7
2826, 27bitrd 261 . . . . . 6
2924, 28syl 17 . . . . 5
3011, 29mpbid 215 . . . 4