lidlunin0

Description: The union of a nonempty subset of ideals in a ring is nonempty. (Contributed by AV, 28-Jun-2026)

		Ref	Expression
	Assertion	lidlunin0	$⊢ (R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \to ⋃ C \neq \emptyset$

Proof

Step	Hyp	Ref	Expression
1		n0	$⊢ C \neq \emptyset \leftrightarrow \exists y y \in C$
2		simpl	$⊢ (R \in Ring \land C \subseteq LIdeal (R)) \to R \in Ring$
3		ssel	$⊢ C \subseteq LIdeal (R) \to (y \in C \to y \in LIdeal (R))$
4	3	adantl	$⊢ (R \in Ring \land C \subseteq LIdeal (R)) \to (y \in C \to y \in LIdeal (R))$
5	4	imp	$⊢ ((R \in Ring \land C \subseteq LIdeal (R)) \land y \in C) \to y \in LIdeal (R)$
6		eqid	$⊢ LIdeal (R) = LIdeal (R)$
7		eqid	$⊢ 0_{R} = 0_{R}$
8	6 7	lidl0cl	$⊢ (R \in Ring \land y \in LIdeal (R)) \to 0_{R} \in y$
9	2 5 8	syl2an2r	$⊢ ((R \in Ring \land C \subseteq LIdeal (R)) \land y \in C) \to 0_{R} \in y$
10		simpr	$⊢ ((R \in Ring \land C \subseteq LIdeal (R)) \land y \in C) \to y \in C$
11	9 10	jca	$⊢ ((R \in Ring \land C \subseteq LIdeal (R)) \land y \in C) \to (0_{R} \in y \land y \in C)$
12	11	ex	$⊢ (R \in Ring \land C \subseteq LIdeal (R)) \to (y \in C \to (0_{R} \in y \land y \in C))$
13	12	eximdv	$⊢ (R \in Ring \land C \subseteq LIdeal (R)) \to (\exists y y \in C \to \exists y (0_{R} \in y \land y \in C))$
14	1 13	biimtrid	$⊢ (R \in Ring \land C \subseteq LIdeal (R)) \to (C \neq \emptyset \to \exists y (0_{R} \in y \land y \in C))$
15	14	ex	$⊢ R \in Ring \to (C \subseteq LIdeal (R) \to (C \neq \emptyset \to \exists y (0_{R} \in y \land y \in C)))$
16	15	com23	$⊢ R \in Ring \to (C \neq \emptyset \to (C \subseteq LIdeal (R) \to \exists y (0_{R} \in y \land y \in C)))$
17	16	3imp	$⊢ (R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \to \exists y (0_{R} \in y \land y \in C)$
18		eluni	$⊢ 0_{R} \in ⋃ C \leftrightarrow \exists y (0_{R} \in y \land y \in C)$
19	17 18	sylibr	$⊢ (R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \to 0_{R} \in ⋃ C$
20	19	ne0d	$⊢ (R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \to ⋃ C \neq \emptyset$

Metamath Proof Explorer

Theorem lidlunin0

Proof