unichnlidl

Description: The union of a nonempty chain of ideals is an ideal. (Contributed by Jeff Madsen, 5-Jan-2011) (Revised by AV, 28-Jun-2026)

		Ref	Expression
	Assertion	unichnlidl	$⊢ (R \in Ring \land (C \neq \emptyset \land C \subseteq LIdeal (R) \land \forall i \in C \forall j \in C (i \subseteq j \lor j \subseteq i))) \to ⋃ C \in LIdeal (R)$

Proof

Step	Hyp	Ref	Expression
1		dfss3	$⊢ C \subseteq LIdeal (R) \leftrightarrow \forall i \in C i \in LIdeal (R)$
2		eqid	$⊢ {Base}_{R} = {Base}_{R}$
3		eqid	$⊢ LIdeal (R) = LIdeal (R)$
4	2 3	lidlss	$⊢ i \in LIdeal (R) \to i \subseteq {Base}_{R}$
5	4	a1i	$⊢ R \in Ring \to (i \in LIdeal (R) \to i \subseteq {Base}_{R})$
6	5	ralimdv	$⊢ R \in Ring \to (\forall i \in C i \in LIdeal (R) \to \forall i \in C i \subseteq {Base}_{R})$
7	6	imp	$⊢ (R \in Ring \land \forall i \in C i \in LIdeal (R)) \to \forall i \in C i \subseteq {Base}_{R}$
8	1 7	sylan2b	$⊢ (R \in Ring \land C \subseteq LIdeal (R)) \to \forall i \in C i \subseteq {Base}_{R}$
9		unissb	$⊢ ⋃ C \subseteq {Base}_{R} \leftrightarrow \forall i \in C i \subseteq {Base}_{R}$
10	8 9	sylibr	$⊢ (R \in Ring \land C \subseteq LIdeal (R)) \to ⋃ C \subseteq {Base}_{R}$
11	10	3ad2antr2	$⊢ (R \in Ring \land (C \neq \emptyset \land C \subseteq LIdeal (R) \land \forall i \in C \forall j \in C (i \subseteq j \lor j \subseteq i))) \to ⋃ C \subseteq {Base}_{R}$
12		lidlunin0	$⊢ (R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \to ⋃ C \neq \emptyset$
13	12	3adant3r3	$⊢ (R \in Ring \land (C \neq \emptyset \land C \subseteq LIdeal (R) \land \forall i \in C \forall j \in C (i \subseteq j \lor j \subseteq i))) \to ⋃ C \neq \emptyset$
14		eluni2	$⊢ x \in ⋃ C \leftrightarrow \exists k \in C x \in k$
15		eluni2	$⊢ y \in ⋃ C \leftrightarrow \exists l \in C y \in l$
16		simpl	$⊢ (k \in C \land x \in k) \to k \in C$
17		simpl	$⊢ (l \in C \land y \in l) \to l \in C$
18	16 17	anim12i	$⊢ ((k \in C \land x \in k) \land (l \in C \land y \in l)) \to (k \in C \land l \in C)$
19	18	3adant1	$⊢ (b \in {Base}_{R} \land (k \in C \land x \in k) \land (l \in C \land y \in l)) \to (k \in C \land l \in C)$
20	19	adantl	$⊢ ((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land (b \in {Base}_{R} \land (k \in C \land x \in k) \land (l \in C \land y \in l))) \to (k \in C \land l \in C)$
21		sseq1	$⊢ i = k \to (i \subseteq j \leftrightarrow k \subseteq j)$
22		sseq2	$⊢ i = k \to (j \subseteq i \leftrightarrow j \subseteq k)$
23	21 22	orbi12d	$⊢ i = k \to ((i \subseteq j \lor j \subseteq i) \leftrightarrow (k \subseteq j \lor j \subseteq k))$
24		sseq2	$⊢ j = l \to (k \subseteq j \leftrightarrow k \subseteq l)$
25		sseq1	$⊢ j = l \to (j \subseteq k \leftrightarrow l \subseteq k)$
26	24 25	orbi12d	$⊢ j = l \to ((k \subseteq j \lor j \subseteq k) \leftrightarrow (k \subseteq l \lor l \subseteq k))$
27	23 26	rspc2v	$⊢ (k \in C \land l \in C) \to (\forall i \in C \forall j \in C (i \subseteq j \lor j \subseteq i) \to (k \subseteq l \lor l \subseteq k))$
28	20 27	syl	$⊢ ((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land (b \in {Base}_{R} \land (k \in C \land x \in k) \land (l \in C \land y \in l))) \to (\forall i \in C \forall j \in C (i \subseteq j \lor j \subseteq i) \to (k \subseteq l \lor l \subseteq k))$
29		simpl1	$⊢ ((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land (b \in {Base}_{R} \land (k \in C \land x \in k) \land (l \in C \land y \in l))) \to R \in Ring$
30		ssel	$⊢ C \subseteq LIdeal (R) \to (k \in C \to k \in LIdeal (R))$
31	30	com12	$⊢ k \in C \to (C \subseteq LIdeal (R) \to k \in LIdeal (R))$
32	31	adantr	$⊢ (k \in C \land x \in k) \to (C \subseteq LIdeal (R) \to k \in LIdeal (R))$
33	32	3ad2ant2	$⊢ (b \in {Base}_{R} \land (k \in C \land x \in k) \land (l \in C \land y \in l)) \to (C \subseteq LIdeal (R) \to k \in LIdeal (R))$
34	33	com12	$⊢ C \subseteq LIdeal (R) \to ((b \in {Base}_{R} \land (k \in C \land x \in k) \land (l \in C \land y \in l)) \to k \in LIdeal (R))$
35	34	3ad2ant3	$⊢ (R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \to ((b \in {Base}_{R} \land (k \in C \land x \in k) \land (l \in C \land y \in l)) \to k \in LIdeal (R))$
36	35	imp	$⊢ ((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land (b \in {Base}_{R} \land (k \in C \land x \in k) \land (l \in C \land y \in l))) \to k \in LIdeal (R)$
37	29 36	jca	$⊢ ((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land (b \in {Base}_{R} \land (k \in C \land x \in k) \land (l \in C \land y \in l))) \to (R \in Ring \land k \in LIdeal (R))$
38		simpr	$⊢ (k \in C \land x \in k) \to x \in k$
39	38	anim2i	$⊢ (b \in {Base}_{R} \land (k \in C \land x \in k)) \to (b \in {Base}_{R} \land x \in k)$
40	39	3adant3	$⊢ (b \in {Base}_{R} \land (k \in C \land x \in k) \land (l \in C \land y \in l)) \to (b \in {Base}_{R} \land x \in k)$
41	40	adantl	$⊢ ((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land (b \in {Base}_{R} \land (k \in C \land x \in k) \land (l \in C \land y \in l))) \to (b \in {Base}_{R} \land x \in k)$
42	37 41	jca	$⊢ ((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land (b \in {Base}_{R} \land (k \in C \land x \in k) \land (l \in C \land y \in l))) \to ((R \in Ring \land k \in LIdeal (R)) \land (b \in {Base}_{R} \land x \in k))$
43	42	adantr	$⊢ (((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land (b \in {Base}_{R} \land (k \in C \land x \in k) \land (l \in C \land y \in l))) \land (k \subseteq l \lor l \subseteq k)) \to ((R \in Ring \land k \in LIdeal (R)) \land (b \in {Base}_{R} \land x \in k))$
44		eqid	$⊢ \cdot_{R} = \cdot_{R}$
45	3 2 44	lidlmcl	$⊢ ((R \in Ring \land k \in LIdeal (R)) \land (b \in {Base}_{R} \land x \in k)) \to b \cdot_{R} x \in k$
46	43 45	syl	$⊢ (((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land (b \in {Base}_{R} \land (k \in C \land x \in k) \land (l \in C \land y \in l))) \land (k \subseteq l \lor l \subseteq k)) \to b \cdot_{R} x \in k$
47		ssel	$⊢ C \subseteq LIdeal (R) \to (l \in C \to l \in LIdeal (R))$
48	47	com12	$⊢ l \in C \to (C \subseteq LIdeal (R) \to l \in LIdeal (R))$
49	48	adantr	$⊢ (l \in C \land y \in l) \to (C \subseteq LIdeal (R) \to l \in LIdeal (R))$
50	49	3ad2ant3	$⊢ (b \in {Base}_{R} \land (k \in C \land x \in k) \land (l \in C \land y \in l)) \to (C \subseteq LIdeal (R) \to l \in LIdeal (R))$
51	50	com12	$⊢ C \subseteq LIdeal (R) \to ((b \in {Base}_{R} \land (k \in C \land x \in k) \land (l \in C \land y \in l)) \to l \in LIdeal (R))$
52	51	3ad2ant3	$⊢ (R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \to ((b \in {Base}_{R} \land (k \in C \land x \in k) \land (l \in C \land y \in l)) \to l \in LIdeal (R))$
53	52	imp	$⊢ ((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land (b \in {Base}_{R} \land (k \in C \land x \in k) \land (l \in C \land y \in l))) \to l \in LIdeal (R)$
54	29 53	jca	$⊢ ((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land (b \in {Base}_{R} \land (k \in C \land x \in k) \land (l \in C \land y \in l))) \to (R \in Ring \land l \in LIdeal (R))$
55	54	adantr	$⊢ (((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land (b \in {Base}_{R} \land (k \in C \land x \in k) \land (l \in C \land y \in l))) \land b \cdot_{R} x \in k) \to (R \in Ring \land l \in LIdeal (R))$
56	55	adantr	$⊢ ((((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land (b \in {Base}_{R} \land (k \in C \land x \in k) \land (l \in C \land y \in l))) \land b \cdot_{R} x \in k) \land k \subseteq l) \to (R \in Ring \land l \in LIdeal (R))$
57		ssel	$⊢ k \subseteq l \to (b \cdot_{R} x \in k \to b \cdot_{R} x \in l)$
58	57	com12	$⊢ b \cdot_{R} x \in k \to (k \subseteq l \to b \cdot_{R} x \in l)$
59	58	adantl	$⊢ (((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land (b \in {Base}_{R} \land (k \in C \land x \in k) \land (l \in C \land y \in l))) \land b \cdot_{R} x \in k) \to (k \subseteq l \to b \cdot_{R} x \in l)$
60	59	imp	$⊢ ((((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land (b \in {Base}_{R} \land (k \in C \land x \in k) \land (l \in C \land y \in l))) \land b \cdot_{R} x \in k) \land k \subseteq l) \to b \cdot_{R} x \in l$
61		simpr	$⊢ (l \in C \land y \in l) \to y \in l$
62	61	3ad2ant3	$⊢ (b \in {Base}_{R} \land (k \in C \land x \in k) \land (l \in C \land y \in l)) \to y \in l$
63	62	ad3antlr	$⊢ ((((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land (b \in {Base}_{R} \land (k \in C \land x \in k) \land (l \in C \land y \in l))) \land b \cdot_{R} x \in k) \land k \subseteq l) \to y \in l$
64		eqid	$⊢ +_{R} = +_{R}$
65	3 64	lidlacl	$⊢ ((R \in Ring \land l \in LIdeal (R)) \land (b \cdot_{R} x \in l \land y \in l)) \to (b \cdot_{R} x) +_{R} y \in l$
66	56 60 63 65	syl12anc	$⊢ ((((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land (b \in {Base}_{R} \land (k \in C \land x \in k) \land (l \in C \land y \in l))) \land b \cdot_{R} x \in k) \land k \subseteq l) \to (b \cdot_{R} x) +_{R} y \in l$
67	17	3ad2ant3	$⊢ (b \in {Base}_{R} \land (k \in C \land x \in k) \land (l \in C \land y \in l)) \to l \in C$
68	67	ad3antlr	$⊢ ((((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land (b \in {Base}_{R} \land (k \in C \land x \in k) \land (l \in C \land y \in l))) \land b \cdot_{R} x \in k) \land k \subseteq l) \to l \in C$
69		elunii	$⊢ ((b \cdot_{R} x) +_{R} y \in l \land l \in C) \to (b \cdot_{R} x) +_{R} y \in ⋃ C$
70	66 68 69	syl2anc	$⊢ ((((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land (b \in {Base}_{R} \land (k \in C \land x \in k) \land (l \in C \land y \in l))) \land b \cdot_{R} x \in k) \land k \subseteq l) \to (b \cdot_{R} x) +_{R} y \in ⋃ C$
71	70	ex	$⊢ (((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land (b \in {Base}_{R} \land (k \in C \land x \in k) \land (l \in C \land y \in l))) \land b \cdot_{R} x \in k) \to (k \subseteq l \to (b \cdot_{R} x) +_{R} y \in ⋃ C)$
72	37	adantr	$⊢ (((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land (b \in {Base}_{R} \land (k \in C \land x \in k) \land (l \in C \land y \in l))) \land b \cdot_{R} x \in k) \to (R \in Ring \land k \in LIdeal (R))$
73	72	adantr	$⊢ ((((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land (b \in {Base}_{R} \land (k \in C \land x \in k) \land (l \in C \land y \in l))) \land b \cdot_{R} x \in k) \land l \subseteq k) \to (R \in Ring \land k \in LIdeal (R))$
74		simpr	$⊢ (((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land (b \in {Base}_{R} \land (k \in C \land x \in k) \land (l \in C \land y \in l))) \land b \cdot_{R} x \in k) \to b \cdot_{R} x \in k$
75	74	adantr	$⊢ ((((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land (b \in {Base}_{R} \land (k \in C \land x \in k) \land (l \in C \land y \in l))) \land b \cdot_{R} x \in k) \land l \subseteq k) \to b \cdot_{R} x \in k$
76		ssel	$⊢ l \subseteq k \to (y \in l \to y \in k)$
77	76	com12	$⊢ y \in l \to (l \subseteq k \to y \in k)$
78	77	adantl	$⊢ (l \in C \land y \in l) \to (l \subseteq k \to y \in k)$
79	78	3ad2ant3	$⊢ (b \in {Base}_{R} \land (k \in C \land x \in k) \land (l \in C \land y \in l)) \to (l \subseteq k \to y \in k)$
80	79	adantl	$⊢ ((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land (b \in {Base}_{R} \land (k \in C \land x \in k) \land (l \in C \land y \in l))) \to (l \subseteq k \to y \in k)$
81	80	adantr	$⊢ (((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land (b \in {Base}_{R} \land (k \in C \land x \in k) \land (l \in C \land y \in l))) \land b \cdot_{R} x \in k) \to (l \subseteq k \to y \in k)$
82	81	imp	$⊢ ((((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land (b \in {Base}_{R} \land (k \in C \land x \in k) \land (l \in C \land y \in l))) \land b \cdot_{R} x \in k) \land l \subseteq k) \to y \in k$
83	3 64	lidlacl	$⊢ ((R \in Ring \land k \in LIdeal (R)) \land (b \cdot_{R} x \in k \land y \in k)) \to (b \cdot_{R} x) +_{R} y \in k$
84	73 75 82 83	syl12anc	$⊢ ((((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land (b \in {Base}_{R} \land (k \in C \land x \in k) \land (l \in C \land y \in l))) \land b \cdot_{R} x \in k) \land l \subseteq k) \to (b \cdot_{R} x) +_{R} y \in k$
85	16	3ad2ant2	$⊢ (b \in {Base}_{R} \land (k \in C \land x \in k) \land (l \in C \land y \in l)) \to k \in C$
86	85	ad3antlr	$⊢ ((((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land (b \in {Base}_{R} \land (k \in C \land x \in k) \land (l \in C \land y \in l))) \land b \cdot_{R} x \in k) \land l \subseteq k) \to k \in C$
87		elunii	$⊢ ((b \cdot_{R} x) +_{R} y \in k \land k \in C) \to (b \cdot_{R} x) +_{R} y \in ⋃ C$
88	84 86 87	syl2anc	$⊢ ((((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land (b \in {Base}_{R} \land (k \in C \land x \in k) \land (l \in C \land y \in l))) \land b \cdot_{R} x \in k) \land l \subseteq k) \to (b \cdot_{R} x) +_{R} y \in ⋃ C$
89	88	ex	$⊢ (((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land (b \in {Base}_{R} \land (k \in C \land x \in k) \land (l \in C \land y \in l))) \land b \cdot_{R} x \in k) \to (l \subseteq k \to (b \cdot_{R} x) +_{R} y \in ⋃ C)$
90	71 89	jaod	$⊢ (((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land (b \in {Base}_{R} \land (k \in C \land x \in k) \land (l \in C \land y \in l))) \land b \cdot_{R} x \in k) \to ((k \subseteq l \lor l \subseteq k) \to (b \cdot_{R} x) +_{R} y \in ⋃ C)$
91	90	impancom	$⊢ (((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land (b \in {Base}_{R} \land (k \in C \land x \in k) \land (l \in C \land y \in l))) \land (k \subseteq l \lor l \subseteq k)) \to (b \cdot_{R} x \in k \to (b \cdot_{R} x) +_{R} y \in ⋃ C)$
92	46 91	mpd	$⊢ (((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land (b \in {Base}_{R} \land (k \in C \land x \in k) \land (l \in C \land y \in l))) \land (k \subseteq l \lor l \subseteq k)) \to (b \cdot_{R} x) +_{R} y \in ⋃ C$
93	92	ex	$⊢ ((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land (b \in {Base}_{R} \land (k \in C \land x \in k) \land (l \in C \land y \in l))) \to ((k \subseteq l \lor l \subseteq k) \to (b \cdot_{R} x) +_{R} y \in ⋃ C)$
94	28 93	syld	$⊢ ((R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \land (b \in {Base}_{R} \land (k \in C \land x \in k) \land (l \in C \land y \in l))) \to (\forall i \in C \forall j \in C (i \subseteq j \lor j \subseteq i) \to (b \cdot_{R} x) +_{R} y \in ⋃ C)$
95	94	ex	$⊢ (R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \to ((b \in {Base}_{R} \land (k \in C \land x \in k) \land (l \in C \land y \in l)) \to (\forall i \in C \forall j \in C (i \subseteq j \lor j \subseteq i) \to (b \cdot_{R} x) +_{R} y \in ⋃ C))$
96	95	com23	$⊢ (R \in Ring \land C \neq \emptyset \land C \subseteq LIdeal (R)) \to (\forall i \in C \forall j \in C (i \subseteq j \lor j \subseteq i) \to ((b \in {Base}_{R} \land (k \in C \land x \in k) \land (l \in C \land y \in l)) \to (b \cdot_{R} x) +_{R} y \in ⋃ C))$
97	96	3exp	$⊢ R \in Ring \to (C \neq \emptyset \to (C \subseteq LIdeal (R) \to (\forall i \in C \forall j \in C (i \subseteq j \lor j \subseteq i) \to ((b \in {Base}_{R} \land (k \in C \land x \in k) \land (l \in C \land y \in l)) \to (b \cdot_{R} x) +_{R} y \in ⋃ C))))$
98	97	3imp2	$⊢ (R \in Ring \land (C \neq \emptyset \land C \subseteq LIdeal (R) \land \forall i \in C \forall j \in C (i \subseteq j \lor j \subseteq i))) \to ((b \in {Base}_{R} \land (k \in C \land x \in k) \land (l \in C \land y \in l)) \to (b \cdot_{R} x) +_{R} y \in ⋃ C)$
99	98	3expd	$⊢ (R \in Ring \land (C \neq \emptyset \land C \subseteq LIdeal (R) \land \forall i \in C \forall j \in C (i \subseteq j \lor j \subseteq i))) \to (b \in {Base}_{R} \to ((k \in C \land x \in k) \to ((l \in C \land y \in l) \to (b \cdot_{R} x) +_{R} y \in ⋃ C)))$
100	99	imp41	$⊢ ((((R \in Ring \land (C \neq \emptyset \land C \subseteq LIdeal (R) \land \forall i \in C \forall j \in C (i \subseteq j \lor j \subseteq i))) \land b \in {Base}_{R}) \land (k \in C \land x \in k)) \land (l \in C \land y \in l)) \to (b \cdot_{R} x) +_{R} y \in ⋃ C$
101	100	rexlimdvaa	$⊢ (((R \in Ring \land (C \neq \emptyset \land C \subseteq LIdeal (R) \land \forall i \in C \forall j \in C (i \subseteq j \lor j \subseteq i))) \land b \in {Base}_{R}) \land (k \in C \land x \in k)) \to (\exists l \in C y \in l \to (b \cdot_{R} x) +_{R} y \in ⋃ C)$
102	15 101	biimtrid	$⊢ (((R \in Ring \land (C \neq \emptyset \land C \subseteq LIdeal (R) \land \forall i \in C \forall j \in C (i \subseteq j \lor j \subseteq i))) \land b \in {Base}_{R}) \land (k \in C \land x \in k)) \to (y \in ⋃ C \to (b \cdot_{R} x) +_{R} y \in ⋃ C)$
103	102	ralrimiv	$⊢ (((R \in Ring \land (C \neq \emptyset \land C \subseteq LIdeal (R) \land \forall i \in C \forall j \in C (i \subseteq j \lor j \subseteq i))) \land b \in {Base}_{R}) \land (k \in C \land x \in k)) \to \forall y \in ⋃ C (b \cdot_{R} x) +_{R} y \in ⋃ C$
104	103	rexlimdvaa	$⊢ ((R \in Ring \land (C \neq \emptyset \land C \subseteq LIdeal (R) \land \forall i \in C \forall j \in C (i \subseteq j \lor j \subseteq i))) \land b \in {Base}_{R}) \to (\exists k \in C x \in k \to \forall y \in ⋃ C (b \cdot_{R} x) +_{R} y \in ⋃ C)$
105	14 104	biimtrid	$⊢ ((R \in Ring \land (C \neq \emptyset \land C \subseteq LIdeal (R) \land \forall i \in C \forall j \in C (i \subseteq j \lor j \subseteq i))) \land b \in {Base}_{R}) \to (x \in ⋃ C \to \forall y \in ⋃ C (b \cdot_{R} x) +_{R} y \in ⋃ C)$
106	105	ralrimiv	$⊢ ((R \in Ring \land (C \neq \emptyset \land C \subseteq LIdeal (R) \land \forall i \in C \forall j \in C (i \subseteq j \lor j \subseteq i))) \land b \in {Base}_{R}) \to \forall x \in ⋃ C \forall y \in ⋃ C (b \cdot_{R} x) +_{R} y \in ⋃ C$
107	106	ralrimiva	$⊢ (R \in Ring \land (C \neq \emptyset \land C \subseteq LIdeal (R) \land \forall i \in C \forall j \in C (i \subseteq j \lor j \subseteq i))) \to \forall b \in {Base}_{R} \forall x \in ⋃ C \forall y \in ⋃ C (b \cdot_{R} x) +_{R} y \in ⋃ C$
108	3 2 64 44	islidl	$⊢ ⋃ C \in LIdeal (R) \leftrightarrow (⋃ C \subseteq {Base}_{R} \land ⋃ C \neq \emptyset \land \forall b \in {Base}_{R} \forall x \in ⋃ C \forall y \in ⋃ C (b \cdot_{R} x) +_{R} y \in ⋃ C)$
109	11 13 107 108	syl3anbrc	$⊢ (R \in Ring \land (C \neq \emptyset \land C \subseteq LIdeal (R) \land \forall i \in C \forall j \in C (i \subseteq j \lor j \subseteq i))) \to ⋃ C \in LIdeal (R)$

Metamath Proof Explorer

Theorem unichnlidl

Proof