unichnidl

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

		Ref	Expression
	Assertion	unichnidl	$⊢ (R \in RingOps \land (C \neq \emptyset \land C \subseteq Idl (R) \land \forall i \in C \forall j \in C (i \subseteq j \lor j \subseteq i))) \to ⋃ C \in Idl (R)$

Proof

Step	Hyp	Ref	Expression
1		dfss3	$⊢ C \subseteq Idl (R) \leftrightarrow \forall i \in C i \in Idl (R)$
2		eqid	$⊢ 1^{st} (R) = 1^{st} (R)$
3		eqid	$⊢ ran 1^{st} (R) = ran 1^{st} (R)$
4	2 3	idlss	$⊢ (R \in RingOps \land i \in Idl (R)) \to i \subseteq ran 1^{st} (R)$
5	4	ex	$⊢ R \in RingOps \to (i \in Idl (R) \to i \subseteq ran 1^{st} (R))$
6	5	ralimdv	$⊢ R \in RingOps \to (\forall i \in C i \in Idl (R) \to \forall i \in C i \subseteq ran 1^{st} (R))$
7	6	imp	$⊢ (R \in RingOps \land \forall i \in C i \in Idl (R)) \to \forall i \in C i \subseteq ran 1^{st} (R)$
8	1 7	sylan2b	$⊢ (R \in RingOps \land C \subseteq Idl (R)) \to \forall i \in C i \subseteq ran 1^{st} (R)$
9		unissb	$⊢ ⋃ C \subseteq ran 1^{st} (R) \leftrightarrow \forall i \in C i \subseteq ran 1^{st} (R)$
10	8 9	sylibr	$⊢ (R \in RingOps \land C \subseteq Idl (R)) \to ⋃ C \subseteq ran 1^{st} (R)$
11	10	3ad2antr2	$⊢ (R \in RingOps \land (C \neq \emptyset \land C \subseteq Idl (R) \land \forall i \in C \forall j \in C (i \subseteq j \lor j \subseteq i))) \to ⋃ C \subseteq ran 1^{st} (R)$
12		eqid	$⊢ GId (1^{st} (R)) = GId (1^{st} (R))$
13	2 12	idl0cl	$⊢ (R \in RingOps \land i \in Idl (R)) \to GId (1^{st} (R)) \in i$
14	13	ex	$⊢ R \in RingOps \to (i \in Idl (R) \to GId (1^{st} (R)) \in i)$
15	14	ralimdv	$⊢ R \in RingOps \to (\forall i \in C i \in Idl (R) \to \forall i \in C GId (1^{st} (R)) \in i)$
16	15	imp	$⊢ (R \in RingOps \land \forall i \in C i \in Idl (R)) \to \forall i \in C GId (1^{st} (R)) \in i$
17	1 16	sylan2b	$⊢ (R \in RingOps \land C \subseteq Idl (R)) \to \forall i \in C GId (1^{st} (R)) \in i$
18		r19.2z	$⊢ (C \neq \emptyset \land \forall i \in C GId (1^{st} (R)) \in i) \to \exists i \in C GId (1^{st} (R)) \in i$
19	17 18	sylan2	$⊢ (C \neq \emptyset \land (R \in RingOps \land C \subseteq Idl (R))) \to \exists i \in C GId (1^{st} (R)) \in i$
20	19	an12s	$⊢ (R \in RingOps \land (C \neq \emptyset \land C \subseteq Idl (R))) \to \exists i \in C GId (1^{st} (R)) \in i$
21		eluni2	$⊢ GId (1^{st} (R)) \in ⋃ C \leftrightarrow \exists i \in C GId (1^{st} (R)) \in i$
22	20 21	sylibr	$⊢ (R \in RingOps \land (C \neq \emptyset \land C \subseteq Idl (R))) \to GId (1^{st} (R)) \in ⋃ C$
23	22	3adantr3	$⊢ (R \in RingOps \land (C \neq \emptyset \land C \subseteq Idl (R) \land \forall i \in C \forall j \in C (i \subseteq j \lor j \subseteq i))) \to GId (1^{st} (R)) \in ⋃ C$
24		eluni2	$⊢ x \in ⋃ C \leftrightarrow \exists k \in C x \in k$
25		sseq1	$⊢ i = k \to (i \subseteq j \leftrightarrow k \subseteq j)$
26		sseq2	$⊢ i = k \to (j \subseteq i \leftrightarrow j \subseteq k)$
27	25 26	orbi12d	$⊢ i = k \to ((i \subseteq j \lor j \subseteq i) \leftrightarrow (k \subseteq j \lor j \subseteq k))$
28	27	ralbidv	$⊢ i = k \to (\forall j \in C (i \subseteq j \lor j \subseteq i) \leftrightarrow \forall j \in C (k \subseteq j \lor j \subseteq k))$
29	28	rspcv	$⊢ k \in C \to (\forall i \in C \forall j \in C (i \subseteq j \lor j \subseteq i) \to \forall j \in C (k \subseteq j \lor j \subseteq k))$
30	29	adantr	$⊢ (k \in C \land x \in k) \to (\forall i \in C \forall j \in C (i \subseteq j \lor j \subseteq i) \to \forall j \in C (k \subseteq j \lor j \subseteq k))$
31	30	ad2antlr	$⊢ ((R \in RingOps \land (k \in C \land x \in k)) \land C \subseteq Idl (R)) \to (\forall i \in C \forall j \in C (i \subseteq j \lor j \subseteq i) \to \forall j \in C (k \subseteq j \lor j \subseteq k))$
32	31	imp	$⊢ (((R \in RingOps \land (k \in C \land x \in k)) \land C \subseteq Idl (R)) \land \forall i \in C \forall j \in C (i \subseteq j \lor j \subseteq i)) \to \forall j \in C (k \subseteq j \lor j \subseteq k)$
33		eluni2	$⊢ y \in ⋃ C \leftrightarrow \exists i \in C y \in i$
34		sseq2	$⊢ j = i \to (k \subseteq j \leftrightarrow k \subseteq i)$
35		sseq1	$⊢ j = i \to (j \subseteq k \leftrightarrow i \subseteq k)$
36	34 35	orbi12d	$⊢ j = i \to ((k \subseteq j \lor j \subseteq k) \leftrightarrow (k \subseteq i \lor i \subseteq k))$
37	36	rspcv	$⊢ i \in C \to (\forall j \in C (k \subseteq j \lor j \subseteq k) \to (k \subseteq i \lor i \subseteq k))$
38	37	ad2antrl	$⊢ (((R \in RingOps \land (k \in C \land x \in k)) \land C \subseteq Idl (R)) \land (i \in C \land y \in i)) \to (\forall j \in C (k \subseteq j \lor j \subseteq k) \to (k \subseteq i \lor i \subseteq k))$
39	38	imp	$⊢ ((((R \in RingOps \land (k \in C \land x \in k)) \land C \subseteq Idl (R)) \land (i \in C \land y \in i)) \land \forall j \in C (k \subseteq j \lor j \subseteq k)) \to (k \subseteq i \lor i \subseteq k)$
40		ssel2	$⊢ (k \subseteq i \land x \in k) \to x \in i$
41	40	ancoms	$⊢ (x \in k \land k \subseteq i) \to x \in i$
42	41	adantll	$⊢ ((k \in C \land x \in k) \land k \subseteq i) \to x \in i$
43		ssel2	$⊢ (C \subseteq Idl (R) \land i \in C) \to i \in Idl (R)$
44	2	idladdcl	$⊢ ((R \in RingOps \land i \in Idl (R)) \land (x \in i \land y \in i)) \to x 1^{st} (R) y \in i$
45	44	ancom2s	$⊢ ((R \in RingOps \land i \in Idl (R)) \land (y \in i \land x \in i)) \to x 1^{st} (R) y \in i$
46	45	expr	$⊢ ((R \in RingOps \land i \in Idl (R)) \land y \in i) \to (x \in i \to x 1^{st} (R) y \in i)$
47	46	an32s	$⊢ ((R \in RingOps \land y \in i) \land i \in Idl (R)) \to (x \in i \to x 1^{st} (R) y \in i)$
48	43 47	sylan2	$⊢ ((R \in RingOps \land y \in i) \land (C \subseteq Idl (R) \land i \in C)) \to (x \in i \to x 1^{st} (R) y \in i)$
49	48	an42s	$⊢ ((R \in RingOps \land C \subseteq Idl (R)) \land (i \in C \land y \in i)) \to (x \in i \to x 1^{st} (R) y \in i)$
50	49	anasss	$⊢ (R \in RingOps \land (C \subseteq Idl (R) \land (i \in C \land y \in i))) \to (x \in i \to x 1^{st} (R) y \in i)$
51	50	imp	$⊢ ((R \in RingOps \land (C \subseteq Idl (R) \land (i \in C \land y \in i))) \land x \in i) \to x 1^{st} (R) y \in i$
52		simprl	$⊢ (C \subseteq Idl (R) \land (i \in C \land y \in i)) \to i \in C$
53	52	ad2antlr	$⊢ ((R \in RingOps \land (C \subseteq Idl (R) \land (i \in C \land y \in i))) \land x \in i) \to i \in C$
54		elunii	$⊢ (x 1^{st} (R) y \in i \land i \in C) \to x 1^{st} (R) y \in ⋃ C$
55	51 53 54	syl2anc	$⊢ ((R \in RingOps \land (C \subseteq Idl (R) \land (i \in C \land y \in i))) \land x \in i) \to x 1^{st} (R) y \in ⋃ C$
56	42 55	sylan2	$⊢ ((R \in RingOps \land (C \subseteq Idl (R) \land (i \in C \land y \in i))) \land ((k \in C \land x \in k) \land k \subseteq i)) \to x 1^{st} (R) y \in ⋃ C$
57	56	expr	$⊢ ((R \in RingOps \land (C \subseteq Idl (R) \land (i \in C \land y \in i))) \land (k \in C \land x \in k)) \to (k \subseteq i \to x 1^{st} (R) y \in ⋃ C)$
58	57	an32s	$⊢ ((R \in RingOps \land (k \in C \land x \in k)) \land (C \subseteq Idl (R) \land (i \in C \land y \in i))) \to (k \subseteq i \to x 1^{st} (R) y \in ⋃ C)$
59	58	anassrs	$⊢ (((R \in RingOps \land (k \in C \land x \in k)) \land C \subseteq Idl (R)) \land (i \in C \land y \in i)) \to (k \subseteq i \to x 1^{st} (R) y \in ⋃ C)$
60	59	imp	$⊢ ((((R \in RingOps \land (k \in C \land x \in k)) \land C \subseteq Idl (R)) \land (i \in C \land y \in i)) \land k \subseteq i) \to x 1^{st} (R) y \in ⋃ C$
61		ssel2	$⊢ (i \subseteq k \land y \in i) \to y \in k$
62	61	ancoms	$⊢ (y \in i \land i \subseteq k) \to y \in k$
63	62	adantll	$⊢ ((i \in C \land y \in i) \land i \subseteq k) \to y \in k$
64		ssel2	$⊢ (C \subseteq Idl (R) \land k \in C) \to k \in Idl (R)$
65	2	idladdcl	$⊢ ((R \in RingOps \land k \in Idl (R)) \land (x \in k \land y \in k)) \to x 1^{st} (R) y \in k$
66	65	expr	$⊢ ((R \in RingOps \land k \in Idl (R)) \land x \in k) \to (y \in k \to x 1^{st} (R) y \in k)$
67	66	an32s	$⊢ ((R \in RingOps \land x \in k) \land k \in Idl (R)) \to (y \in k \to x 1^{st} (R) y \in k)$
68	64 67	sylan2	$⊢ ((R \in RingOps \land x \in k) \land (C \subseteq Idl (R) \land k \in C)) \to (y \in k \to x 1^{st} (R) y \in k)$
69	68	an42s	$⊢ ((R \in RingOps \land C \subseteq Idl (R)) \land (k \in C \land x \in k)) \to (y \in k \to x 1^{st} (R) y \in k)$
70	69	an32s	$⊢ ((R \in RingOps \land (k \in C \land x \in k)) \land C \subseteq Idl (R)) \to (y \in k \to x 1^{st} (R) y \in k)$
71	70	imp	$⊢ (((R \in RingOps \land (k \in C \land x \in k)) \land C \subseteq Idl (R)) \land y \in k) \to x 1^{st} (R) y \in k$
72		simprl	$⊢ (R \in RingOps \land (k \in C \land x \in k)) \to k \in C$
73	72	ad2antrr	$⊢ (((R \in RingOps \land (k \in C \land x \in k)) \land C \subseteq Idl (R)) \land y \in k) \to k \in C$
74		elunii	$⊢ (x 1^{st} (R) y \in k \land k \in C) \to x 1^{st} (R) y \in ⋃ C$
75	71 73 74	syl2anc	$⊢ (((R \in RingOps \land (k \in C \land x \in k)) \land C \subseteq Idl (R)) \land y \in k) \to x 1^{st} (R) y \in ⋃ C$
76	63 75	sylan2	$⊢ (((R \in RingOps \land (k \in C \land x \in k)) \land C \subseteq Idl (R)) \land ((i \in C \land y \in i) \land i \subseteq k)) \to x 1^{st} (R) y \in ⋃ C$
77	76	anassrs	$⊢ ((((R \in RingOps \land (k \in C \land x \in k)) \land C \subseteq Idl (R)) \land (i \in C \land y \in i)) \land i \subseteq k) \to x 1^{st} (R) y \in ⋃ C$
78	60 77	jaodan	$⊢ ((((R \in RingOps \land (k \in C \land x \in k)) \land C \subseteq Idl (R)) \land (i \in C \land y \in i)) \land (k \subseteq i \lor i \subseteq k)) \to x 1^{st} (R) y \in ⋃ C$
79	39 78	syldan	$⊢ ((((R \in RingOps \land (k \in C \land x \in k)) \land C \subseteq Idl (R)) \land (i \in C \land y \in i)) \land \forall j \in C (k \subseteq j \lor j \subseteq k)) \to x 1^{st} (R) y \in ⋃ C$
80	79	an32s	$⊢ ((((R \in RingOps \land (k \in C \land x \in k)) \land C \subseteq Idl (R)) \land \forall j \in C (k \subseteq j \lor j \subseteq k)) \land (i \in C \land y \in i)) \to x 1^{st} (R) y \in ⋃ C$
81	80	rexlimdvaa	$⊢ (((R \in RingOps \land (k \in C \land x \in k)) \land C \subseteq Idl (R)) \land \forall j \in C (k \subseteq j \lor j \subseteq k)) \to (\exists i \in C y \in i \to x 1^{st} (R) y \in ⋃ C)$
82	33 81	biimtrid	$⊢ (((R \in RingOps \land (k \in C \land x \in k)) \land C \subseteq Idl (R)) \land \forall j \in C (k \subseteq j \lor j \subseteq k)) \to (y \in ⋃ C \to x 1^{st} (R) y \in ⋃ C)$
83	82	ralrimiv	$⊢ (((R \in RingOps \land (k \in C \land x \in k)) \land C \subseteq Idl (R)) \land \forall j \in C (k \subseteq j \lor j \subseteq k)) \to \forall y \in ⋃ C x 1^{st} (R) y \in ⋃ C$
84	32 83	syldan	$⊢ (((R \in RingOps \land (k \in C \land x \in k)) \land C \subseteq Idl (R)) \land \forall i \in C \forall j \in C (i \subseteq j \lor j \subseteq i)) \to \forall y \in ⋃ C x 1^{st} (R) y \in ⋃ C$
85	84	anasss	$⊢ ((R \in RingOps \land (k \in C \land x \in k)) \land (C \subseteq Idl (R) \land \forall i \in C \forall j \in C (i \subseteq j \lor j \subseteq i))) \to \forall y \in ⋃ C x 1^{st} (R) y \in ⋃ C$
86	85	3adantr1	$⊢ ((R \in RingOps \land (k \in C \land x \in k)) \land (C \neq \emptyset \land C \subseteq Idl (R) \land \forall i \in C \forall j \in C (i \subseteq j \lor j \subseteq i))) \to \forall y \in ⋃ C x 1^{st} (R) y \in ⋃ C$
87	86	an32s	$⊢ ((R \in RingOps \land (C \neq \emptyset \land C \subseteq Idl (R) \land \forall i \in C \forall j \in C (i \subseteq j \lor j \subseteq i))) \land (k \in C \land x \in k)) \to \forall y \in ⋃ C x 1^{st} (R) y \in ⋃ C$
88		eqid	$⊢ 2^{nd} (R) = 2^{nd} (R)$
89	2 88 3	idllmulcl	$⊢ ((R \in RingOps \land k \in Idl (R)) \land (x \in k \land z \in ran 1^{st} (R))) \to z 2^{nd} (R) x \in k$
90	89	exp43	$⊢ R \in RingOps \to (k \in Idl (R) \to (x \in k \to (z \in ran 1^{st} (R) \to z 2^{nd} (R) x \in k)))$
91	90	com23	$⊢ R \in RingOps \to (x \in k \to (k \in Idl (R) \to (z \in ran 1^{st} (R) \to z 2^{nd} (R) x \in k)))$
92	91	imp41	$⊢ (((R \in RingOps \land x \in k) \land k \in Idl (R)) \land z \in ran 1^{st} (R)) \to z 2^{nd} (R) x \in k$
93	64 92	sylanl2	$⊢ (((R \in RingOps \land x \in k) \land (C \subseteq Idl (R) \land k \in C)) \land z \in ran 1^{st} (R)) \to z 2^{nd} (R) x \in k$
94		simplrr	$⊢ (((R \in RingOps \land x \in k) \land (C \subseteq Idl (R) \land k \in C)) \land z \in ran 1^{st} (R)) \to k \in C$
95		elunii	$⊢ (z 2^{nd} (R) x \in k \land k \in C) \to z 2^{nd} (R) x \in ⋃ C$
96	93 94 95	syl2anc	$⊢ (((R \in RingOps \land x \in k) \land (C \subseteq Idl (R) \land k \in C)) \land z \in ran 1^{st} (R)) \to z 2^{nd} (R) x \in ⋃ C$
97	2 88 3	idlrmulcl	$⊢ ((R \in RingOps \land k \in Idl (R)) \land (x \in k \land z \in ran 1^{st} (R))) \to x 2^{nd} (R) z \in k$
98	97	exp43	$⊢ R \in RingOps \to (k \in Idl (R) \to (x \in k \to (z \in ran 1^{st} (R) \to x 2^{nd} (R) z \in k)))$
99	98	com23	$⊢ R \in RingOps \to (x \in k \to (k \in Idl (R) \to (z \in ran 1^{st} (R) \to x 2^{nd} (R) z \in k)))$
100	99	imp41	$⊢ (((R \in RingOps \land x \in k) \land k \in Idl (R)) \land z \in ran 1^{st} (R)) \to x 2^{nd} (R) z \in k$
101	64 100	sylanl2	$⊢ (((R \in RingOps \land x \in k) \land (C \subseteq Idl (R) \land k \in C)) \land z \in ran 1^{st} (R)) \to x 2^{nd} (R) z \in k$
102		elunii	$⊢ (x 2^{nd} (R) z \in k \land k \in C) \to x 2^{nd} (R) z \in ⋃ C$
103	101 94 102	syl2anc	$⊢ (((R \in RingOps \land x \in k) \land (C \subseteq Idl (R) \land k \in C)) \land z \in ran 1^{st} (R)) \to x 2^{nd} (R) z \in ⋃ C$
104	96 103	jca	$⊢ (((R \in RingOps \land x \in k) \land (C \subseteq Idl (R) \land k \in C)) \land z \in ran 1^{st} (R)) \to (z 2^{nd} (R) x \in ⋃ C \land x 2^{nd} (R) z \in ⋃ C)$
105	104	ralrimiva	$⊢ ((R \in RingOps \land x \in k) \land (C \subseteq Idl (R) \land k \in C)) \to \forall z \in ran 1^{st} (R) (z 2^{nd} (R) x \in ⋃ C \land x 2^{nd} (R) z \in ⋃ C)$
106	105	an42s	$⊢ ((R \in RingOps \land C \subseteq Idl (R)) \land (k \in C \land x \in k)) \to \forall z \in ran 1^{st} (R) (z 2^{nd} (R) x \in ⋃ C \land x 2^{nd} (R) z \in ⋃ C)$
107	106	an32s	$⊢ ((R \in RingOps \land (k \in C \land x \in k)) \land C \subseteq Idl (R)) \to \forall z \in ran 1^{st} (R) (z 2^{nd} (R) x \in ⋃ C \land x 2^{nd} (R) z \in ⋃ C)$
108	107	3ad2antr2	$⊢ ((R \in RingOps \land (k \in C \land x \in k)) \land (C \neq \emptyset \land C \subseteq Idl (R) \land \forall i \in C \forall j \in C (i \subseteq j \lor j \subseteq i))) \to \forall z \in ran 1^{st} (R) (z 2^{nd} (R) x \in ⋃ C \land x 2^{nd} (R) z \in ⋃ C)$
109	108	an32s	$⊢ ((R \in RingOps \land (C \neq \emptyset \land C \subseteq Idl (R) \land \forall i \in C \forall j \in C (i \subseteq j \lor j \subseteq i))) \land (k \in C \land x \in k)) \to \forall z \in ran 1^{st} (R) (z 2^{nd} (R) x \in ⋃ C \land x 2^{nd} (R) z \in ⋃ C)$
110	87 109	jca	$⊢ ((R \in RingOps \land (C \neq \emptyset \land C \subseteq Idl (R) \land \forall i \in C \forall j \in C (i \subseteq j \lor j \subseteq i))) \land (k \in C \land x \in k)) \to (\forall y \in ⋃ C x 1^{st} (R) y \in ⋃ C \land \forall z \in ran 1^{st} (R) (z 2^{nd} (R) x \in ⋃ C \land x 2^{nd} (R) z \in ⋃ C))$
111	110	rexlimdvaa	$⊢ (R \in RingOps \land (C \neq \emptyset \land C \subseteq Idl (R) \land \forall i \in C \forall j \in C (i \subseteq j \lor j \subseteq i))) \to (\exists k \in C x \in k \to (\forall y \in ⋃ C x 1^{st} (R) y \in ⋃ C \land \forall z \in ran 1^{st} (R) (z 2^{nd} (R) x \in ⋃ C \land x 2^{nd} (R) z \in ⋃ C)))$
112	24 111	biimtrid	$⊢ (R \in RingOps \land (C \neq \emptyset \land C \subseteq Idl (R) \land \forall i \in C \forall j \in C (i \subseteq j \lor j \subseteq i))) \to (x \in ⋃ C \to (\forall y \in ⋃ C x 1^{st} (R) y \in ⋃ C \land \forall z \in ran 1^{st} (R) (z 2^{nd} (R) x \in ⋃ C \land x 2^{nd} (R) z \in ⋃ C)))$
113	112	ralrimiv	$⊢ (R \in RingOps \land (C \neq \emptyset \land C \subseteq Idl (R) \land \forall i \in C \forall j \in C (i \subseteq j \lor j \subseteq i))) \to \forall x \in ⋃ C (\forall y \in ⋃ C x 1^{st} (R) y \in ⋃ C \land \forall z \in ran 1^{st} (R) (z 2^{nd} (R) x \in ⋃ C \land x 2^{nd} (R) z \in ⋃ C))$
114	2 88 3 12	isidl	$⊢ R \in RingOps \to (⋃ C \in Idl (R) \leftrightarrow (⋃ C \subseteq ran 1^{st} (R) \land GId (1^{st} (R)) \in ⋃ C \land \forall x \in ⋃ C (\forall y \in ⋃ C x 1^{st} (R) y \in ⋃ C \land \forall z \in ran 1^{st} (R) (z 2^{nd} (R) x \in ⋃ C \land x 2^{nd} (R) z \in ⋃ C))))$
115	114	adantr	$⊢ (R \in RingOps \land (C \neq \emptyset \land C \subseteq Idl (R) \land \forall i \in C \forall j \in C (i \subseteq j \lor j \subseteq i))) \to (⋃ C \in Idl (R) \leftrightarrow (⋃ C \subseteq ran 1^{st} (R) \land GId (1^{st} (R)) \in ⋃ C \land \forall x \in ⋃ C (\forall y \in ⋃ C x 1^{st} (R) y \in ⋃ C \land \forall z \in ran 1^{st} (R) (z 2^{nd} (R) x \in ⋃ C \land x 2^{nd} (R) z \in ⋃ C))))$
116	11 23 113 115	mpbir3and	$⊢ (R \in RingOps \land (C \neq \emptyset \land C \subseteq Idl (R) \land \forall i \in C \forall j \in C (i \subseteq j \lor j \subseteq i))) \to ⋃ C \in Idl (R)$

Metamath Proof Explorer

Theorem unichnidl

Proof