Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > dprdf2 | Structured version Visualization version GIF version |
Description: The function 𝑆 is a family of subgroups. (Contributed by Mario Carneiro, 25-Apr-2016.) |
Ref | Expression |
---|---|
dprdcntz.1 | ⊢ (𝜑 → 𝐺dom DProd 𝑆) |
dprdcntz.2 | ⊢ (𝜑 → dom 𝑆 = 𝐼) |
Ref | Expression |
---|---|
dprdf2 | ⊢ (𝜑 → 𝑆:𝐼⟶(SubGrp‘𝐺)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dprdcntz.1 | . . 3 ⊢ (𝜑 → 𝐺dom DProd 𝑆) | |
2 | dprdf 19111 | . . 3 ⊢ (𝐺dom DProd 𝑆 → 𝑆:dom 𝑆⟶(SubGrp‘𝐺)) | |
3 | 1, 2 | syl 17 | . 2 ⊢ (𝜑 → 𝑆:dom 𝑆⟶(SubGrp‘𝐺)) |
4 | dprdcntz.2 | . . 3 ⊢ (𝜑 → dom 𝑆 = 𝐼) | |
5 | 4 | feq2d 6486 | . 2 ⊢ (𝜑 → (𝑆:dom 𝑆⟶(SubGrp‘𝐺) ↔ 𝑆:𝐼⟶(SubGrp‘𝐺))) |
6 | 3, 5 | mpbid 234 | 1 ⊢ (𝜑 → 𝑆:𝐼⟶(SubGrp‘𝐺)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1537 class class class wbr 5052 dom cdm 5541 ⟶wf 6337 ‘cfv 6341 SubGrpcsubg 18256 DProd cdprd 19098 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-rep 5176 ax-sep 5189 ax-nul 5196 ax-pow 5252 ax-pr 5316 ax-un 7447 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-ral 3143 df-rex 3144 df-reu 3145 df-rab 3147 df-v 3488 df-sbc 3764 df-csb 3872 df-dif 3927 df-un 3929 df-in 3931 df-ss 3940 df-nul 4280 df-if 4454 df-pw 4527 df-sn 4554 df-pr 4556 df-op 4560 df-uni 4825 df-iun 4907 df-br 5053 df-opab 5115 df-mpt 5133 df-id 5446 df-xp 5547 df-rel 5548 df-cnv 5549 df-co 5550 df-dm 5551 df-rn 5552 df-res 5553 df-ima 5554 df-iota 6300 df-fun 6343 df-fn 6344 df-f 6345 df-f1 6346 df-fo 6347 df-f1o 6348 df-fv 6349 df-oprab 7146 df-mpo 7147 df-1st 7675 df-2nd 7676 df-ixp 8448 df-dprd 19100 |
This theorem is referenced by: dprdff 19117 dprdfid 19122 dprdfinv 19124 dprdfadd 19125 dprdfeq0 19127 dprdres 19133 dprdss 19134 dprdf1o 19137 dprdf1 19138 subgdprd 19140 dmdprdsplitlem 19142 dprdcntz2 19143 dpjlem 19156 dpjcntz 19157 dpjdisj 19158 dpjlsm 19159 dpjf 19162 dpjidcl 19163 dpjlid 19166 dpjghm 19168 dpjghm2 19169 ablfac1c 19176 ablfac1eulem 19177 ablfac1eu 19178 ablfaclem2 19191 ablfaclem3 19192 dchrptlem3 25828 |
Copyright terms: Public domain | W3C validator |