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

Theorem dprdf1o 19951
Description: Rearrange the index set of a direct product family. (Contributed by Mario Carneiro, 25-Apr-2016.)
Hypotheses
Ref Expression
dprdf1o.1 (๐œ‘ โ†’ ๐บdom DProd ๐‘†)
dprdf1o.2 (๐œ‘ โ†’ dom ๐‘† = ๐ผ)
dprdf1o.3 (๐œ‘ โ†’ ๐น:๐ฝโ€“1-1-ontoโ†’๐ผ)
Assertion
Ref Expression
dprdf1o (๐œ‘ โ†’ (๐บdom DProd (๐‘† โˆ˜ ๐น) โˆง (๐บ DProd (๐‘† โˆ˜ ๐น)) = (๐บ DProd ๐‘†)))

Proof of Theorem dprdf1o
Dummy variables ๐‘ฅ ๐‘ฆ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2726 . . 3 (Cntzโ€˜๐บ) = (Cntzโ€˜๐บ)
2 eqid 2726 . . 3 (0gโ€˜๐บ) = (0gโ€˜๐บ)
3 eqid 2726 . . 3 (mrClsโ€˜(SubGrpโ€˜๐บ)) = (mrClsโ€˜(SubGrpโ€˜๐บ))
4 dprdf1o.1 . . . 4 (๐œ‘ โ†’ ๐บdom DProd ๐‘†)
5 dprdgrp 19924 . . . 4 (๐บdom DProd ๐‘† โ†’ ๐บ โˆˆ Grp)
64, 5syl 17 . . 3 (๐œ‘ โ†’ ๐บ โˆˆ Grp)
7 dprdf1o.3 . . . . 5 (๐œ‘ โ†’ ๐น:๐ฝโ€“1-1-ontoโ†’๐ผ)
8 f1of1 6825 . . . . 5 (๐น:๐ฝโ€“1-1-ontoโ†’๐ผ โ†’ ๐น:๐ฝโ€“1-1โ†’๐ผ)
97, 8syl 17 . . . 4 (๐œ‘ โ†’ ๐น:๐ฝโ€“1-1โ†’๐ผ)
10 dprdf1o.2 . . . . 5 (๐œ‘ โ†’ dom ๐‘† = ๐ผ)
114, 10dprddomcld 19920 . . . 4 (๐œ‘ โ†’ ๐ผ โˆˆ V)
12 f1dmex 7939 . . . 4 ((๐น:๐ฝโ€“1-1โ†’๐ผ โˆง ๐ผ โˆˆ V) โ†’ ๐ฝ โˆˆ V)
139, 11, 12syl2anc 583 . . 3 (๐œ‘ โ†’ ๐ฝ โˆˆ V)
144, 10dprdf2 19926 . . . 4 (๐œ‘ โ†’ ๐‘†:๐ผโŸถ(SubGrpโ€˜๐บ))
15 f1of 6826 . . . . 5 (๐น:๐ฝโ€“1-1-ontoโ†’๐ผ โ†’ ๐น:๐ฝโŸถ๐ผ)
167, 15syl 17 . . . 4 (๐œ‘ โ†’ ๐น:๐ฝโŸถ๐ผ)
17 fco 6734 . . . 4 ((๐‘†:๐ผโŸถ(SubGrpโ€˜๐บ) โˆง ๐น:๐ฝโŸถ๐ผ) โ†’ (๐‘† โˆ˜ ๐น):๐ฝโŸถ(SubGrpโ€˜๐บ))
1814, 16, 17syl2anc 583 . . 3 (๐œ‘ โ†’ (๐‘† โˆ˜ ๐น):๐ฝโŸถ(SubGrpโ€˜๐บ))
194adantr 480 . . . . 5 ((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ ๐ฝ โˆง ๐‘ฅ โ‰  ๐‘ฆ)) โ†’ ๐บdom DProd ๐‘†)
2010adantr 480 . . . . 5 ((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ ๐ฝ โˆง ๐‘ฅ โ‰  ๐‘ฆ)) โ†’ dom ๐‘† = ๐ผ)
2116adantr 480 . . . . . 6 ((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ ๐ฝ โˆง ๐‘ฅ โ‰  ๐‘ฆ)) โ†’ ๐น:๐ฝโŸถ๐ผ)
22 simpr1 1191 . . . . . 6 ((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ ๐ฝ โˆง ๐‘ฅ โ‰  ๐‘ฆ)) โ†’ ๐‘ฅ โˆˆ ๐ฝ)
2321, 22ffvelcdmd 7080 . . . . 5 ((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ ๐ฝ โˆง ๐‘ฅ โ‰  ๐‘ฆ)) โ†’ (๐นโ€˜๐‘ฅ) โˆˆ ๐ผ)
24 simpr2 1192 . . . . . 6 ((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ ๐ฝ โˆง ๐‘ฅ โ‰  ๐‘ฆ)) โ†’ ๐‘ฆ โˆˆ ๐ฝ)
2521, 24ffvelcdmd 7080 . . . . 5 ((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ ๐ฝ โˆง ๐‘ฅ โ‰  ๐‘ฆ)) โ†’ (๐นโ€˜๐‘ฆ) โˆˆ ๐ผ)
26 simpr3 1193 . . . . . 6 ((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ ๐ฝ โˆง ๐‘ฅ โ‰  ๐‘ฆ)) โ†’ ๐‘ฅ โ‰  ๐‘ฆ)
279adantr 480 . . . . . . . 8 ((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ ๐ฝ โˆง ๐‘ฅ โ‰  ๐‘ฆ)) โ†’ ๐น:๐ฝโ€“1-1โ†’๐ผ)
28 f1fveq 7256 . . . . . . . 8 ((๐น:๐ฝโ€“1-1โ†’๐ผ โˆง (๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ ๐ฝ)) โ†’ ((๐นโ€˜๐‘ฅ) = (๐นโ€˜๐‘ฆ) โ†” ๐‘ฅ = ๐‘ฆ))
2927, 22, 24, 28syl12anc 834 . . . . . . 7 ((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ ๐ฝ โˆง ๐‘ฅ โ‰  ๐‘ฆ)) โ†’ ((๐นโ€˜๐‘ฅ) = (๐นโ€˜๐‘ฆ) โ†” ๐‘ฅ = ๐‘ฆ))
3029necon3bid 2979 . . . . . 6 ((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ ๐ฝ โˆง ๐‘ฅ โ‰  ๐‘ฆ)) โ†’ ((๐นโ€˜๐‘ฅ) โ‰  (๐นโ€˜๐‘ฆ) โ†” ๐‘ฅ โ‰  ๐‘ฆ))
3126, 30mpbird 257 . . . . 5 ((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ ๐ฝ โˆง ๐‘ฅ โ‰  ๐‘ฆ)) โ†’ (๐นโ€˜๐‘ฅ) โ‰  (๐นโ€˜๐‘ฆ))
3219, 20, 23, 25, 31, 1dprdcntz 19927 . . . 4 ((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ ๐ฝ โˆง ๐‘ฅ โ‰  ๐‘ฆ)) โ†’ (๐‘†โ€˜(๐นโ€˜๐‘ฅ)) โІ ((Cntzโ€˜๐บ)โ€˜(๐‘†โ€˜(๐นโ€˜๐‘ฆ))))
33 fvco3 6983 . . . . 5 ((๐น:๐ฝโŸถ๐ผ โˆง ๐‘ฅ โˆˆ ๐ฝ) โ†’ ((๐‘† โˆ˜ ๐น)โ€˜๐‘ฅ) = (๐‘†โ€˜(๐นโ€˜๐‘ฅ)))
3421, 22, 33syl2anc 583 . . . 4 ((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ ๐ฝ โˆง ๐‘ฅ โ‰  ๐‘ฆ)) โ†’ ((๐‘† โˆ˜ ๐น)โ€˜๐‘ฅ) = (๐‘†โ€˜(๐นโ€˜๐‘ฅ)))
35 fvco3 6983 . . . . . 6 ((๐น:๐ฝโŸถ๐ผ โˆง ๐‘ฆ โˆˆ ๐ฝ) โ†’ ((๐‘† โˆ˜ ๐น)โ€˜๐‘ฆ) = (๐‘†โ€˜(๐นโ€˜๐‘ฆ)))
3621, 24, 35syl2anc 583 . . . . 5 ((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ ๐ฝ โˆง ๐‘ฅ โ‰  ๐‘ฆ)) โ†’ ((๐‘† โˆ˜ ๐น)โ€˜๐‘ฆ) = (๐‘†โ€˜(๐นโ€˜๐‘ฆ)))
3736fveq2d 6888 . . . 4 ((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ ๐ฝ โˆง ๐‘ฅ โ‰  ๐‘ฆ)) โ†’ ((Cntzโ€˜๐บ)โ€˜((๐‘† โˆ˜ ๐น)โ€˜๐‘ฆ)) = ((Cntzโ€˜๐บ)โ€˜(๐‘†โ€˜(๐นโ€˜๐‘ฆ))))
3832, 34, 373sstr4d 4024 . . 3 ((๐œ‘ โˆง (๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ ๐ฝ โˆง ๐‘ฅ โ‰  ๐‘ฆ)) โ†’ ((๐‘† โˆ˜ ๐น)โ€˜๐‘ฅ) โІ ((Cntzโ€˜๐บ)โ€˜((๐‘† โˆ˜ ๐น)โ€˜๐‘ฆ)))
3916, 33sylan 579 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ฝ) โ†’ ((๐‘† โˆ˜ ๐น)โ€˜๐‘ฅ) = (๐‘†โ€˜(๐นโ€˜๐‘ฅ)))
40 imaco 6243 . . . . . . . . 9 ((๐‘† โˆ˜ ๐น) โ€œ (๐ฝ โˆ– {๐‘ฅ})) = (๐‘† โ€œ (๐น โ€œ (๐ฝ โˆ– {๐‘ฅ})))
417adantr 480 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ฝ) โ†’ ๐น:๐ฝโ€“1-1-ontoโ†’๐ผ)
42 dff1o3 6832 . . . . . . . . . . . . 13 (๐น:๐ฝโ€“1-1-ontoโ†’๐ผ โ†” (๐น:๐ฝโ€“ontoโ†’๐ผ โˆง Fun โ—ก๐น))
4342simprbi 496 . . . . . . . . . . . 12 (๐น:๐ฝโ€“1-1-ontoโ†’๐ผ โ†’ Fun โ—ก๐น)
44 imadif 6625 . . . . . . . . . . . 12 (Fun โ—ก๐น โ†’ (๐น โ€œ (๐ฝ โˆ– {๐‘ฅ})) = ((๐น โ€œ ๐ฝ) โˆ– (๐น โ€œ {๐‘ฅ})))
4541, 43, 443syl 18 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ฝ) โ†’ (๐น โ€œ (๐ฝ โˆ– {๐‘ฅ})) = ((๐น โ€œ ๐ฝ) โˆ– (๐น โ€œ {๐‘ฅ})))
46 f1ofo 6833 . . . . . . . . . . . . 13 (๐น:๐ฝโ€“1-1-ontoโ†’๐ผ โ†’ ๐น:๐ฝโ€“ontoโ†’๐ผ)
47 foima 6803 . . . . . . . . . . . . 13 (๐น:๐ฝโ€“ontoโ†’๐ผ โ†’ (๐น โ€œ ๐ฝ) = ๐ผ)
4841, 46, 473syl 18 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ฝ) โ†’ (๐น โ€œ ๐ฝ) = ๐ผ)
49 f1ofn 6827 . . . . . . . . . . . . . . 15 (๐น:๐ฝโ€“1-1-ontoโ†’๐ผ โ†’ ๐น Fn ๐ฝ)
507, 49syl 17 . . . . . . . . . . . . . 14 (๐œ‘ โ†’ ๐น Fn ๐ฝ)
51 fnsnfv 6963 . . . . . . . . . . . . . 14 ((๐น Fn ๐ฝ โˆง ๐‘ฅ โˆˆ ๐ฝ) โ†’ {(๐นโ€˜๐‘ฅ)} = (๐น โ€œ {๐‘ฅ}))
5250, 51sylan 579 . . . . . . . . . . . . 13 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ฝ) โ†’ {(๐นโ€˜๐‘ฅ)} = (๐น โ€œ {๐‘ฅ}))
5352eqcomd 2732 . . . . . . . . . . . 12 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ฝ) โ†’ (๐น โ€œ {๐‘ฅ}) = {(๐นโ€˜๐‘ฅ)})
5448, 53difeq12d 4118 . . . . . . . . . . 11 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ฝ) โ†’ ((๐น โ€œ ๐ฝ) โˆ– (๐น โ€œ {๐‘ฅ})) = (๐ผ โˆ– {(๐นโ€˜๐‘ฅ)}))
5545, 54eqtrd 2766 . . . . . . . . . 10 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ฝ) โ†’ (๐น โ€œ (๐ฝ โˆ– {๐‘ฅ})) = (๐ผ โˆ– {(๐นโ€˜๐‘ฅ)}))
5655imaeq2d 6052 . . . . . . . . 9 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ฝ) โ†’ (๐‘† โ€œ (๐น โ€œ (๐ฝ โˆ– {๐‘ฅ}))) = (๐‘† โ€œ (๐ผ โˆ– {(๐นโ€˜๐‘ฅ)})))
5740, 56eqtrid 2778 . . . . . . . 8 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ฝ) โ†’ ((๐‘† โˆ˜ ๐น) โ€œ (๐ฝ โˆ– {๐‘ฅ})) = (๐‘† โ€œ (๐ผ โˆ– {(๐นโ€˜๐‘ฅ)})))
5857unieqd 4915 . . . . . . 7 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ฝ) โ†’ โˆช ((๐‘† โˆ˜ ๐น) โ€œ (๐ฝ โˆ– {๐‘ฅ})) = โˆช (๐‘† โ€œ (๐ผ โˆ– {(๐นโ€˜๐‘ฅ)})))
5958fveq2d 6888 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ฝ) โ†’ ((mrClsโ€˜(SubGrpโ€˜๐บ))โ€˜โˆช ((๐‘† โˆ˜ ๐น) โ€œ (๐ฝ โˆ– {๐‘ฅ}))) = ((mrClsโ€˜(SubGrpโ€˜๐บ))โ€˜โˆช (๐‘† โ€œ (๐ผ โˆ– {(๐นโ€˜๐‘ฅ)}))))
6039, 59ineq12d 4208 . . . . 5 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ฝ) โ†’ (((๐‘† โˆ˜ ๐น)โ€˜๐‘ฅ) โˆฉ ((mrClsโ€˜(SubGrpโ€˜๐บ))โ€˜โˆช ((๐‘† โˆ˜ ๐น) โ€œ (๐ฝ โˆ– {๐‘ฅ})))) = ((๐‘†โ€˜(๐นโ€˜๐‘ฅ)) โˆฉ ((mrClsโ€˜(SubGrpโ€˜๐บ))โ€˜โˆช (๐‘† โ€œ (๐ผ โˆ– {(๐นโ€˜๐‘ฅ)})))))
614adantr 480 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ฝ) โ†’ ๐บdom DProd ๐‘†)
6210adantr 480 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ฝ) โ†’ dom ๐‘† = ๐ผ)
6316ffvelcdmda 7079 . . . . . 6 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ฝ) โ†’ (๐นโ€˜๐‘ฅ) โˆˆ ๐ผ)
6461, 62, 63, 2, 3dprddisj 19928 . . . . 5 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ฝ) โ†’ ((๐‘†โ€˜(๐นโ€˜๐‘ฅ)) โˆฉ ((mrClsโ€˜(SubGrpโ€˜๐บ))โ€˜โˆช (๐‘† โ€œ (๐ผ โˆ– {(๐นโ€˜๐‘ฅ)})))) = {(0gโ€˜๐บ)})
6560, 64eqtrd 2766 . . . 4 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ฝ) โ†’ (((๐‘† โˆ˜ ๐น)โ€˜๐‘ฅ) โˆฉ ((mrClsโ€˜(SubGrpโ€˜๐บ))โ€˜โˆช ((๐‘† โˆ˜ ๐น) โ€œ (๐ฝ โˆ– {๐‘ฅ})))) = {(0gโ€˜๐บ)})
66 eqimss 4035 . . . 4 ((((๐‘† โˆ˜ ๐น)โ€˜๐‘ฅ) โˆฉ ((mrClsโ€˜(SubGrpโ€˜๐บ))โ€˜โˆช ((๐‘† โˆ˜ ๐น) โ€œ (๐ฝ โˆ– {๐‘ฅ})))) = {(0gโ€˜๐บ)} โ†’ (((๐‘† โˆ˜ ๐น)โ€˜๐‘ฅ) โˆฉ ((mrClsโ€˜(SubGrpโ€˜๐บ))โ€˜โˆช ((๐‘† โˆ˜ ๐น) โ€œ (๐ฝ โˆ– {๐‘ฅ})))) โІ {(0gโ€˜๐บ)})
6765, 66syl 17 . . 3 ((๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ฝ) โ†’ (((๐‘† โˆ˜ ๐น)โ€˜๐‘ฅ) โˆฉ ((mrClsโ€˜(SubGrpโ€˜๐บ))โ€˜โˆช ((๐‘† โˆ˜ ๐น) โ€œ (๐ฝ โˆ– {๐‘ฅ})))) โІ {(0gโ€˜๐บ)})
681, 2, 3, 6, 13, 18, 38, 67dmdprdd 19918 . 2 (๐œ‘ โ†’ ๐บdom DProd (๐‘† โˆ˜ ๐น))
69 rnco2 6245 . . . . . 6 ran (๐‘† โˆ˜ ๐น) = (๐‘† โ€œ ran ๐น)
70 forn 6801 . . . . . . . . 9 (๐น:๐ฝโ€“ontoโ†’๐ผ โ†’ ran ๐น = ๐ผ)
717, 46, 703syl 18 . . . . . . . 8 (๐œ‘ โ†’ ran ๐น = ๐ผ)
7271imaeq2d 6052 . . . . . . 7 (๐œ‘ โ†’ (๐‘† โ€œ ran ๐น) = (๐‘† โ€œ ๐ผ))
73 ffn 6710 . . . . . . . 8 (๐‘†:๐ผโŸถ(SubGrpโ€˜๐บ) โ†’ ๐‘† Fn ๐ผ)
74 fnima 6673 . . . . . . . 8 (๐‘† Fn ๐ผ โ†’ (๐‘† โ€œ ๐ผ) = ran ๐‘†)
7514, 73, 743syl 18 . . . . . . 7 (๐œ‘ โ†’ (๐‘† โ€œ ๐ผ) = ran ๐‘†)
7672, 75eqtrd 2766 . . . . . 6 (๐œ‘ โ†’ (๐‘† โ€œ ran ๐น) = ran ๐‘†)
7769, 76eqtrid 2778 . . . . 5 (๐œ‘ โ†’ ran (๐‘† โˆ˜ ๐น) = ran ๐‘†)
7877unieqd 4915 . . . 4 (๐œ‘ โ†’ โˆช ran (๐‘† โˆ˜ ๐น) = โˆช ran ๐‘†)
7978fveq2d 6888 . . 3 (๐œ‘ โ†’ ((mrClsโ€˜(SubGrpโ€˜๐บ))โ€˜โˆช ran (๐‘† โˆ˜ ๐น)) = ((mrClsโ€˜(SubGrpโ€˜๐บ))โ€˜โˆช ran ๐‘†))
803dprdspan 19946 . . . 4 (๐บdom DProd (๐‘† โˆ˜ ๐น) โ†’ (๐บ DProd (๐‘† โˆ˜ ๐น)) = ((mrClsโ€˜(SubGrpโ€˜๐บ))โ€˜โˆช ran (๐‘† โˆ˜ ๐น)))
8168, 80syl 17 . . 3 (๐œ‘ โ†’ (๐บ DProd (๐‘† โˆ˜ ๐น)) = ((mrClsโ€˜(SubGrpโ€˜๐บ))โ€˜โˆช ran (๐‘† โˆ˜ ๐น)))
823dprdspan 19946 . . . 4 (๐บdom DProd ๐‘† โ†’ (๐บ DProd ๐‘†) = ((mrClsโ€˜(SubGrpโ€˜๐บ))โ€˜โˆช ran ๐‘†))
834, 82syl 17 . . 3 (๐œ‘ โ†’ (๐บ DProd ๐‘†) = ((mrClsโ€˜(SubGrpโ€˜๐บ))โ€˜โˆช ran ๐‘†))
8479, 81, 833eqtr4d 2776 . 2 (๐œ‘ โ†’ (๐บ DProd (๐‘† โˆ˜ ๐น)) = (๐บ DProd ๐‘†))
8568, 84jca 511 1 (๐œ‘ โ†’ (๐บdom DProd (๐‘† โˆ˜ ๐น) โˆง (๐บ DProd (๐‘† โˆ˜ ๐น)) = (๐บ DProd ๐‘†)))
Colors of variables: wff setvar class
Syntax hints:   โ†’ wi 4   โ†” wb 205   โˆง wa 395   โˆง w3a 1084   = wceq 1533   โˆˆ wcel 2098   โ‰  wne 2934  Vcvv 3468   โˆ– cdif 3940   โˆฉ cin 3942   โІ wss 3943  {csn 4623  โˆช cuni 4902   class class class wbr 5141  โ—กccnv 5668  dom cdm 5669  ran crn 5670   โ€œ cima 5672   โˆ˜ ccom 5673  Fun wfun 6530   Fn wfn 6531  โŸถwf 6532  โ€“1-1โ†’wf1 6533  โ€“ontoโ†’wfo 6534  โ€“1-1-ontoโ†’wf1o 6535  โ€˜cfv 6536  (class class class)co 7404  0gc0g 17391  mrClscmrc 17533  Grpcgrp 18860  SubGrpcsubg 19044  Cntzccntz 19228   DProd cdprd 19912
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7721  ax-cnex 11165  ax-resscn 11166  ax-1cn 11167  ax-icn 11168  ax-addcl 11169  ax-addrcl 11170  ax-mulcl 11171  ax-mulrcl 11172  ax-mulcom 11173  ax-addass 11174  ax-mulass 11175  ax-distr 11176  ax-i2m1 11177  ax-1ne0 11178  ax-1rid 11179  ax-rnegex 11180  ax-rrecex 11181  ax-cnre 11182  ax-pre-lttri 11183  ax-pre-lttrn 11184  ax-pre-ltadd 11185  ax-pre-mulgt0 11186
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-nel 3041  df-ral 3056  df-rex 3065  df-rmo 3370  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-int 4944  df-iun 4992  df-iin 4993  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-se 5625  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6293  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6488  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-isom 6545  df-riota 7360  df-ov 7407  df-oprab 7408  df-mpo 7409  df-of 7666  df-om 7852  df-1st 7971  df-2nd 7972  df-supp 8144  df-tpos 8209  df-frecs 8264  df-wrecs 8295  df-recs 8369  df-rdg 8408  df-1o 8464  df-er 8702  df-map 8821  df-ixp 8891  df-en 8939  df-dom 8940  df-sdom 8941  df-fin 8942  df-fsupp 9361  df-oi 9504  df-card 9933  df-pnf 11251  df-mnf 11252  df-xr 11253  df-ltxr 11254  df-le 11255  df-sub 11447  df-neg 11448  df-nn 12214  df-2 12276  df-n0 12474  df-z 12560  df-uz 12824  df-fz 13488  df-fzo 13631  df-seq 13970  df-hash 14293  df-sets 17103  df-slot 17121  df-ndx 17133  df-base 17151  df-ress 17180  df-plusg 17216  df-0g 17393  df-gsum 17394  df-mre 17536  df-mrc 17537  df-acs 17539  df-mgm 18570  df-sgrp 18649  df-mnd 18665  df-mhm 18710  df-submnd 18711  df-grp 18863  df-minusg 18864  df-sbg 18865  df-mulg 18993  df-subg 19047  df-ghm 19136  df-gim 19181  df-cntz 19230  df-oppg 19259  df-cmn 19699  df-dprd 19914
This theorem is referenced by:  dprdf1  19952  ablfaclem2  20005
  Copyright terms: Public domain W3C validator