Theorem unichnidl 35926

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 3888	. . . . 5 ⊢ (𝐶 ⊆ (Idl‘𝑅) ↔ ∀𝑖 ∈ 𝐶 𝑖 ∈ (Idl‘𝑅))
2		eqid 2737	. . . . . . . . 9 ⊢ (1st ‘𝑅) = (1st ‘𝑅)
3		eqid 2737	. . . . . . . . 9 ⊢ ran (1st ‘𝑅) = ran (1st ‘𝑅)
4	2, 3	idlss 35911	. . . . . . . 8 ⊢ ((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) → 𝑖 ⊆ ran (1st ‘𝑅))
5	4	ex 416	. . . . . . 7 ⊢ (𝑅 ∈ RingOps → (𝑖 ∈ (Idl‘𝑅) → 𝑖 ⊆ ran (1st ‘𝑅)))
6	5	ralimdv 3101	. . . . . 6 ⊢ (𝑅 ∈ RingOps → (∀𝑖 ∈ 𝐶 𝑖 ∈ (Idl‘𝑅) → ∀𝑖 ∈ 𝐶 𝑖 ⊆ ran (1st ‘𝑅)))
7	6	imp 410	. . . . 5 ⊢ ((𝑅 ∈ RingOps ∧ ∀𝑖 ∈ 𝐶 𝑖 ∈ (Idl‘𝑅)) → ∀𝑖 ∈ 𝐶 𝑖 ⊆ ran (1st ‘𝑅))
8	1, 7	sylan2b 597	. . . 4 ⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∀𝑖 ∈ 𝐶 𝑖 ⊆ ran (1st ‘𝑅))
9		unissb 4853	. . . 4 ⊢ (∪ 𝐶 ⊆ ran (1st ‘𝑅) ↔ ∀𝑖 ∈ 𝐶 𝑖 ⊆ ran (1st ‘𝑅))
10	8, 9	sylibr 237	. . 3 ⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∪ 𝐶 ⊆ ran (1st ‘𝑅))
11	10	3ad2antr2 1191	. 2 ⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → ∪ 𝐶 ⊆ ran (1st ‘𝑅))
12		eqid 2737	. . . . . . . . . . 11 ⊢ (GId‘(1st ‘𝑅)) = (GId‘(1st ‘𝑅))
13	2, 12	idl0cl 35913	. . . . . . . . . 10 ⊢ ((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) → (GId‘(1st ‘𝑅)) ∈ 𝑖)
14	13	ex 416	. . . . . . . . 9 ⊢ (𝑅 ∈ RingOps → (𝑖 ∈ (Idl‘𝑅) → (GId‘(1st ‘𝑅)) ∈ 𝑖))
15	14	ralimdv 3101	. . . . . . . 8 ⊢ (𝑅 ∈ RingOps → (∀𝑖 ∈ 𝐶 𝑖 ∈ (Idl‘𝑅) → ∀𝑖 ∈ 𝐶 (GId‘(1st ‘𝑅)) ∈ 𝑖))
16	15	imp 410	. . . . . . 7 ⊢ ((𝑅 ∈ RingOps ∧ ∀𝑖 ∈ 𝐶 𝑖 ∈ (Idl‘𝑅)) → ∀𝑖 ∈ 𝐶 (GId‘(1st ‘𝑅)) ∈ 𝑖)
17	1, 16	sylan2b 597	. . . . . 6 ⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∀𝑖 ∈ 𝐶 (GId‘(1st ‘𝑅)) ∈ 𝑖)
18		r19.2z 4406	. . . . . 6 ⊢ ((𝐶 ≠ ∅ ∧ ∀𝑖 ∈ 𝐶 (GId‘(1st ‘𝑅)) ∈ 𝑖) → ∃𝑖 ∈ 𝐶 (GId‘(1st ‘𝑅)) ∈ 𝑖)
19	17, 18	sylan2 596	. . . . 5 ⊢ ((𝐶 ≠ ∅ ∧ (𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅))) → ∃𝑖 ∈ 𝐶 (GId‘(1st ‘𝑅)) ∈ 𝑖)
20	19	an12s 649	. . . 4 ⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅))) → ∃𝑖 ∈ 𝐶 (GId‘(1st ‘𝑅)) ∈ 𝑖)
21		eluni2 4823	. . . 4 ⊢ ((GId‘(1st ‘𝑅)) ∈ ∪ 𝐶 ↔ ∃𝑖 ∈ 𝐶 (GId‘(1st ‘𝑅)) ∈ 𝑖)
22	20, 21	sylibr 237	. . 3 ⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅))) → (GId‘(1st ‘𝑅)) ∈ ∪ 𝐶)
23	22	3adantr3 1173	. 2 ⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → (GId‘(1st ‘𝑅)) ∈ ∪ 𝐶)
24		eluni2 4823	. . . 4 ⊢ (𝑥 ∈ ∪ 𝐶 ↔ ∃𝑘 ∈ 𝐶 𝑥 ∈ 𝑘)
25		sseq1 3926	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑘 → (𝑖 ⊆ 𝑗 ↔ 𝑘 ⊆ 𝑗))
26		sseq2 3927	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑘 → (𝑗 ⊆ 𝑖 ↔ 𝑗 ⊆ 𝑘))
27	25, 26	orbi12d 919	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑘 → ((𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖) ↔ (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)))
28	27	ralbidv 3118	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑘 → (∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖) ↔ ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)))
29	28	rspcv 3532	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ 𝐶 → (∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖) → ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)))
30	29	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘) → (∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖) → ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)))
31	30	ad2antlr 727	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) → (∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖) → ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)))
32	31	imp 410	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖)) → ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘))
33		eluni2 4823	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ∪ 𝐶 ↔ ∃𝑖 ∈ 𝐶 𝑦 ∈ 𝑖)
34		sseq2 3927	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝑖 → (𝑘 ⊆ 𝑗 ↔ 𝑘 ⊆ 𝑖))
35		sseq1 3926	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝑖 → (𝑗 ⊆ 𝑘 ↔ 𝑖 ⊆ 𝑘))
36	34, 35	orbi12d 919	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑖 → ((𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘) ↔ (𝑘 ⊆ 𝑖 ∨ 𝑖 ⊆ 𝑘)))
37	36	rspcv 3532	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 ∈ 𝐶 → (∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘) → (𝑘 ⊆ 𝑖 ∨ 𝑖 ⊆ 𝑘)))
38	37	ad2antrl 728	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖)) → (∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘) → (𝑘 ⊆ 𝑖 ∨ 𝑖 ⊆ 𝑘)))
39	38	imp 410	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖)) ∧ ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)) → (𝑘 ⊆ 𝑖 ∨ 𝑖 ⊆ 𝑘))
40		ssel2 3895	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ⊆ 𝑖 ∧ 𝑥 ∈ 𝑘) → 𝑥 ∈ 𝑖)
41	40	ancoms 462	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ 𝑘 ∧ 𝑘 ⊆ 𝑖) → 𝑥 ∈ 𝑖)
42	41	adantll 714	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘) ∧ 𝑘 ⊆ 𝑖) → 𝑥 ∈ 𝑖)
43		ssel2 3895	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐶 ⊆ (Idl‘𝑅) ∧ 𝑖 ∈ 𝐶) → 𝑖 ∈ (Idl‘𝑅))
44	2	idladdcl 35914	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ (𝑥 ∈ 𝑖 ∧ 𝑦 ∈ 𝑖)) → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑖)
45	44	ancom2s 650	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ (𝑦 ∈ 𝑖 ∧ 𝑥 ∈ 𝑖)) → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑖)
46	45	expr 460	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ 𝑦 ∈ 𝑖) → (𝑥 ∈ 𝑖 → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑖))
47	46	an32s 652	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑅 ∈ RingOps ∧ 𝑦 ∈ 𝑖) ∧ 𝑖 ∈ (Idl‘𝑅)) → (𝑥 ∈ 𝑖 → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑖))
48	43, 47	sylan2 596	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑅 ∈ RingOps ∧ 𝑦 ∈ 𝑖) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑖 ∈ 𝐶)) → (𝑥 ∈ 𝑖 → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑖))
49	48	an42s 661	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖)) → (𝑥 ∈ 𝑖 → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑖))
50	49	anasss 470	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖))) → (𝑥 ∈ 𝑖 → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑖))
51	50	imp 410	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖))) ∧ 𝑥 ∈ 𝑖) → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑖)
52		simprl 771	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖)) → 𝑖 ∈ 𝐶)
53	52	ad2antlr 727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖))) ∧ 𝑥 ∈ 𝑖) → 𝑖 ∈ 𝐶)
54		elunii 4824	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥(1st ‘𝑅)𝑦) ∈ 𝑖 ∧ 𝑖 ∈ 𝐶) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
55	51, 53, 54	syl2anc 587	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖))) ∧ 𝑥 ∈ 𝑖) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
56	42, 55	sylan2 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖))) ∧ ((𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘) ∧ 𝑘 ⊆ 𝑖)) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
57	56	expr 460	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖))) ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) → (𝑘 ⊆ 𝑖 → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶))
58	57	an32s 652	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖))) → (𝑘 ⊆ 𝑖 → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶))
59	58	anassrs 471	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖)) → (𝑘 ⊆ 𝑖 → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶))
60	59	imp 410	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖)) ∧ 𝑘 ⊆ 𝑖) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
61		ssel2 3895	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ⊆ 𝑘 ∧ 𝑦 ∈ 𝑖) → 𝑦 ∈ 𝑘)
62	61	ancoms 462	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ 𝑖 ∧ 𝑖 ⊆ 𝑘) → 𝑦 ∈ 𝑘)
63	62	adantll 714	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖) ∧ 𝑖 ⊆ 𝑘) → 𝑦 ∈ 𝑘)
64		ssel2 3895	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘 ∈ 𝐶) → 𝑘 ∈ (Idl‘𝑅))
65	2	idladdcl 35914	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑅 ∈ RingOps ∧ 𝑘 ∈ (Idl‘𝑅)) ∧ (𝑥 ∈ 𝑘 ∧ 𝑦 ∈ 𝑘)) → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑘)
66	65	expr 460	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑅 ∈ RingOps ∧ 𝑘 ∈ (Idl‘𝑅)) ∧ 𝑥 ∈ 𝑘) → (𝑦 ∈ 𝑘 → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑘))
67	66	an32s 652	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ 𝑘 ∈ (Idl‘𝑅)) → (𝑦 ∈ 𝑘 → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑘))
68	64, 67	sylan2 596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘 ∈ 𝐶)) → (𝑦 ∈ 𝑘 → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑘))
69	68	an42s 661	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) → (𝑦 ∈ 𝑘 → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑘))
70	69	an32s 652	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) → (𝑦 ∈ 𝑘 → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑘))
71	70	imp 410	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑦 ∈ 𝑘) → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑘)
72		simprl 771	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) → 𝑘 ∈ 𝐶)
73	72	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑦 ∈ 𝑘) → 𝑘 ∈ 𝐶)
74		elunii 4824	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥(1st ‘𝑅)𝑦) ∈ 𝑘 ∧ 𝑘 ∈ 𝐶) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
75	71, 73, 74	syl2anc 587	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑦 ∈ 𝑘) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
76	63, 75	sylan2 596	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ((𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖) ∧ 𝑖 ⊆ 𝑘)) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
77	76	anassrs 471	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖)) ∧ 𝑖 ⊆ 𝑘) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
78	60, 77	jaodan 958	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖)) ∧ (𝑘 ⊆ 𝑖 ∨ 𝑖 ⊆ 𝑘)) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
79	39, 78	syldan 594	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖)) ∧ ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
80	79	an32s 652	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖)) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
81	80	rexlimdvaa 3204	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)) → (∃𝑖 ∈ 𝐶 𝑦 ∈ 𝑖 → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶))
82	33, 81	syl5bi 245	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)) → (𝑦 ∈ ∪ 𝐶 → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶))
83	82	ralrimiv 3104	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)) → ∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
84	32, 83	syldan 594	. . . . . . . . 9 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖)) → ∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
85	84	anasss 470	. . . . . . . 8 ⊢ (((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → ∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
86	85	3adantr1 1171	. . . . . . 7 ⊢ (((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → ∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
87	86	an32s 652	. . . . . 6 ⊢ (((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) → ∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
88		eqid 2737	. . . . . . . . . . . . . . . . . 18 ⊢ (2nd ‘𝑅) = (2nd ‘𝑅)
89	2, 88, 3	idllmulcl 35915	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ RingOps ∧ 𝑘 ∈ (Idl‘𝑅)) ∧ (𝑥 ∈ 𝑘 ∧ 𝑧 ∈ ran (1st ‘𝑅))) → (𝑧(2nd ‘𝑅)𝑥) ∈ 𝑘)
90	89	exp43 440	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ RingOps → (𝑘 ∈ (Idl‘𝑅) → (𝑥 ∈ 𝑘 → (𝑧 ∈ ran (1st ‘𝑅) → (𝑧(2nd ‘𝑅)𝑥) ∈ 𝑘))))
91	90	com23 86	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ RingOps → (𝑥 ∈ 𝑘 → (𝑘 ∈ (Idl‘𝑅) → (𝑧 ∈ ran (1st ‘𝑅) → (𝑧(2nd ‘𝑅)𝑥) ∈ 𝑘))))
92	91	imp41 429	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ 𝑘 ∈ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝑧(2nd ‘𝑅)𝑥) ∈ 𝑘)
93	64, 92	sylanl2 681	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘 ∈ 𝐶)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝑧(2nd ‘𝑅)𝑥) ∈ 𝑘)
94		simplrr 778	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘 ∈ 𝐶)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → 𝑘 ∈ 𝐶)
95		elunii 4824	. . . . . . . . . . . . 13 ⊢ (((𝑧(2nd ‘𝑅)𝑥) ∈ 𝑘 ∧ 𝑘 ∈ 𝐶) → (𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶)
96	93, 94, 95	syl2anc 587	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘 ∈ 𝐶)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶)
97	2, 88, 3	idlrmulcl 35916	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ RingOps ∧ 𝑘 ∈ (Idl‘𝑅)) ∧ (𝑥 ∈ 𝑘 ∧ 𝑧 ∈ ran (1st ‘𝑅))) → (𝑥(2nd ‘𝑅)𝑧) ∈ 𝑘)
98	97	exp43 440	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ RingOps → (𝑘 ∈ (Idl‘𝑅) → (𝑥 ∈ 𝑘 → (𝑧 ∈ ran (1st ‘𝑅) → (𝑥(2nd ‘𝑅)𝑧) ∈ 𝑘))))
99	98	com23 86	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ RingOps → (𝑥 ∈ 𝑘 → (𝑘 ∈ (Idl‘𝑅) → (𝑧 ∈ ran (1st ‘𝑅) → (𝑥(2nd ‘𝑅)𝑧) ∈ 𝑘))))
100	99	imp41 429	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ 𝑘 ∈ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝑥(2nd ‘𝑅)𝑧) ∈ 𝑘)
101	64, 100	sylanl2 681	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘 ∈ 𝐶)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝑥(2nd ‘𝑅)𝑧) ∈ 𝑘)
102		elunii 4824	. . . . . . . . . . . . 13 ⊢ (((𝑥(2nd ‘𝑅)𝑧) ∈ 𝑘 ∧ 𝑘 ∈ 𝐶) → (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶)
103	101, 94, 102	syl2anc 587	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘 ∈ 𝐶)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶)
104	96, 103	jca 515	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘 ∈ 𝐶)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → ((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶))
105	104	ralrimiva 3105	. . . . . . . . . 10 ⊢ (((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘 ∈ 𝐶)) → ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶))
106	105	an42s 661	. . . . . . . . 9 ⊢ (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) → ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶))
107	106	an32s 652	. . . . . . . 8 ⊢ (((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶))
108	107	3ad2antr2 1191	. . . . . . 7 ⊢ (((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶))
109	108	an32s 652	. . . . . 6 ⊢ (((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) → ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶))
110	87, 109	jca 515	. . . . 5 ⊢ (((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) → (∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶 ∧ ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶)))
111	110	rexlimdvaa 3204	. . . 4 ⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → (∃𝑘 ∈ 𝐶 𝑥 ∈ 𝑘 → (∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶 ∧ ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶))))
112	24, 111	syl5bi 245	. . 3 ⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → (𝑥 ∈ ∪ 𝐶 → (∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶 ∧ ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶))))
113	112	ralrimiv 3104	. 2 ⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → ∀𝑥 ∈ ∪ 𝐶(∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶 ∧ ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶)))
114	2, 88, 3, 12	isidl 35909	. . 3 ⊢ (𝑅 ∈ RingOps → (∪ 𝐶 ∈ (Idl‘𝑅) ↔ (∪ 𝐶 ⊆ ran (1st ‘𝑅) ∧ (GId‘(1st ‘𝑅)) ∈ ∪ 𝐶 ∧ ∀𝑥 ∈ ∪ 𝐶(∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶 ∧ ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶)))))
115	114	adantr 484	. 2 ⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → (∪ 𝐶 ∈ (Idl‘𝑅) ↔ (∪ 𝐶 ⊆ ran (1st ‘𝑅) ∧ (GId‘(1st ‘𝑅)) ∈ ∪ 𝐶 ∧ ∀𝑥 ∈ ∪ 𝐶(∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶 ∧ ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶)))))
116	11, 23, 113, 115	mpbir3and 1344	1 ⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → ∪ 𝐶 ∈ (Idl‘𝑅))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 847   ∧ w3a 1089   ∈ wcel 2110   ≠ wne 2940  ∀wral 3061  ∃wrex 3062   ⊆ wss 3866  ∅c0 4237  ∪ cuni 4819  ran crn 5552  ‘cfv 6380  (class class class)co 7213  1^st c1st 7759  2^nd c2nd 7760  GIdcgi 28571  RingOpscrngo 35789  Idlcidl 35902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4820  df-br 5054  df-opab 5116  df-mpt 5136  df-id 5455  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-iota 6338  df-fun 6382  df-fv 6388  df-ov 7216  df-idl 35905

This theorem is referenced by: (None)