Theorem unichnidl 16179

Description: The union of a nonempty chain of ideals is an ideal.

Assertion

Ref	Expression
unichnidl	|- ((R e. Ring /\ (C =/= (/) /\ C C_ (Idl` R) /\ A.i e. C A.j e. C (i C_ j \/ j C_ i))) -> U.C e. (Idl` R))

Distinct variable groups:   R,i   C,i,j

Proof of Theorem unichnidl

Step	Hyp	Ref	Expression
1		eqid 1884	. . . . . . . . . 10 |- (1st` R) = (1st` R)
2		eqid 1884	. . . . . . . . . 10 |- ran (1st` R) = ran (1st` R)
3	1, 2	idlss 16164	. . . . . . . . 9 |- ((R e. Ring /\ i e. (Idl` R)) -> i C_ ran (1st` R))
4	3	ex 402	. . . . . . . 8 |- (R e. Ring -> (i e. (Idl` R) -> i C_ ran (1st` R)))
5	4	ralimdv 2172	. . . . . . 7 |- (R e. Ring -> (A.i e. C i e. (Idl` R) -> A.i e. C i C_ ran (1st` R)))
6	5	imp 377	. . . . . 6 |- ((R e. Ring /\ A.i e. C i e. (Idl` R)) -> A.i e. C i C_ ran (1st` R))
7		dfss3 2611	. . . . . 6 |- (C C_ (Idl` R) <-> A.i e. C i e. (Idl` R))
8	6, 7	sylan2b 501	. . . . 5 |- ((R e. Ring /\ C C_ (Idl` R)) -> A.i e. C i C_ ran (1st` R))
9		unissb 3208	. . . . 5 |- (U.C C_ ran (1st` R) <-> A.i e. C i C_ ran (1st` R))
10	8, 9	sylibr 217	. . . 4 |- ((R e. Ring /\ C C_ (Idl` R)) -> U.C C_ ran (1st` R))
11	10	3ad2antr2 1042	. . 3 |- ((R e. Ring /\ (C =/= (/) /\ C C_ (Idl` R) /\ A.i e. C A.j e. C (i C_ j \/ j C_ i))) -> U.C C_ ran (1st` R))
12		r19.2z 2958	. . . . . . 7 |- ((C =/= (/) /\ A.i e. C (Id` (1st` R)) e. i) -> E.i e. C (Id` (1st` R)) e. i)
13		eqid 1884	. . . . . . . . . . . 12 |- (Id` (1st` R)) = (Id` (1st` R))
14	1, 13	idl0cl 16166	. . . . . . . . . . 11 |- ((R e. Ring /\ i e. (Idl` R)) -> (Id` (1st` R)) e. i)
15	14	ex 402	. . . . . . . . . 10 |- (R e. Ring -> (i e. (Idl` R) -> (Id` (1st` R)) e. i))
16	15	ralimdv 2172	. . . . . . . . 9 |- (R e. Ring -> (A.i e. C i e. (Idl` R) -> A.i e. C (Id` (1st` R)) e. i))
17	16	imp 377	. . . . . . . 8 |- ((R e. Ring /\ A.i e. C i e. (Idl` R)) -> A.i e. C (Id` (1st` R)) e. i)
18	17, 7	sylan2b 501	. . . . . . 7 |- ((R e. Ring /\ C C_ (Idl` R)) -> A.i e. C (Id` (1st` R)) e. i)
19	12, 18	sylan2 500	. . . . . 6 |- ((C =/= (/) /\ (R e. Ring /\ C C_ (Idl` R))) -> E.i e. C (Id` (1st` R)) e. i)
20	19	an1s 544	. . . . 5 |- ((R e. Ring /\ (C =/= (/) /\ C C_ (Idl` R))) -> E.i e. C (Id` (1st` R)) e. i)
21		eluni2 3181	. . . . 5 |- ((Id` (1st` R)) e. U.C <-> E.i e. C (Id` (1st` R)) e. i)
22	20, 21	sylibr 217	. . . 4 |- ((R e. Ring /\ (C =/= (/) /\ C C_ (Idl` R))) -> (Id` (1st` R)) e. U.C)
23	22	3adantr3 1037	. . 3 |- ((R e. Ring /\ (C =/= (/) /\ C C_ (Idl` R) /\ A.i e. C A.j e. C (i C_ j \/ j C_ i))) -> (Id` (1st` R)) e. U.C)
24		sseq1 2637	. . . . . . . . . . . . . . . . . 18 |- (i = k -> (i C_ j <-> k C_ j))
25		sseq2 2639	. . . . . . . . . . . . . . . . . 18 |- (i = k -> (j C_ i <-> j C_ k))
26	24, 25	orbi12d 689	. . . . . . . . . . . . . . . . 17 |- (i = k -> ((i C_ j \/ j C_ i) <-> (k C_ j \/ j C_ k)))
27	26	ralbidv 2123	. . . . . . . . . . . . . . . 16 |- (i = k -> (A.j e. C (i C_ j \/ j C_ i) <-> A.j e. C (k C_ j \/ j C_ k)))
28	27	rcla4v 2376	. . . . . . . . . . . . . . 15 |- (k e. C -> (A.i e. C A.j e. C (i C_ j \/ j C_ i) -> A.j e. C (k C_ j \/ j C_ k)))
29	28	adantr 425	. . . . . . . . . . . . . 14 |- ((k e. C /\ x e. k) -> (A.i e. C A.j e. C (i C_ j \/ j C_ i) -> A.j e. C (k C_ j \/ j C_ k)))
30	29	ad2antlr 441	. . . . . . . . . . . . 13 |- (((R e. Ring /\ (k e. C /\ x e. k)) /\ C C_ (Idl` R)) -> (A.i e. C A.j e. C (i C_ j \/ j C_ i) -> A.j e. C (k C_ j \/ j C_ k)))
31	30	imp 377	. . . . . . . . . . . 12 |- ((((R e. Ring /\ (k e. C /\ x e. k)) /\ C C_ (Idl` R)) /\ A.i e. C A.j e. C (i C_ j \/ j C_ i)) -> A.j e. C (k C_ j \/ j C_ k))
32		sseq2 2639	. . . . . . . . . . . . . . . . . . . . . 22 |- (j = i -> (k C_ j <-> k C_ i))
33		sseq1 2637	. . . . . . . . . . . . . . . . . . . . . 22 |- (j = i -> (j C_ k <-> i C_ k))
34	32, 33	orbi12d 689	. . . . . . . . . . . . . . . . . . . . 21 |- (j = i -> ((k C_ j \/ j C_ k) <-> (k C_ i \/ i C_ k)))
35	34	rcla4v 2376	. . . . . . . . . . . . . . . . . . . 20 |- (i e. C -> (A.j e. C (k C_ j \/ j C_ k) -> (k C_ i \/ i C_ k)))
36	35	ad2antrl 442	. . . . . . . . . . . . . . . . . . 19 |- ((((R e. Ring /\ (k e. C /\ x e. k)) /\ C C_ (Idl` R)) /\ (i e. C /\ y e. i)) -> (A.j e. C (k C_ j \/ j C_ k) -> (k C_ i \/ i C_ k)))
37	36	imp 377	. . . . . . . . . . . . . . . . . 18 |- (((((R e. Ring /\ (k e. C /\ x e. k)) /\ C C_ (Idl` R)) /\ (i e. C /\ y e. i)) /\ A.j e. C (k C_ j \/ j C_ k)) -> (k C_ i \/ i C_ k))
38	1	idladdcl 16167	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- (((R e. Ring /\ i e. (Idl` R)) /\ (x e. i /\ y e. i)) -> (x(1st` R)y) e. i)
39	38	ancom2s 545	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (((R e. Ring /\ i e. (Idl` R)) /\ (y e. i /\ x e. i)) -> (x(1st` R)y) e. i)
40	39	expr 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (((R e. Ring /\ i e. (Idl` R)) /\ y e. i) -> (x e. i -> (x(1st` R)y) e. i))
41	40	an1rs 547	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (((R e. Ring /\ y e. i) /\ i e. (Idl` R)) -> (x e. i -> (x(1st` R)y) e. i))
42		ssel2 2616	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((C C_ (Idl` R) /\ i e. C) -> i e. (Idl` R))
43	41, 42	sylan2 500	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((R e. Ring /\ y e. i) /\ (C C_ (Idl` R) /\ i e. C)) -> (x e. i -> (x(1st` R)y) e. i))
44	43	an42s 567	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((R e. Ring /\ C C_ (Idl` R)) /\ (i e. C /\ y e. i)) -> (x e. i -> (x(1st` R)y) e. i))
45	44	anasss 488	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((R e. Ring /\ (C C_ (Idl` R) /\ (i e. C /\ y e. i))) -> (x e. i -> (x(1st` R)y) e. i))
46	45	imp 377	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((R e. Ring /\ (C C_ (Idl` R) /\ (i e. C /\ y e. i))) /\ x e. i) -> (x(1st` R)y) e. i)
47		simprl 450	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((C C_ (Idl` R) /\ (i e. C /\ y e. i)) -> i e. C)
48	47	ad2antlr 441	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((R e. Ring /\ (C C_ (Idl` R) /\ (i e. C /\ y e. i))) /\ x e. i) -> i e. C)
49		elunii 3182	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((x(1st` R)y) e. i /\ i e. C) -> (x(1st` R)y) e. U.C)
50	46, 48, 49	syl11anc 524	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((R e. Ring /\ (C C_ (Idl` R) /\ (i e. C /\ y e. i))) /\ x e. i) -> (x(1st` R)y) e. U.C)
51		ssel2 2616	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((k C_ i /\ x e. k) -> x e. i)
52	51	ancoms 484	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((x e. k /\ k C_ i) -> x e. i)
53	52	adantll 428	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((k e. C /\ x e. k) /\ k C_ i) -> x e. i)
54	50, 53	sylan2 500	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((R e. Ring /\ (C C_ (Idl` R) /\ (i e. C /\ y e. i))) /\ ((k e. C /\ x e. k) /\ k C_ i)) -> (x(1st` R)y) e. U.C)
55	54	expr 418	. . . . . . . . . . . . . . . . . . . . . 22 |- (((R e. Ring /\ (C C_ (Idl` R) /\ (i e. C /\ y e. i))) /\ (k e. C /\ x e. k)) -> (k C_ i -> (x(1st` R)y) e. U.C))
56	55	an1rs 547	. . . . . . . . . . . . . . . . . . . . 21 |- (((R e. Ring /\ (k e. C /\ x e. k)) /\ (C C_ (Idl` R) /\ (i e. C /\ y e. i))) -> (k C_ i -> (x(1st` R)y) e. U.C))
57	56	anassrs 489	. . . . . . . . . . . . . . . . . . . 20 |- ((((R e. Ring /\ (k e. C /\ x e. k)) /\ C C_ (Idl` R)) /\ (i e. C /\ y e. i)) -> (k C_ i -> (x(1st` R)y) e. U.C))
58	57	imp 377	. . . . . . . . . . . . . . . . . . 19 |- (((((R e. Ring /\ (k e. C /\ x e. k)) /\ C C_ (Idl` R)) /\ (i e. C /\ y e. i)) /\ k C_ i) -> (x(1st` R)y) e. U.C)
59	1	idladdcl 16167	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((R e. Ring /\ k e. (Idl` R)) /\ (x e. k /\ y e. k)) -> (x(1st` R)y) e. k)
60	59	expr 418	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((R e. Ring /\ k e. (Idl` R)) /\ x e. k) -> (y e. k -> (x(1st` R)y) e. k))
61	60	an1rs 547	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((R e. Ring /\ x e. k) /\ k e. (Idl` R)) -> (y e. k -> (x(1st` R)y) e. k))
62		ssel2 2616	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((C C_ (Idl` R) /\ k e. C) -> k e. (Idl` R))
63	61, 62	sylan2 500	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((R e. Ring /\ x e. k) /\ (C C_ (Idl` R) /\ k e. C)) -> (y e. k -> (x(1st` R)y) e. k))
64	63	an42s 567	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((R e. Ring /\ C C_ (Idl` R)) /\ (k e. C /\ x e. k)) -> (y e. k -> (x(1st` R)y) e. k))
65	64	an1rs 547	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((R e. Ring /\ (k e. C /\ x e. k)) /\ C C_ (Idl` R)) -> (y e. k -> (x(1st` R)y) e. k))
66	65	imp 377	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((R e. Ring /\ (k e. C /\ x e. k)) /\ C C_ (Idl` R)) /\ y e. k) -> (x(1st` R)y) e. k)
67		simprl 450	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((R e. Ring /\ (k e. C /\ x e. k)) -> k e. C)
68	67	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((R e. Ring /\ (k e. C /\ x e. k)) /\ C C_ (Idl` R)) /\ y e. k) -> k e. C)
69		elunii 3182	. . . . . . . . . . . . . . . . . . . . . 22 |- (((x(1st` R)y) e. k /\ k e. C) -> (x(1st` R)y) e. U.C)
70	66, 68, 69	syl11anc 524	. . . . . . . . . . . . . . . . . . . . 21 |- ((((R e. Ring /\ (k e. C /\ x e. k)) /\ C C_ (Idl` R)) /\ y e. k) -> (x(1st` R)y) e. U.C)
71		ssel2 2616	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((i C_ k /\ y e. i) -> y e. k)
72	71	ancoms 484	. . . . . . . . . . . . . . . . . . . . . 22 |- ((y e. i /\ i C_ k) -> y e. k)
73	72	adantll 428	. . . . . . . . . . . . . . . . . . . . 21 |- (((i e. C /\ y e. i) /\ i C_ k) -> y e. k)
74	70, 73	sylan2 500	. . . . . . . . . . . . . . . . . . . 20 |- ((((R e. Ring /\ (k e. C /\ x e. k)) /\ C C_ (Idl` R)) /\ ((i e. C /\ y e. i) /\ i C_ k)) -> (x(1st` R)y) e. U.C)
75	74	anassrs 489	. . . . . . . . . . . . . . . . . . 19 |- (((((R e. Ring /\ (k e. C /\ x e. k)) /\ C C_ (Idl` R)) /\ (i e. C /\ y e. i)) /\ i C_ k) -> (x(1st` R)y) e. U.C)
76	58, 75	jaodan 471	. . . . . . . . . . . . . . . . . 18 |- (((((R e. Ring /\ (k e. C /\ x e. k)) /\ C C_ (Idl` R)) /\ (i e. C /\ y e. i)) /\ (k C_ i \/ i C_ k)) -> (x(1st` R)y) e. U.C)
77	37, 76	syldan 516	. . . . . . . . . . . . . . . . 17 |- (((((R e. Ring /\ (k e. C /\ x e. k)) /\ C C_ (Idl` R)) /\ (i e. C /\ y e. i)) /\ A.j e. C (k C_ j \/ j C_ k)) -> (x(1st` R)y) e. U.C)
78	77	an1rs 547	. . . . . . . . . . . . . . . 16 |- (((((R e. Ring /\ (k e. C /\ x e. k)) /\ C C_ (Idl` R)) /\ A.j e. C (k C_ j \/ j C_ k)) /\ (i e. C /\ y e. i)) -> (x(1st` R)y) e. U.C)
79	78	exp32 408	. . . . . . . . . . . . . . 15 |- ((((R e. Ring /\ (k e. C /\ x e. k)) /\ C C_ (Idl` R)) /\ A.j e. C (k C_ j \/ j C_ k)) -> (i e. C -> (y e. i -> (x(1st` R)y) e. U.C)))
80	79	r19.23adv 2215	. . . . . . . . . . . . . 14 |- ((((R e. Ring /\ (k e. C /\ x e. k)) /\ C C_ (Idl` R)) /\ A.j e. C (k C_ j \/ j C_ k)) -> (E.i e. C y e. i -> (x(1st` R)y) e. U.C))
81		eluni2 3181	. . . . . . . . . . . . . 14 |- (y e. U.C <-> E.i e. C y e. i)
82	80, 81	syl5ib 223	. . . . . . . . . . . . 13 |- ((((R e. Ring /\ (k e. C /\ x e. k)) /\ C C_ (Idl` R)) /\ A.j e. C (k C_ j \/ j C_ k)) -> (y e. U.C -> (x(1st` R)y) e. U.C))
83	82	r19.21aiv 2175	. . . . . . . . . . . 12 |- ((((R e. Ring /\ (k e. C /\ x e. k)) /\ C C_ (Idl` R)) /\ A.j e. C (k C_ j \/ j C_ k)) -> A.y e. U.C(x(1st` R)y) e. U.C)
84	31, 83	syldan 516	. . . . . . . . . . 11 |- ((((R e. Ring /\ (k e. C /\ x e. k)) /\ C C_ (Idl` R)) /\ A.i e. C A.j e. C (i C_ j \/ j C_ i)) -> A.y e. U.C(x(1st` R)y) e. U.C)
85	84	anasss 488	. . . . . . . . . 10 |- (((R e. Ring /\ (k e. C /\ x e. k)) /\ (C C_ (Idl` R) /\ A.i e. C A.j e. C (i C_ j \/ j C_ i))) -> A.y e. U.C(x(1st` R)y) e. U.C)
86	85	3adantr1 1035	. . . . . . . . 9 |- (((R e. Ring /\ (k e. C /\ x e. k)) /\ (C =/= (/) /\ C C_ (Idl` R) /\ A.i e. C A.j e. C (i C_ j \/ j C_ i))) -> A.y e. U.C(x(1st` R)y) e. U.C)
87	86	an1rs 547	. . . . . . . 8 |- (((R e. Ring /\ (C =/= (/) /\ C C_ (Idl` R) /\ A.i e. C A.j e. C (i C_ j \/ j C_ i))) /\ (k e. C /\ x e. k)) -> A.y e. U.C(x(1st` R)y) e. U.C)
88		eqid 1884	. . . . . . . . . . . . . . . . . . . 20 |- (2nd` R) = (2nd` R)
89	1, 88, 2	idllmulcl 16168	. . . . . . . . . . . . . . . . . . 19 |- (((R e. Ring /\ k e. (Idl` R)) /\ (x e. k /\ z e. ran (1st` R))) -> (z(2nd` R)x) e. k)
90	89	exp43 415	. . . . . . . . . . . . . . . . . 18 |- (R e. Ring -> (k e. (Idl` R) -> (x e. k -> (z e. ran (1st` R) -> (z(2nd` R)x) e. k))))
91	90	com23 36	. . . . . . . . . . . . . . . . 17 |- (R e. Ring -> (x e. k -> (k e. (Idl` R) -> (z e. ran (1st` R) -> (z(2nd` R)x) e. k))))
92	91	imp41 395	. . . . . . . . . . . . . . . 16 |- ((((R e. Ring /\ x e. k) /\ k e. (Idl` R)) /\ z e. ran (1st` R)) -> (z(2nd` R)x) e. k)
93	92, 62	sylanl2 510	. . . . . . . . . . . . . . 15 |- ((((R e. Ring /\ x e. k) /\ (C C_ (Idl` R) /\ k e. C)) /\ z e. ran (1st` R)) -> (z(2nd` R)x) e. k)
94		simplrr 455	. . . . . . . . . . . . . . 15 |- ((((R e. Ring /\ x e. k) /\ (C C_ (Idl` R) /\ k e. C)) /\ z e. ran (1st` R)) -> k e. C)
95		elunii 3182	. . . . . . . . . . . . . . 15 |- (((z(2nd` R)x) e. k /\ k e. C) -> (z(2nd` R)x) e. U.C)
96	93, 94, 95	syl11anc 524	. . . . . . . . . . . . . 14 |- ((((R e. Ring /\ x e. k) /\ (C C_ (Idl` R) /\ k e. C)) /\ z e. ran (1st` R)) -> (z(2nd` R)x) e. U.C)
97	1, 88, 2	idlrmulcl 16169	. . . . . . . . . . . . . . . . . . 19 |- (((R e. Ring /\ k e. (Idl` R)) /\ (x e. k /\ z e. ran (1st` R))) -> (x(2nd` R)z) e. k)
98	97	exp43 415	. . . . . . . . . . . . . . . . . 18 |- (R e. Ring -> (k e. (Idl` R) -> (x e. k -> (z e. ran (1st` R) -> (x(2nd` R)z) e. k))))
99	98	com23 36	. . . . . . . . . . . . . . . . 17 |- (R e. Ring -> (x e. k -> (k e. (Idl` R) -> (z e. ran (1st` R) -> (x(2nd` R)z) e. k))))
100	99	imp41 395	. . . . . . . . . . . . . . . 16 |- ((((R e. Ring /\ x e. k) /\ k e. (Idl` R)) /\ z e. ran (1st` R)) -> (x(2nd` R)z) e. k)
101	100, 62	sylanl2 510	. . . . . . . . . . . . . . 15 |- ((((R e. Ring /\ x e. k) /\ (C C_ (Idl` R) /\ k e. C)) /\ z e. ran (1st` R)) -> (x(2nd` R)z) e. k)
102		elunii 3182	. . . . . . . . . . . . . . 15 |- (((x(2nd` R)z) e. k /\ k e. C) -> (x(2nd` R)z) e. U.C)
103	101, 94, 102	syl11anc 524	. . . . . . . . . . . . . 14 |- ((((R e. Ring /\ x e. k) /\ (C C_ (Idl` R) /\ k e. C)) /\ z e. ran (1st` R)) -> (x(2nd` R)z) e. U.C)
104	96, 103	jca 310	. . . . . . . . . . . . 13 |- ((((R e. Ring /\ x e. k) /\ (C C_ (Idl` R) /\ k e. C)) /\ z e. ran (1st` R)) -> ((z(2nd` R)x) e. U.C /\ (x(2nd` R)z) e. U.C))
105	104	r19.21aiva 2176	. . . . . . . . . . . 12 |- (((R e. Ring /\ x e. k) /\ (C C_ (Idl` R) /\ k e. C)) -> A.z e. ran (1st` R)((z(2nd` R)x) e. U.C /\ (x(2nd` R)z) e. U.C))
106	105	an42s 567	. . . . . . . . . . 11 |- (((R e. Ring /\ C C_ (Idl` R)) /\ (k e. C /\ x e. k)) -> A.z e. ran (1st` R)((z(2nd` R)x) e. U.C /\ (x(2nd` R)z) e. U.C))
107	106	an1rs 547	. . . . . . . . . 10 |- (((R e. Ring /\ (k e. C /\ x e. k)) /\ C C_ (Idl` R)) -> A.z e. ran (1st` R)((z(2nd` R)x) e. U.C /\ (x(2nd` R)z) e. U.C))
108	107	3ad2antr2 1042	. . . . . . . . 9 |- (((R e. Ring /\ (k e. C /\ x e. k)) /\ (C =/= (/) /\ C C_ (Idl` R) /\ A.i e. C A.j e. C (i C_ j \/ j C_ i))) -> A.z e. ran (1st` R)((z(2nd` R)x) e. U.C /\ (x(2nd` R)z) e. U.C))
109	108	an1rs 547	. . . . . . . 8 |- (((R e. Ring /\ (C =/= (/) /\ C C_ (Idl` R) /\ A.i e. C A.j e. C (i C_ j \/ j C_ i))) /\ (k e. C /\ x e. k)) -> A.z e. ran (1st` R)((z(2nd` R)x) e. U.C /\ (x(2nd` R)z) e. U.C))
110	87, 109	jca 310	. . . . . . 7 |- (((R e. Ring /\ (C =/= (/) /\ C C_ (Idl` R) /\ A.i e. C A.j e. C (i C_ j \/ j C_ i))) /\ (k e. C /\ x e. k)) -> (A.y e. U.C(x(1st` R)y) e. U.C /\ A.z e. ran (1st` R)((z(2nd` R)x) e. U.C /\ (x(2nd` R)z) e. U.C)))
111	110	exp32 408	. . . . . 6 |- ((R e. Ring /\ (C =/= (/) /\ C C_ (Idl` R) /\ A.i e. C A.j e. C (i C_ j \/ j C_ i))) -> (k e. C -> (x e. k -> (A.y e. U.C(x(1st` R)y) e. U.C /\ A.z e. ran (1st` R)((z(2nd` R)x) e. U.C /\ (x(2nd` R)z) e. U.C)))))
112	111	r19.23adv 2215	. . . . 5 |- ((R e. Ring /\ (C =/= (/) /\ C C_ (Idl` R) /\ A.i e. C A.j e. C (i C_ j \/ j C_ i))) -> (E.k e. C x e. k -> (A.y e. U.C(x(1st` R)y) e. U.C /\ A.z e. ran (1st` R)((z(2nd` R)x) e. U.C /\ (x(2nd` R)z) e. U.C))))
113		eluni2 3181	. . . . 5 |- (x e. U.C <-> E.k e. C x e. k)
114	112, 113	syl5ib 223	. . . 4 |- ((R e. Ring /\ (C =/= (/) /\ C C_ (Idl` R) /\ A.i e. C A.j e. C (i C_ j \/ j C_ i))) -> (x e. U.C -> (A.y e. U.C(x(1st` R)y) e. U.C /\ A.z e. ran (1st` R)((z(2nd` R)x) e. U.C /\ (x(2nd` R)z) e. U.C))))
115	114	r19.21aiv 2175	. . 3 |- ((R e. Ring /\ (C =/= (/) /\ C C_ (Idl` R) /\ A.i e. C A.j e. C (i C_ j \/ j C_ i))) -> A.x e. U.C(A.y e. U.C(x(1st` R)y) e. U.C /\ A.z e. ran (1st` R)((z(2nd` R)x) e. U.C /\ (x(2nd` R)z) e. U.C)))
116	11, 23, 115	3jca 1050	. 2 |- ((R e. Ring /\ (C =/= (/) /\ C C_ (Idl` R) /\ A.i e. C A.j e. C (i C_ j \/ j C_ i))) -> (U.C C_ ran (1st` R) /\ (Id` (1st` R)) e. U.C /\ A.x e. U.C(A.y e. U.C(x(1st` R)y) e. U.C /\ A.z e. ran (1st` R)((z(2nd` R)x) e. U.C /\ (x(2nd` R)z) e. U.C))))
117	1, 88, 2, 13	isidl 16162	. . 3 |- (R e. Ring -> (U.C e. (Idl` R) <-> (U.C C_ ran (1st` R) /\ (Id` (1st` R)) e. U.C /\ A.x e. U.C(A.y e. U.C(x(1st` R)y) e. U.C /\ A.z e. ran (1st` R)((z(2nd` R)x) e. U.C /\ (x(2nd` R)z) e. U.C)))))
118	117	adantr 425	. 2 |- ((R e. Ring /\ (C =/= (/) /\ C C_ (Idl` R) /\ A.i e. C A.j e. C (i C_ j \/ j C_ i))) -> (U.C e. (Idl` R) <-> (U.C C_ ran (1st` R) /\ (Id` (1st` R)) e. U.C /\ A.x e. U.C(A.y e. U.C(x(1st` R)y) e. U.C /\ A.z e. ran (1st` R)((z(2nd` R)x) e. U.C /\ (x(2nd` R)z) e. U.C)))))
119	116, 118	mpbird 213	1 |- ((R e. Ring /\ (C =/= (/) /\ C C_ (Idl` R) /\ A.i e. C A.j e. C (i C_ j \/ j C_ i))) -> U.C e. (Idl` R))

Syntax hints:   -> wi 3   <-> wb 163   \/ wo 239   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300   =/= wne 2017  A.wral 2105  E.wrex 2106   C_ wss 2593  (/)c0 2875  U.cuni 3177  ran crn 3987  ` cfv 3998  (class class class)co 4884  1stc1st 5018  2ndc2nd 5019  Idcgi 9312  Ringcring 9463  Idlcidl 16155

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-rab 2112  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fv 4014  df-opr 4886  df-idl 16158

Copyright terms: Public domain