Theorem unichnidl 36899

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

Assertion

Ref	Expression
unichnidl	⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → ∪ 𝐶 ∈ (Idl‘𝑅))

Distinct variable groups:   𝑅,𝑖   𝐶,𝑖,𝑗

Allowed substitution hint:   𝑅(𝑗)

Proof of Theorem unichnidl

Dummy variables 𝑘 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfss3 3971	. . . . 5 ⊢ (𝐶 ⊆ (Idl‘𝑅) ↔ ∀𝑖 ∈ 𝐶 𝑖 ∈ (Idl‘𝑅))
2		eqid 2733	. . . . . . . . 9 ⊢ (1st ‘𝑅) = (1st ‘𝑅)
3		eqid 2733	. . . . . . . . 9 ⊢ ran (1st ‘𝑅) = ran (1st ‘𝑅)
4	2, 3	idlss 36884	. . . . . . . 8 ⊢ ((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) → 𝑖 ⊆ ran (1st ‘𝑅))
5	4	ex 414	. . . . . . 7 ⊢ (𝑅 ∈ RingOps → (𝑖 ∈ (Idl‘𝑅) → 𝑖 ⊆ ran (1st ‘𝑅)))
6	5	ralimdv 3170	. . . . . 6 ⊢ (𝑅 ∈ RingOps → (∀𝑖 ∈ 𝐶 𝑖 ∈ (Idl‘𝑅) → ∀𝑖 ∈ 𝐶 𝑖 ⊆ ran (1st ‘𝑅)))
7	6	imp 408	. . . . 5 ⊢ ((𝑅 ∈ RingOps ∧ ∀𝑖 ∈ 𝐶 𝑖 ∈ (Idl‘𝑅)) → ∀𝑖 ∈ 𝐶 𝑖 ⊆ ran (1st ‘𝑅))
8	1, 7	sylan2b 595	. . . 4 ⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∀𝑖 ∈ 𝐶 𝑖 ⊆ ran (1st ‘𝑅))
9		unissb 4944	. . . 4 ⊢ (∪ 𝐶 ⊆ ran (1st ‘𝑅) ↔ ∀𝑖 ∈ 𝐶 𝑖 ⊆ ran (1st ‘𝑅))
10	8, 9	sylibr 233	. . 3 ⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∪ 𝐶 ⊆ ran (1st ‘𝑅))
11	10	3ad2antr2 1190	. 2 ⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → ∪ 𝐶 ⊆ ran (1st ‘𝑅))
12		eqid 2733	. . . . . . . . . . 11 ⊢ (GId‘(1st ‘𝑅)) = (GId‘(1st ‘𝑅))
13	2, 12	idl0cl 36886	. . . . . . . . . 10 ⊢ ((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) → (GId‘(1st ‘𝑅)) ∈ 𝑖)
14	13	ex 414	. . . . . . . . 9 ⊢ (𝑅 ∈ RingOps → (𝑖 ∈ (Idl‘𝑅) → (GId‘(1st ‘𝑅)) ∈ 𝑖))
15	14	ralimdv 3170	. . . . . . . 8 ⊢ (𝑅 ∈ RingOps → (∀𝑖 ∈ 𝐶 𝑖 ∈ (Idl‘𝑅) → ∀𝑖 ∈ 𝐶 (GId‘(1st ‘𝑅)) ∈ 𝑖))
16	15	imp 408	. . . . . . 7 ⊢ ((𝑅 ∈ RingOps ∧ ∀𝑖 ∈ 𝐶 𝑖 ∈ (Idl‘𝑅)) → ∀𝑖 ∈ 𝐶 (GId‘(1st ‘𝑅)) ∈ 𝑖)
17	1, 16	sylan2b 595	. . . . . 6 ⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∀𝑖 ∈ 𝐶 (GId‘(1st ‘𝑅)) ∈ 𝑖)
18		r19.2z 4495	. . . . . 6 ⊢ ((𝐶 ≠ ∅ ∧ ∀𝑖 ∈ 𝐶 (GId‘(1st ‘𝑅)) ∈ 𝑖) → ∃𝑖 ∈ 𝐶 (GId‘(1st ‘𝑅)) ∈ 𝑖)
19	17, 18	sylan2 594	. . . . 5 ⊢ ((𝐶 ≠ ∅ ∧ (𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅))) → ∃𝑖 ∈ 𝐶 (GId‘(1st ‘𝑅)) ∈ 𝑖)
20	19	an12s 648	. . . 4 ⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅))) → ∃𝑖 ∈ 𝐶 (GId‘(1st ‘𝑅)) ∈ 𝑖)
21		eluni2 4913	. . . 4 ⊢ ((GId‘(1st ‘𝑅)) ∈ ∪ 𝐶 ↔ ∃𝑖 ∈ 𝐶 (GId‘(1st ‘𝑅)) ∈ 𝑖)
22	20, 21	sylibr 233	. . 3 ⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅))) → (GId‘(1st ‘𝑅)) ∈ ∪ 𝐶)
23	22	3adantr3 1172	. 2 ⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → (GId‘(1st ‘𝑅)) ∈ ∪ 𝐶)
24		eluni2 4913	. . . 4 ⊢ (𝑥 ∈ ∪ 𝐶 ↔ ∃𝑘 ∈ 𝐶 𝑥 ∈ 𝑘)
25		sseq1 4008	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑘 → (𝑖 ⊆ 𝑗 ↔ 𝑘 ⊆ 𝑗))
26		sseq2 4009	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑘 → (𝑗 ⊆ 𝑖 ↔ 𝑗 ⊆ 𝑘))
27	25, 26	orbi12d 918	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑘 → ((𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖) ↔ (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)))
28	27	ralbidv 3178	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑘 → (∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖) ↔ ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)))
29	28	rspcv 3609	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ 𝐶 → (∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖) → ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)))
30	29	adantr 482	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘) → (∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖) → ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)))
31	30	ad2antlr 726	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) → (∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖) → ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)))
32	31	imp 408	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖)) → ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘))
33		eluni2 4913	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ∪ 𝐶 ↔ ∃𝑖 ∈ 𝐶 𝑦 ∈ 𝑖)
34		sseq2 4009	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝑖 → (𝑘 ⊆ 𝑗 ↔ 𝑘 ⊆ 𝑖))
35		sseq1 4008	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝑖 → (𝑗 ⊆ 𝑘 ↔ 𝑖 ⊆ 𝑘))
36	34, 35	orbi12d 918	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑖 → ((𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘) ↔ (𝑘 ⊆ 𝑖 ∨ 𝑖 ⊆ 𝑘)))
37	36	rspcv 3609	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 ∈ 𝐶 → (∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘) → (𝑘 ⊆ 𝑖 ∨ 𝑖 ⊆ 𝑘)))
38	37	ad2antrl 727	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖)) → (∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘) → (𝑘 ⊆ 𝑖 ∨ 𝑖 ⊆ 𝑘)))
39	38	imp 408	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖)) ∧ ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)) → (𝑘 ⊆ 𝑖 ∨ 𝑖 ⊆ 𝑘))
40		ssel2 3978	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ⊆ 𝑖 ∧ 𝑥 ∈ 𝑘) → 𝑥 ∈ 𝑖)
41	40	ancoms 460	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ 𝑘 ∧ 𝑘 ⊆ 𝑖) → 𝑥 ∈ 𝑖)
42	41	adantll 713	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘) ∧ 𝑘 ⊆ 𝑖) → 𝑥 ∈ 𝑖)
43		ssel2 3978	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐶 ⊆ (Idl‘𝑅) ∧ 𝑖 ∈ 𝐶) → 𝑖 ∈ (Idl‘𝑅))
44	2	idladdcl 36887	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ (𝑥 ∈ 𝑖 ∧ 𝑦 ∈ 𝑖)) → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑖)
45	44	ancom2s 649	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ (𝑦 ∈ 𝑖 ∧ 𝑥 ∈ 𝑖)) → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑖)
46	45	expr 458	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ 𝑦 ∈ 𝑖) → (𝑥 ∈ 𝑖 → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑖))
47	46	an32s 651	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑅 ∈ RingOps ∧ 𝑦 ∈ 𝑖) ∧ 𝑖 ∈ (Idl‘𝑅)) → (𝑥 ∈ 𝑖 → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑖))
48	43, 47	sylan2 594	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑅 ∈ RingOps ∧ 𝑦 ∈ 𝑖) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑖 ∈ 𝐶)) → (𝑥 ∈ 𝑖 → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑖))
49	48	an42s 660	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖)) → (𝑥 ∈ 𝑖 → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑖))
50	49	anasss 468	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖))) → (𝑥 ∈ 𝑖 → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑖))
51	50	imp 408	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖))) ∧ 𝑥 ∈ 𝑖) → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑖)
52		simprl 770	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖)) → 𝑖 ∈ 𝐶)
53	52	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖))) ∧ 𝑥 ∈ 𝑖) → 𝑖 ∈ 𝐶)
54		elunii 4914	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥(1st ‘𝑅)𝑦) ∈ 𝑖 ∧ 𝑖 ∈ 𝐶) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
55	51, 53, 54	syl2anc 585	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖))) ∧ 𝑥 ∈ 𝑖) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
56	42, 55	sylan2 594	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖))) ∧ ((𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘) ∧ 𝑘 ⊆ 𝑖)) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
57	56	expr 458	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖))) ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) → (𝑘 ⊆ 𝑖 → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶))
58	57	an32s 651	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖))) → (𝑘 ⊆ 𝑖 → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶))
59	58	anassrs 469	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖)) → (𝑘 ⊆ 𝑖 → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶))
60	59	imp 408	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖)) ∧ 𝑘 ⊆ 𝑖) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
61		ssel2 3978	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ⊆ 𝑘 ∧ 𝑦 ∈ 𝑖) → 𝑦 ∈ 𝑘)
62	61	ancoms 460	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ 𝑖 ∧ 𝑖 ⊆ 𝑘) → 𝑦 ∈ 𝑘)
63	62	adantll 713	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖) ∧ 𝑖 ⊆ 𝑘) → 𝑦 ∈ 𝑘)
64		ssel2 3978	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘 ∈ 𝐶) → 𝑘 ∈ (Idl‘𝑅))
65	2	idladdcl 36887	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑅 ∈ RingOps ∧ 𝑘 ∈ (Idl‘𝑅)) ∧ (𝑥 ∈ 𝑘 ∧ 𝑦 ∈ 𝑘)) → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑘)
66	65	expr 458	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑅 ∈ RingOps ∧ 𝑘 ∈ (Idl‘𝑅)) ∧ 𝑥 ∈ 𝑘) → (𝑦 ∈ 𝑘 → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑘))
67	66	an32s 651	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ 𝑘 ∈ (Idl‘𝑅)) → (𝑦 ∈ 𝑘 → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑘))
68	64, 67	sylan2 594	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘 ∈ 𝐶)) → (𝑦 ∈ 𝑘 → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑘))
69	68	an42s 660	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) → (𝑦 ∈ 𝑘 → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑘))
70	69	an32s 651	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) → (𝑦 ∈ 𝑘 → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑘))
71	70	imp 408	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑦 ∈ 𝑘) → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑘)
72		simprl 770	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) → 𝑘 ∈ 𝐶)
73	72	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑦 ∈ 𝑘) → 𝑘 ∈ 𝐶)
74		elunii 4914	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥(1st ‘𝑅)𝑦) ∈ 𝑘 ∧ 𝑘 ∈ 𝐶) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
75	71, 73, 74	syl2anc 585	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑦 ∈ 𝑘) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
76	63, 75	sylan2 594	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ((𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖) ∧ 𝑖 ⊆ 𝑘)) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
77	76	anassrs 469	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖)) ∧ 𝑖 ⊆ 𝑘) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
78	60, 77	jaodan 957	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖)) ∧ (𝑘 ⊆ 𝑖 ∨ 𝑖 ⊆ 𝑘)) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
79	39, 78	syldan 592	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖)) ∧ ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
80	79	an32s 651	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖)) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
81	80	rexlimdvaa 3157	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)) → (∃𝑖 ∈ 𝐶 𝑦 ∈ 𝑖 → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶))
82	33, 81	biimtrid 241	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)) → (𝑦 ∈ ∪ 𝐶 → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶))
83	82	ralrimiv 3146	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)) → ∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
84	32, 83	syldan 592	. . . . . . . . 9 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖)) → ∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
85	84	anasss 468	. . . . . . . 8 ⊢ (((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → ∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
86	85	3adantr1 1170	. . . . . . 7 ⊢ (((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → ∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
87	86	an32s 651	. . . . . 6 ⊢ (((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) → ∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
88		eqid 2733	. . . . . . . . . . . . . . . . . 18 ⊢ (2nd ‘𝑅) = (2nd ‘𝑅)
89	2, 88, 3	idllmulcl 36888	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ RingOps ∧ 𝑘 ∈ (Idl‘𝑅)) ∧ (𝑥 ∈ 𝑘 ∧ 𝑧 ∈ ran (1st ‘𝑅))) → (𝑧(2nd ‘𝑅)𝑥) ∈ 𝑘)
90	89	exp43 438	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ RingOps → (𝑘 ∈ (Idl‘𝑅) → (𝑥 ∈ 𝑘 → (𝑧 ∈ ran (1st ‘𝑅) → (𝑧(2nd ‘𝑅)𝑥) ∈ 𝑘))))
91	90	com23 86	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ RingOps → (𝑥 ∈ 𝑘 → (𝑘 ∈ (Idl‘𝑅) → (𝑧 ∈ ran (1st ‘𝑅) → (𝑧(2nd ‘𝑅)𝑥) ∈ 𝑘))))
92	91	imp41 427	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ 𝑘 ∈ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝑧(2nd ‘𝑅)𝑥) ∈ 𝑘)
93	64, 92	sylanl2 680	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘 ∈ 𝐶)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝑧(2nd ‘𝑅)𝑥) ∈ 𝑘)
94		simplrr 777	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘 ∈ 𝐶)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → 𝑘 ∈ 𝐶)
95		elunii 4914	. . . . . . . . . . . . 13 ⊢ (((𝑧(2nd ‘𝑅)𝑥) ∈ 𝑘 ∧ 𝑘 ∈ 𝐶) → (𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶)
96	93, 94, 95	syl2anc 585	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘 ∈ 𝐶)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶)
97	2, 88, 3	idlrmulcl 36889	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ RingOps ∧ 𝑘 ∈ (Idl‘𝑅)) ∧ (𝑥 ∈ 𝑘 ∧ 𝑧 ∈ ran (1st ‘𝑅))) → (𝑥(2nd ‘𝑅)𝑧) ∈ 𝑘)
98	97	exp43 438	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ RingOps → (𝑘 ∈ (Idl‘𝑅) → (𝑥 ∈ 𝑘 → (𝑧 ∈ ran (1st ‘𝑅) → (𝑥(2nd ‘𝑅)𝑧) ∈ 𝑘))))
99	98	com23 86	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ RingOps → (𝑥 ∈ 𝑘 → (𝑘 ∈ (Idl‘𝑅) → (𝑧 ∈ ran (1st ‘𝑅) → (𝑥(2nd ‘𝑅)𝑧) ∈ 𝑘))))
100	99	imp41 427	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ 𝑘 ∈ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝑥(2nd ‘𝑅)𝑧) ∈ 𝑘)
101	64, 100	sylanl2 680	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘 ∈ 𝐶)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝑥(2nd ‘𝑅)𝑧) ∈ 𝑘)
102		elunii 4914	. . . . . . . . . . . . 13 ⊢ (((𝑥(2nd ‘𝑅)𝑧) ∈ 𝑘 ∧ 𝑘 ∈ 𝐶) → (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶)
103	101, 94, 102	syl2anc 585	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘 ∈ 𝐶)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶)
104	96, 103	jca 513	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘 ∈ 𝐶)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → ((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶))
105	104	ralrimiva 3147	. . . . . . . . . 10 ⊢ (((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘 ∈ 𝐶)) → ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶))
106	105	an42s 660	. . . . . . . . 9 ⊢ (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) → ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶))
107	106	an32s 651	. . . . . . . 8 ⊢ (((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶))
108	107	3ad2antr2 1190	. . . . . . 7 ⊢ (((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶))
109	108	an32s 651	. . . . . 6 ⊢ (((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) → ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶))
110	87, 109	jca 513	. . . . 5 ⊢ (((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) → (∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶 ∧ ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶)))
111	110	rexlimdvaa 3157	. . . 4 ⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → (∃𝑘 ∈ 𝐶 𝑥 ∈ 𝑘 → (∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶 ∧ ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶))))
112	24, 111	biimtrid 241	. . 3 ⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → (𝑥 ∈ ∪ 𝐶 → (∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶 ∧ ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶))))
113	112	ralrimiv 3146	. 2 ⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → ∀𝑥 ∈ ∪ 𝐶(∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶 ∧ ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶)))
114	2, 88, 3, 12	isidl 36882	. . 3 ⊢ (𝑅 ∈ RingOps → (∪ 𝐶 ∈ (Idl‘𝑅) ↔ (∪ 𝐶 ⊆ ran (1st ‘𝑅) ∧ (GId‘(1st ‘𝑅)) ∈ ∪ 𝐶 ∧ ∀𝑥 ∈ ∪ 𝐶(∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶 ∧ ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶)))))
115	114	adantr 482	. 2 ⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → (∪ 𝐶 ∈ (Idl‘𝑅) ↔ (∪ 𝐶 ⊆ ran (1st ‘𝑅) ∧ (GId‘(1st ‘𝑅)) ∈ ∪ 𝐶 ∧ ∀𝑥 ∈ ∪ 𝐶(∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶 ∧ ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶)))))
116	11, 23, 113, 115	mpbir3and 1343	1 ⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → ∪ 𝐶 ∈ (Idl‘𝑅))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   ∧ w3a 1088   ∈ wcel 2107   ≠ wne 2941  ∀wral 3062  ∃wrex 3071   ⊆ wss 3949  ∅c0 4323  ∪ cuni 4909  ran crn 5678  ‘cfv 6544  (class class class)co 7409  1^st c1st 7973  2^nd c2nd 7974  GIdcgi 29743  RingOpscrngo 36762  Idlcidl 36875

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-iota 6496  df-fun 6546  df-fv 6552  df-ov 7412  df-idl 36878

This theorem is referenced by: (None)