Theorem mxidlnzrb

Description: A ring is nonzero if and only if it has maximal ideals. (Contributed by Thierry Arnoux, 10-Apr-2024)

	Ref	Expression
Assertion	mxidlnzrb	Could not format assertion : No typesetting found for |- ( R e. Ring -> ( R e. NzRing <-> E. m m e. ( MaxIdeal ` R ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		krull	Could not format ( R e. NzRing -> E. m m e. ( MaxIdeal ` R ) ) : No typesetting found for |- ( R e. NzRing -> E. m m e. ( MaxIdeal ` R ) ) with typecode |-
2	1	adantl	Could not format ( ( R e. Ring /\ R e. NzRing ) -> E. m m e. ( MaxIdeal ` R ) ) : No typesetting found for |- ( ( R e. Ring /\ R e. NzRing ) -> E. m m e. ( MaxIdeal ` R ) ) with typecode |-
3		19.42v	Could not format ( E. m ( R e. Ring /\ m e. ( MaxIdeal ` R ) ) <-> ( R e. Ring /\ E. m m e. ( MaxIdeal ` R ) ) ) : No typesetting found for |- ( E. m ( R e. Ring /\ m e. ( MaxIdeal ` R ) ) <-> ( R e. Ring /\ E. m m e. ( MaxIdeal ` R ) ) ) with typecode |-
4		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
5	4	mxidlnzr	Could not format ( ( R e. Ring /\ m e. ( MaxIdeal ` R ) ) -> R e. NzRing ) : No typesetting found for |- ( ( R e. Ring /\ m e. ( MaxIdeal ` R ) ) -> R e. NzRing ) with typecode |-
6	5	exlimiv	Could not format ( E. m ( R e. Ring /\ m e. ( MaxIdeal ` R ) ) -> R e. NzRing ) : No typesetting found for |- ( E. m ( R e. Ring /\ m e. ( MaxIdeal ` R ) ) -> R e. NzRing ) with typecode |-
7	3 6	sylbir	Could not format ( ( R e. Ring /\ E. m m e. ( MaxIdeal ` R ) ) -> R e. NzRing ) : No typesetting found for |- ( ( R e. Ring /\ E. m m e. ( MaxIdeal ` R ) ) -> R e. NzRing ) with typecode |-
8	2 7	impbida	Could not format ( R e. Ring -> ( R e. NzRing <-> E. m m e. ( MaxIdeal ` R ) ) ) : No typesetting found for |- ( R e. Ring -> ( R e. NzRing <-> E. m m e. ( MaxIdeal ` R ) ) ) with typecode |-