Theorem 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	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) → ∪ 𝐶 ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		n0	⊢ ( 𝐶 ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ 𝐶 )
2		simpl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) → 𝑅 ∈ Ring )
3		ssel	⊢ ( 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) → ( 𝑦 ∈ 𝐶 → 𝑦 ∈ ( LIdeal ‘ 𝑅 ) ) )
4	3	adantl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) → ( 𝑦 ∈ 𝐶 → 𝑦 ∈ ( LIdeal ‘ 𝑅 ) ) )
5	4	imp	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑦 ∈ 𝐶 ) → 𝑦 ∈ ( LIdeal ‘ 𝑅 ) )
6		eqid	⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
7		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
8	6 7	lidl0cl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑦 ∈ ( LIdeal ‘ 𝑅 ) ) → ( 0g ‘ 𝑅 ) ∈ 𝑦 )
9	2 5 8	syl2an2r	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑦 ∈ 𝐶 ) → ( 0g ‘ 𝑅 ) ∈ 𝑦 )
10		simpr	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑦 ∈ 𝐶 ) → 𝑦 ∈ 𝐶 )
11	9 10	jca	⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑦 ∈ 𝐶 ) → ( ( 0g ‘ 𝑅 ) ∈ 𝑦 ∧ 𝑦 ∈ 𝐶 ) )
12	11	ex	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) → ( 𝑦 ∈ 𝐶 → ( ( 0g ‘ 𝑅 ) ∈ 𝑦 ∧ 𝑦 ∈ 𝐶 ) ) )
13	12	eximdv	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) → ( ∃ 𝑦 𝑦 ∈ 𝐶 → ∃ 𝑦 ( ( 0g ‘ 𝑅 ) ∈ 𝑦 ∧ 𝑦 ∈ 𝐶 ) ) )
14	1 13	biimtrid	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) → ( 𝐶 ≠ ∅ → ∃ 𝑦 ( ( 0g ‘ 𝑅 ) ∈ 𝑦 ∧ 𝑦 ∈ 𝐶 ) ) )
15	14	ex	⊢ ( 𝑅 ∈ Ring → ( 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) → ( 𝐶 ≠ ∅ → ∃ 𝑦 ( ( 0g ‘ 𝑅 ) ∈ 𝑦 ∧ 𝑦 ∈ 𝐶 ) ) ) )
16	15	com23	⊢ ( 𝑅 ∈ Ring → ( 𝐶 ≠ ∅ → ( 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) → ∃ 𝑦 ( ( 0g ‘ 𝑅 ) ∈ 𝑦 ∧ 𝑦 ∈ 𝐶 ) ) ) )
17	16	3imp	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) → ∃ 𝑦 ( ( 0g ‘ 𝑅 ) ∈ 𝑦 ∧ 𝑦 ∈ 𝐶 ) )
18		eluni	⊢ ( ( 0g ‘ 𝑅 ) ∈ ∪ 𝐶 ↔ ∃ 𝑦 ( ( 0g ‘ 𝑅 ) ∈ 𝑦 ∧ 𝑦 ∈ 𝐶 ) )
19	17 18	sylibr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) → ( 0g ‘ 𝑅 ) ∈ ∪ 𝐶 )
20	19	ne0d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ ( LIdeal ‘ 𝑅 ) ) → ∪ 𝐶 ≠ ∅ )