Description: According to df-subc , the subcategories ( SubcatC ) of a category C are subsets of the homomorphisms of C (see subcssc and subcss2 ). Therefore, the set of field homomorphisms is a "subcategory" of the category of division rings. (Contributed by AV, 20-Feb-2020) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | drhmsubcALTV.c | |
|
drhmsubcALTV.j | |
||
fldhmsubcALTV.d | |
||
fldhmsubcALTV.f | |
||
Assertion | fldhmsubcALTV | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | drhmsubcALTV.c | |
|
2 | drhmsubcALTV.j | |
|
3 | fldhmsubcALTV.d | |
|
4 | fldhmsubcALTV.f | |
|
5 | elin | |
|
6 | 5 | simprbi | |
7 | crngring | |
|
8 | 6 7 | syl | |
9 | df-field | |
|
10 | 8 9 | eleq2s | |
11 | 10 | rgen | |
12 | 11 3 4 | srhmsubcALTV | |
13 | inss1 | |
|
14 | 9 13 | eqsstri | |
15 | sslin | |
|
16 | 14 15 | ax-mp | |
17 | 16 | a1i | |
18 | 3 1 | sseq12i | |
19 | 17 18 | sylibr | |
20 | ssidd | |
|
21 | 4 | a1i | |
22 | oveq12 | |
|
23 | 22 | adantl | |
24 | simprl | |
|
25 | simpr | |
|
26 | 25 | adantl | |
27 | ovexd | |
|
28 | 21 23 24 26 27 | ovmpod | |
29 | 2 | a1i | |
30 | 16 18 | mpbir | |
31 | 30 | sseli | |
32 | 31 | ad2antrl | |
33 | 30 | sseli | |
34 | 33 | adantl | |
35 | 34 | adantl | |
36 | 29 23 32 35 27 | ovmpod | |
37 | 20 28 36 | 3sstr4d | |
38 | 37 | ralrimivva | |
39 | ovex | |
|
40 | 4 39 | fnmpoi | |
41 | 40 | a1i | |
42 | 2 39 | fnmpoi | |
43 | 42 | a1i | |
44 | inex1g | |
|
45 | 1 44 | eqeltrid | |
46 | 41 43 45 | isssc | |
47 | 19 38 46 | mpbir2and | |
48 | 1 2 | drhmsubcALTV | |
49 | eqid | |
|
50 | 49 | subsubc | |
51 | 48 50 | syl | |
52 | 12 47 51 | mpbir2and | |