Theorem on1el4 10205

Description: The only unital ring with one element is the zero ring. (Contributed by FL, 14-Feb-2010.)

Hypotheses

Ref	Expression
on1el3.1	|- G = (1st` R)
on1el3.2	|- X = ran G

Assertion

Ref	Expression
on1el4	|- ((R e. Ring /\ A e. X) -> (X ~~ 1o <-> R = <.{<.<.A, A>., A>.}, {<.<.A, A>., A>.}>.))

Proof of Theorem on1el4

Step	Hyp	Ref	Expression
1		opeq12 2982	. . . . . . . . . 10 |- ((x = A /\ x = A) -> <.x, x>. = <.A, A>.)
2	1	anidms 478	. . . . . . . . 9 |- (x = A -> <.x, x>. = <.A, A>.)
3		opeq12 2982	. . . . . . . . 9 |- ((<.x, x>. = <.A, A>. /\ x = A) -> <.<.x, x>., x>. = <.<.A, A>., A>.)
4	2, 3	mpancom 766	. . . . . . . 8 |- (x = A -> <.<.x, x>., x>. = <.<.A, A>., A>.)
5	4	sneqd 2880	. . . . . . 7 |- (x = A -> {<.<.x, x>., x>.} = {<.<.A, A>., A>.})
6	5, 5	opeq12d 2988	. . . . . 6 |- (x = A -> <.{<.<.x, x>., x>.}, {<.<.x, x>., x>.}>. = <.{<.<.A, A>., A>.}, {<.<.A, A>., A>.}>.)
7	6	eqeq2d 1732	. . . . 5 |- (x = A -> (R = <.{<.<.x, x>., x>.}, {<.<.x, x>., x>.}>. <-> R = <.{<.<.A, A>., A>.}, {<.<.A, A>., A>.}>.))
8	7	bibi2d 677	. . . 4 |- (x = A -> ((X ~~ 1o <-> R = <.{<.<.x, x>., x>.}, {<.<.x, x>., x>.}>.) <-> (X ~~ 1o <-> R = <.{<.<.A, A>., A>.}, {<.<.A, A>., A>.}>.)))
9	8	imbi2d 671	. . 3 |- (x = A -> ((R e. Ring -> (X ~~ 1o <-> R = <.{<.<.x, x>., x>.}, {<.<.x, x>., x>.}>.)) <-> (R e. Ring -> (X ~~ 1o <-> R = <.{<.<.A, A>., A>.}, {<.<.A, A>., A>.}>.))))
10		setwoe 9964	. . . . . . . . . 10 |- ((x e. X /\ X ~~ 1o) -> X = {x})
11		on1el3.1	. . . . . . . . . . . . . 14 |- G = (1st` R)
12		on1el3.2	. . . . . . . . . . . . . 14 |- X = ran G
13	11, 12	on1el3 10204	. . . . . . . . . . . . 13 |- ((R e. Ring /\ x e. X) -> (X = {x} <-> R = <.{<.<.x, x>., x>.}, {<.<.x, x>., x>.}>.))
14	13	biimpd 169	. . . . . . . . . . . 12 |- ((R e. Ring /\ x e. X) -> (X = {x} -> R = <.{<.<.x, x>., x>.}, {<.<.x, x>., x>.}>.))
15	14	ex 400	. . . . . . . . . . 11 |- (R e. Ring -> (x e. X -> (X = {x} -> R = <.{<.<.x, x>., x>.}, {<.<.x, x>., x>.}>.)))
16	15	com13 37	. . . . . . . . . 10 |- (X = {x} -> (x e. X -> (R e. Ring -> R = <.{<.<.x, x>., x>.}, {<.<.x, x>., x>.}>.)))
17	10, 16	syl 12	. . . . . . . . 9 |- ((x e. X /\ X ~~ 1o) -> (x e. X -> (R e. Ring -> R = <.{<.<.x, x>., x>.}, {<.<.x, x>., x>.}>.)))
18	17	ex 400	. . . . . . . 8 |- (x e. X -> (X ~~ 1o -> (x e. X -> (R e. Ring -> R = <.{<.<.x, x>., x>.}, {<.<.x, x>., x>.}>.))))
19	18	pm2.43a 80	. . . . . . 7 |- (x e. X -> (X ~~ 1o -> (R e. Ring -> R = <.{<.<.x, x>., x>.}, {<.<.x, x>., x>.}>.)))
20	19	com23 36	. . . . . 6 |- (x e. X -> (R e. Ring -> (X ~~ 1o -> R = <.{<.<.x, x>., x>.}, {<.<.x, x>., x>.}>.)))
21	20	imp 375	. . . . 5 |- ((x e. X /\ R e. Ring) -> (X ~~ 1o -> R = <.{<.<.x, x>., x>.}, {<.<.x, x>., x>.}>.))
22		fveq2 4492	. . . . . . . 8 |- (R = <.{<.<.x, x>., x>.}, {<.<.x, x>., x>.}>. -> (1st` R) = (1st` <.{<.<.x, x>., x>.}, {<.<.x, x>., x>.}>.))
23		snex 3307	. . . . . . . . . 10 |- {<.<.x, x>., x>.} e. _V
24	23	op1st 4837	. . . . . . . . 9 |- (1st` <.{<.<.x, x>., x>.}, {<.<.x, x>., x>.}>.) = {<.<.x, x>., x>.}
25		eqtr 1741	. . . . . . . . . 10 |- (((1st` R) = (1st` <.{<.<.x, x>., x>.}, {<.<.x, x>., x>.}>.) /\ (1st` <.{<.<.x, x>., x>.}, {<.<.x, x>., x>.}>.) = {<.<.x, x>., x>.}) -> (1st` R) = {<.<.x, x>., x>.})
26		rneq 3997	. . . . . . . . . . 11 |- ((1st` R) = {<.<.x, x>., x>.} -> ran (1st` R) = ran {<.<.x, x>., x>.})
27		eqtr 1741	. . . . . . . . . . . . . 14 |- ((X = ran G /\ ran G = ran (1st` R)) -> X = ran (1st` R))
28		eqtr 1741	. . . . . . . . . . . . . . . 16 |- ((X = ran (1st` R) /\ ran (1st` R) = ran {<.<.x, x>., x>.}) -> X = ran {<.<.x, x>., x>.})
29		opex 3342	. . . . . . . . . . . . . . . . . 18 |- <.x, x>. e. _V
30		visset 2128	. . . . . . . . . . . . . . . . . 18 |- x e. _V
31	29, 30	rnsnop 4186	. . . . . . . . . . . . . . . . 17 |- ran {<.<.x, x>., x>.} = {x}
32		eqtr 1741	. . . . . . . . . . . . . . . . . 18 |- ((X = ran {<.<.x, x>., x>.} /\ ran {<.<.x, x>., x>.} = {x}) -> X = {x})
33	30	ensn1 5294	. . . . . . . . . . . . . . . . . . . 20 |- {x} ~~ 1o
34		breq1 3161	. . . . . . . . . . . . . . . . . . . 20 |- (X = {x} -> (X ~~ 1o <-> {x} ~~ 1o))
35	33, 34	mpbiri 210	. . . . . . . . . . . . . . . . . . 19 |- (X = {x} -> X ~~ 1o)
36	35	a1d 15	. . . . . . . . . . . . . . . . . 18 |- (X = {x} -> (x e. X -> X ~~ 1o))
37	32, 36	syl 12	. . . . . . . . . . . . . . . . 17 |- ((X = ran {<.<.x, x>., x>.} /\ ran {<.<.x, x>., x>.} = {x}) -> (x e. X -> X ~~ 1o))
38	31, 37	mpan2 757	. . . . . . . . . . . . . . . 16 |- (X = ran {<.<.x, x>., x>.} -> (x e. X -> X ~~ 1o))
39	28, 38	syl 12	. . . . . . . . . . . . . . 15 |- ((X = ran (1st` R) /\ ran (1st` R) = ran {<.<.x, x>., x>.}) -> (x e. X -> X ~~ 1o))
40	39	ex 400	. . . . . . . . . . . . . 14 |- (X = ran (1st` R) -> (ran (1st` R) = ran {<.<.x, x>., x>.} -> (x e. X -> X ~~ 1o)))
41	27, 40	syl 12	. . . . . . . . . . . . 13 |- ((X = ran G /\ ran G = ran (1st` R)) -> (ran (1st` R) = ran {<.<.x, x>., x>.} -> (x e. X -> X ~~ 1o)))
42		rneq 3997	. . . . . . . . . . . . 13 |- (G = (1st` R) -> ran G = ran (1st` R))
43	41, 12, 42	sylancr 523	. . . . . . . . . . . 12 |- (G = (1st` R) -> (ran (1st` R) = ran {<.<.x, x>., x>.} -> (x e. X -> X ~~ 1o)))
44	11, 43	ax-mp 7	. . . . . . . . . . 11 |- (ran (1st` R) = ran {<.<.x, x>., x>.} -> (x e. X -> X ~~ 1o))
45	26, 44	syl 12	. . . . . . . . . 10 |- ((1st` R) = {<.<.x, x>., x>.} -> (x e. X -> X ~~ 1o))
46	25, 45	syl 12	. . . . . . . . 9 |- (((1st` R) = (1st` <.{<.<.x, x>., x>.}, {<.<.x, x>., x>.}>.) /\ (1st` <.{<.<.x, x>., x>.}, {<.<.x, x>., x>.}>.) = {<.<.x, x>., x>.}) -> (x e. X -> X ~~ 1o))
47	24, 46	mpan2 757	. . . . . . . 8 |- ((1st` R) = (1st` <.{<.<.x, x>., x>.}, {<.<.x, x>., x>.}>.) -> (x e. X -> X ~~ 1o))
48	22, 47	syl 12	. . . . . . 7 |- (R = <.{<.<.x, x>., x>.}, {<.<.x, x>., x>.}>. -> (x e. X -> X ~~ 1o))
49	48	com12 14	. . . . . 6 |- (x e. X -> (R = <.{<.<.x, x>., x>.}, {<.<.x, x>., x>.}>. -> X ~~ 1o))
50	49	adantr 423	. . . . 5 |- ((x e. X /\ R e. Ring) -> (R = <.{<.<.x, x>., x>.}, {<.<.x, x>., x>.}>. -> X ~~ 1o))
51	21, 50	impbid 571	. . . 4 |- ((x e. X /\ R e. Ring) -> (X ~~ 1o <-> R = <.{<.<.x, x>., x>.}, {<.<.x, x>., x>.}>.))
52	51	ex 400	. . 3 |- (x e. X -> (R e. Ring -> (X ~~ 1o <-> R = <.{<.<.x, x>., x>.}, {<.<.x, x>., x>.}>.)))
53	9, 52	vtoclga 2185	. 2 |- (A e. X -> (R e. Ring -> (X ~~ 1o <-> R = <.{<.<.A, A>., A>.}, {<.<.A, A>., A>.}>.)))
54	53	impcom 376	1 |- ((R e. Ring /\ A e. X) -> (X ~~ 1o <-> R = <.{<.<.A, A>., A>.}, {<.<.A, A>., A>.}>.))

Syntax hints:   -> wi 3   <-> wb 162   /\ wa 239   = wceq 1136   e. wcel 1138  {csn 2868  <.cop 2870   class class class wbr 3158  ran crn 3798  ` cfv 3809  1stc1st 4829  1oc1o 4983   ~~ cen 5234  Ringcring 9258

This theorem is referenced by:  on1el6 10206

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-rep 3243  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-3or 856  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-pss 2440  df-nul 2702  df-if 2807  df-pw 2859  df-sn 2873  df-pr 2874  df-tp 2876  df-op 2877  df-uni 3000  df-br 3159  df-opab 3214  df-tr 3230  df-eprel 3398  df-id 3401  df-po 3406  df-so 3419  df-fr 3440  df-we 3459  df-ord 3475  df-on 3476  df-lim 3477  df-suc 3478  df-om 3761  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-f1 3822  df-fo 3823  df-f1o 3824  df-fv 3825  df-opr 4697  df-1st 4831  df-2nd 4832  df-1o 4988  df-er 5129  df-en 5238  df-dom 5239  df-sdom 5240  df-fin 5241  df-grp 9111  df-abl 9203  df-ring 9259

Copyright terms: Public domain