Theorem ring1cl 10207

Description: The unit of a ring belongs to the base set. (Contributed by FL, 12-Feb-2010.)

Hypotheses

Ref	Expression
ring1cl.1	|- X = ran (1st` R)
ring1cl.2	|- H = (2nd` R)
ring1cl.3	|- U = (Id` H)

Assertion

Ref	Expression
ring1cl	|- (R e. Ring -> U e. X)

Proof of Theorem ring1cl

Step	Hyp	Ref	Expression
1		ring1cl.2	. . . . . 6 |- H = (2nd` R)
2	1	unmnd 10197	. . . . 5 |- (R e. Ring -> H e. Mnd)
3	1	eleq1i 1797	. . . . . 6 |- (H e. Mnd <-> (2nd` R) e. Mnd)
4		mndismgm 10180	. . . . . . 7 |- ((2nd` R) e. Mnd -> (2nd` R) e. Magma)
5		mndisexid 10179	. . . . . . 7 |- ((2nd` R) e. Mnd -> (2nd` R) e. ExId )
6	4, 5	jca 308	. . . . . 6 |- ((2nd` R) e. Mnd -> ((2nd` R) e. Magma /\ (2nd` R) e. ExId ))
7	3, 6	sylbi 215	. . . . 5 |- (H e. Mnd -> ((2nd` R) e. Magma /\ (2nd` R) e. ExId ))
8	2, 7	syl 12	. . . 4 |- (R e. Ring -> ((2nd` R) e. Magma /\ (2nd` R) e. ExId ))
9		elin 2613	. . . 4 |- ((2nd` R) e. (Magma i^i ExId ) <-> ((2nd` R) e. Magma /\ (2nd` R) e. ExId ))
10	8, 9	sylibr 216	. . 3 |- (R e. Ring -> (2nd` R) e. (Magma i^i ExId ))
11		eqid 1721	. . . 4 |- ran (2nd` R) = ran (2nd` R)
12		ring1cl.3	. . . . 5 |- U = (Id` H)
13	1	fveq2i 4495	. . . . 5 |- (Id` H) = (Id` (2nd` R))
14	12, 13	eqtri 1745	. . . 4 |- U = (Id` (2nd` R))
15	11, 14	iorlid 10167	. . 3 |- ((2nd` R) e. (Magma i^i ExId ) -> U e. ran (2nd` R))
16	10, 15	syl 12	. 2 |- (R e. Ring -> U e. ran (2nd` R))
17		eqtr 1741	. . . 4 |- ((X = ran (1st` R) /\ ran (1st` R) = ran (2nd` R)) -> X = ran (2nd` R))
18	17	eleq2d 1801	. . 3 |- ((X = ran (1st` R) /\ ran (1st` R) = ran (2nd` R)) -> (U e. X <-> U e. ran (2nd` R)))
19		ring1cl.1	. . 3 |- X = ran (1st` R)
20		eqid 1721	. . . 4 |- (2nd` R) = (2nd` R)
21		eqid 1721	. . . 4 |- (1st` R) = (1st` R)
22	20, 21	rnplrnml 10196	. . 3 |- (R e. Ring -> ran (1st` R) = ran (2nd` R))
23	18, 19, 22	sylancr 523	. 2 |- (R e. Ring -> (U e. X <-> U e. ran (2nd` R)))
24	16, 23	mpbird 212	1 |- (R e. Ring -> U e. X)

Syntax hints:   -> wi 3   <-> wb 162   /\ wa 239   = wceq 1136   e. wcel 1138   i^i cin 2425  ran crn 3798  ` cfv 3809  1stc1st 4829  2ndc2nd 4830  Idcgi 9107  Ringcring 9258   ExId cexid 10153  Magmacmagm 10157  Mndcmnd 10176

This theorem is referenced by:  uznzr 10208  ringnegmn1l 15784  ringnegmn1r 15785  ringneglmul 15786  ringnegrmul 15787  isdivrng2 15793  rnghomco 15810  rngisocnv 15817  idlnegcl 15852  1idl 15856  0ring 15857  smprngpr 15882  prnc 15897  isfldidl 15898  isdmn3 15904

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1142  ax-gen 1143  ax-8 1144  ax-9 1145  ax-10 1146  ax-11 1147  ax-12 1148  ax-13 1149  ax-14 1150  ax-17 1155  ax-4 1157  ax-5o 1159  ax-6o 1162  ax-9o 1319  ax-10o 1338  ax-16 1418  ax-11o 1426  ax-ext 1702  ax-sep 3253  ax-nul 3260  ax-pow 3296  ax-pr 3339  ax-un 3601

This theorem depends on definitions:  df-bi 163  df-or 240  df-an 241  df-3an 857  df-ex 1165  df-sb 1374  df-eu 1613  df-mo 1614  df-clab 1709  df-cleq 1714  df-clel 1717  df-ne 1856  df-ral 1943  df-rex 1944  df-reu 1945  df-rab 1946  df-v 2127  df-dif 2430  df-un 2433  df-in 2436  df-ss 2438  df-nul 2702  df-pw 2859  df-sn 2873  df-pr 2874  df-op 2877  df-uni 3000  df-br 3159  df-opab 3214  df-id 3401  df-xp 3811  df-rel 3812  df-cnv 3813  df-co 3814  df-dm 3815  df-rn 3816  df-res 3817  df-ima 3818  df-fun 3819  df-fn 3820  df-f 3821  df-fo 3823  df-fv 3825  df-opr 4697  df-1st 4831  df-2nd 4832  df-grp 9111  df-gid 9112  df-abl 9203  df-ring 9259  df-ass 10152  df-exid 10154  df-mgm 10158  df-sgr 10170  df-mnd 10177

Copyright terms: Public domain