Theorem unichnidl 33830

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 3592	. . . . 5 ⊢ (𝐶 ⊆ (Idl‘𝑅) ↔ ∀𝑖 ∈ 𝐶 𝑖 ∈ (Idl‘𝑅))
2		eqid 2622	. . . . . . . . 9 ⊢ (1st ‘𝑅) = (1st ‘𝑅)
3		eqid 2622	. . . . . . . . 9 ⊢ ran (1st ‘𝑅) = ran (1st ‘𝑅)
4	2, 3	idlss 33815	. . . . . . . 8 ⊢ ((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) → 𝑖 ⊆ ran (1st ‘𝑅))
5	4	ex 450	. . . . . . 7 ⊢ (𝑅 ∈ RingOps → (𝑖 ∈ (Idl‘𝑅) → 𝑖 ⊆ ran (1st ‘𝑅)))
6	5	ralimdv 2963	. . . . . 6 ⊢ (𝑅 ∈ RingOps → (∀𝑖 ∈ 𝐶 𝑖 ∈ (Idl‘𝑅) → ∀𝑖 ∈ 𝐶 𝑖 ⊆ ran (1st ‘𝑅)))
7	6	imp 445	. . . . 5 ⊢ ((𝑅 ∈ RingOps ∧ ∀𝑖 ∈ 𝐶 𝑖 ∈ (Idl‘𝑅)) → ∀𝑖 ∈ 𝐶 𝑖 ⊆ ran (1st ‘𝑅))
8	1, 7	sylan2b 492	. . . 4 ⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∀𝑖 ∈ 𝐶 𝑖 ⊆ ran (1st ‘𝑅))
9		unissb 4469	. . . 4 ⊢ (∪ 𝐶 ⊆ ran (1st ‘𝑅) ↔ ∀𝑖 ∈ 𝐶 𝑖 ⊆ ran (1st ‘𝑅))
10	8, 9	sylibr 224	. . 3 ⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∪ 𝐶 ⊆ ran (1st ‘𝑅))
11	10	3ad2antr2 1227	. 2 ⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → ∪ 𝐶 ⊆ ran (1st ‘𝑅))
12		eqid 2622	. . . . . . . . . . 11 ⊢ (GId‘(1st ‘𝑅)) = (GId‘(1st ‘𝑅))
13	2, 12	idl0cl 33817	. . . . . . . . . 10 ⊢ ((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) → (GId‘(1st ‘𝑅)) ∈ 𝑖)
14	13	ex 450	. . . . . . . . 9 ⊢ (𝑅 ∈ RingOps → (𝑖 ∈ (Idl‘𝑅) → (GId‘(1st ‘𝑅)) ∈ 𝑖))
15	14	ralimdv 2963	. . . . . . . 8 ⊢ (𝑅 ∈ RingOps → (∀𝑖 ∈ 𝐶 𝑖 ∈ (Idl‘𝑅) → ∀𝑖 ∈ 𝐶 (GId‘(1st ‘𝑅)) ∈ 𝑖))
16	15	imp 445	. . . . . . 7 ⊢ ((𝑅 ∈ RingOps ∧ ∀𝑖 ∈ 𝐶 𝑖 ∈ (Idl‘𝑅)) → ∀𝑖 ∈ 𝐶 (GId‘(1st ‘𝑅)) ∈ 𝑖)
17	1, 16	sylan2b 492	. . . . . 6 ⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∀𝑖 ∈ 𝐶 (GId‘(1st ‘𝑅)) ∈ 𝑖)
18		r19.2z 4060	. . . . . 6 ⊢ ((𝐶 ≠ ∅ ∧ ∀𝑖 ∈ 𝐶 (GId‘(1st ‘𝑅)) ∈ 𝑖) → ∃𝑖 ∈ 𝐶 (GId‘(1st ‘𝑅)) ∈ 𝑖)
19	17, 18	sylan2 491	. . . . 5 ⊢ ((𝐶 ≠ ∅ ∧ (𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅))) → ∃𝑖 ∈ 𝐶 (GId‘(1st ‘𝑅)) ∈ 𝑖)
20	19	an12s 843	. . . 4 ⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅))) → ∃𝑖 ∈ 𝐶 (GId‘(1st ‘𝑅)) ∈ 𝑖)
21		eluni2 4440	. . . 4 ⊢ ((GId‘(1st ‘𝑅)) ∈ ∪ 𝐶 ↔ ∃𝑖 ∈ 𝐶 (GId‘(1st ‘𝑅)) ∈ 𝑖)
22	20, 21	sylibr 224	. . 3 ⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅))) → (GId‘(1st ‘𝑅)) ∈ ∪ 𝐶)
23	22	3adantr3 1222	. 2 ⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → (GId‘(1st ‘𝑅)) ∈ ∪ 𝐶)
24		eluni2 4440	. . . 4 ⊢ (𝑥 ∈ ∪ 𝐶 ↔ ∃𝑘 ∈ 𝐶 𝑥 ∈ 𝑘)
25		sseq1 3626	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑘 → (𝑖 ⊆ 𝑗 ↔ 𝑘 ⊆ 𝑗))
26		sseq2 3627	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑘 → (𝑗 ⊆ 𝑖 ↔ 𝑗 ⊆ 𝑘))
27	25, 26	orbi12d 746	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑘 → ((𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖) ↔ (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)))
28	27	ralbidv 2986	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑘 → (∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖) ↔ ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)))
29	28	rspcv 3305	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ 𝐶 → (∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖) → ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)))
30	29	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘) → (∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖) → ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)))
31	30	ad2antlr 763	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) → (∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖) → ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)))
32	31	imp 445	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖)) → ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘))
33		eluni2 4440	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ∪ 𝐶 ↔ ∃𝑖 ∈ 𝐶 𝑦 ∈ 𝑖)
34		sseq2 3627	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝑖 → (𝑘 ⊆ 𝑗 ↔ 𝑘 ⊆ 𝑖))
35		sseq1 3626	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝑖 → (𝑗 ⊆ 𝑘 ↔ 𝑖 ⊆ 𝑘))
36	34, 35	orbi12d 746	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑖 → ((𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘) ↔ (𝑘 ⊆ 𝑖 ∨ 𝑖 ⊆ 𝑘)))
37	36	rspcv 3305	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 ∈ 𝐶 → (∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘) → (𝑘 ⊆ 𝑖 ∨ 𝑖 ⊆ 𝑘)))
38	37	ad2antrl 764	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖)) → (∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘) → (𝑘 ⊆ 𝑖 ∨ 𝑖 ⊆ 𝑘)))
39	38	imp 445	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖)) ∧ ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)) → (𝑘 ⊆ 𝑖 ∨ 𝑖 ⊆ 𝑘))
40		ssel2 3598	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ⊆ 𝑖 ∧ 𝑥 ∈ 𝑘) → 𝑥 ∈ 𝑖)
41	40	ancoms 469	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ 𝑘 ∧ 𝑘 ⊆ 𝑖) → 𝑥 ∈ 𝑖)
42	41	adantll 750	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘) ∧ 𝑘 ⊆ 𝑖) → 𝑥 ∈ 𝑖)
43		ssel2 3598	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐶 ⊆ (Idl‘𝑅) ∧ 𝑖 ∈ 𝐶) → 𝑖 ∈ (Idl‘𝑅))
44	2	idladdcl 33818	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ (𝑥 ∈ 𝑖 ∧ 𝑦 ∈ 𝑖)) → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑖)
45	44	ancom2s 844	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ (𝑦 ∈ 𝑖 ∧ 𝑥 ∈ 𝑖)) → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑖)
46	45	expr 643	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ 𝑦 ∈ 𝑖) → (𝑥 ∈ 𝑖 → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑖))
47	46	an32s 846	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑅 ∈ RingOps ∧ 𝑦 ∈ 𝑖) ∧ 𝑖 ∈ (Idl‘𝑅)) → (𝑥 ∈ 𝑖 → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑖))
48	43, 47	sylan2 491	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑅 ∈ RingOps ∧ 𝑦 ∈ 𝑖) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑖 ∈ 𝐶)) → (𝑥 ∈ 𝑖 → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑖))
49	48	an42s 870	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖)) → (𝑥 ∈ 𝑖 → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑖))
50	49	anasss 679	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖))) → (𝑥 ∈ 𝑖 → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑖))
51	50	imp 445	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖))) ∧ 𝑥 ∈ 𝑖) → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑖)
52		simprl 794	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖)) → 𝑖 ∈ 𝐶)
53	52	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖))) ∧ 𝑥 ∈ 𝑖) → 𝑖 ∈ 𝐶)
54		elunii 4441	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥(1st ‘𝑅)𝑦) ∈ 𝑖 ∧ 𝑖 ∈ 𝐶) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
55	51, 53, 54	syl2anc 693	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖))) ∧ 𝑥 ∈ 𝑖) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
56	42, 55	sylan2 491	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖))) ∧ ((𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘) ∧ 𝑘 ⊆ 𝑖)) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
57	56	expr 643	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖))) ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) → (𝑘 ⊆ 𝑖 → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶))
58	57	an32s 846	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖))) → (𝑘 ⊆ 𝑖 → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶))
59	58	anassrs 680	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖)) → (𝑘 ⊆ 𝑖 → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶))
60	59	imp 445	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖)) ∧ 𝑘 ⊆ 𝑖) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
61		ssel2 3598	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ⊆ 𝑘 ∧ 𝑦 ∈ 𝑖) → 𝑦 ∈ 𝑘)
62	61	ancoms 469	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ 𝑖 ∧ 𝑖 ⊆ 𝑘) → 𝑦 ∈ 𝑘)
63	62	adantll 750	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖) ∧ 𝑖 ⊆ 𝑘) → 𝑦 ∈ 𝑘)
64		ssel2 3598	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘 ∈ 𝐶) → 𝑘 ∈ (Idl‘𝑅))
65	2	idladdcl 33818	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑅 ∈ RingOps ∧ 𝑘 ∈ (Idl‘𝑅)) ∧ (𝑥 ∈ 𝑘 ∧ 𝑦 ∈ 𝑘)) → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑘)
66	65	expr 643	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑅 ∈ RingOps ∧ 𝑘 ∈ (Idl‘𝑅)) ∧ 𝑥 ∈ 𝑘) → (𝑦 ∈ 𝑘 → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑘))
67	66	an32s 846	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ 𝑘 ∈ (Idl‘𝑅)) → (𝑦 ∈ 𝑘 → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑘))
68	64, 67	sylan2 491	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘 ∈ 𝐶)) → (𝑦 ∈ 𝑘 → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑘))
69	68	an42s 870	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) → (𝑦 ∈ 𝑘 → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑘))
70	69	an32s 846	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) → (𝑦 ∈ 𝑘 → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑘))
71	70	imp 445	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑦 ∈ 𝑘) → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑘)
72		simprl 794	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) → 𝑘 ∈ 𝐶)
73	72	ad2antrr 762	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑦 ∈ 𝑘) → 𝑘 ∈ 𝐶)
74		elunii 4441	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥(1st ‘𝑅)𝑦) ∈ 𝑘 ∧ 𝑘 ∈ 𝐶) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
75	71, 73, 74	syl2anc 693	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑦 ∈ 𝑘) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
76	63, 75	sylan2 491	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ((𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖) ∧ 𝑖 ⊆ 𝑘)) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
77	76	anassrs 680	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖)) ∧ 𝑖 ⊆ 𝑘) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
78	60, 77	jaodan 826	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖)) ∧ (𝑘 ⊆ 𝑖 ∨ 𝑖 ⊆ 𝑘)) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
79	39, 78	syldan 487	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖)) ∧ ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
80	79	an32s 846	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖)) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
81	80	rexlimdvaa 3032	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)) → (∃𝑖 ∈ 𝐶 𝑦 ∈ 𝑖 → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶))
82	33, 81	syl5bi 232	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)) → (𝑦 ∈ ∪ 𝐶 → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶))
83	82	ralrimiv 2965	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)) → ∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
84	32, 83	syldan 487	. . . . . . . . 9 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖)) → ∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
85	84	anasss 679	. . . . . . . 8 ⊢ (((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → ∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
86	85	3adantr1 1220	. . . . . . 7 ⊢ (((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → ∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
87	86	an32s 846	. . . . . 6 ⊢ (((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) → ∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
88		eqid 2622	. . . . . . . . . . . . . . . . . 18 ⊢ (2nd ‘𝑅) = (2nd ‘𝑅)
89	2, 88, 3	idllmulcl 33819	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ RingOps ∧ 𝑘 ∈ (Idl‘𝑅)) ∧ (𝑥 ∈ 𝑘 ∧ 𝑧 ∈ ran (1st ‘𝑅))) → (𝑧(2nd ‘𝑅)𝑥) ∈ 𝑘)
90	89	exp43 640	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ RingOps → (𝑘 ∈ (Idl‘𝑅) → (𝑥 ∈ 𝑘 → (𝑧 ∈ ran (1st ‘𝑅) → (𝑧(2nd ‘𝑅)𝑥) ∈ 𝑘))))
91	90	com23 86	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ RingOps → (𝑥 ∈ 𝑘 → (𝑘 ∈ (Idl‘𝑅) → (𝑧 ∈ ran (1st ‘𝑅) → (𝑧(2nd ‘𝑅)𝑥) ∈ 𝑘))))
92	91	imp41 619	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ 𝑘 ∈ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝑧(2nd ‘𝑅)𝑥) ∈ 𝑘)
93	64, 92	sylanl2 683	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘 ∈ 𝐶)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝑧(2nd ‘𝑅)𝑥) ∈ 𝑘)
94		simplrr 801	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘 ∈ 𝐶)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → 𝑘 ∈ 𝐶)
95		elunii 4441	. . . . . . . . . . . . 13 ⊢ (((𝑧(2nd ‘𝑅)𝑥) ∈ 𝑘 ∧ 𝑘 ∈ 𝐶) → (𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶)
96	93, 94, 95	syl2anc 693	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘 ∈ 𝐶)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶)
97	2, 88, 3	idlrmulcl 33820	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ RingOps ∧ 𝑘 ∈ (Idl‘𝑅)) ∧ (𝑥 ∈ 𝑘 ∧ 𝑧 ∈ ran (1st ‘𝑅))) → (𝑥(2nd ‘𝑅)𝑧) ∈ 𝑘)
98	97	exp43 640	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ RingOps → (𝑘 ∈ (Idl‘𝑅) → (𝑥 ∈ 𝑘 → (𝑧 ∈ ran (1st ‘𝑅) → (𝑥(2nd ‘𝑅)𝑧) ∈ 𝑘))))
99	98	com23 86	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ RingOps → (𝑥 ∈ 𝑘 → (𝑘 ∈ (Idl‘𝑅) → (𝑧 ∈ ran (1st ‘𝑅) → (𝑥(2nd ‘𝑅)𝑧) ∈ 𝑘))))
100	99	imp41 619	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ 𝑘 ∈ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝑥(2nd ‘𝑅)𝑧) ∈ 𝑘)
101	64, 100	sylanl2 683	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘 ∈ 𝐶)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝑥(2nd ‘𝑅)𝑧) ∈ 𝑘)
102		elunii 4441	. . . . . . . . . . . . 13 ⊢ (((𝑥(2nd ‘𝑅)𝑧) ∈ 𝑘 ∧ 𝑘 ∈ 𝐶) → (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶)
103	101, 94, 102	syl2anc 693	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘 ∈ 𝐶)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶)
104	96, 103	jca 554	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘 ∈ 𝐶)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → ((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶))
105	104	ralrimiva 2966	. . . . . . . . . 10 ⊢ (((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘 ∈ 𝐶)) → ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶))
106	105	an42s 870	. . . . . . . . 9 ⊢ (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) → ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶))
107	106	an32s 846	. . . . . . . 8 ⊢ (((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶))
108	107	3ad2antr2 1227	. . . . . . 7 ⊢ (((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶))
109	108	an32s 846	. . . . . 6 ⊢ (((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) → ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶))
110	87, 109	jca 554	. . . . 5 ⊢ (((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) → (∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶 ∧ ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶)))
111	110	rexlimdvaa 3032	. . . 4 ⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → (∃𝑘 ∈ 𝐶 𝑥 ∈ 𝑘 → (∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶 ∧ ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶))))
112	24, 111	syl5bi 232	. . 3 ⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → (𝑥 ∈ ∪ 𝐶 → (∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶 ∧ ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶))))
113	112	ralrimiv 2965	. 2 ⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → ∀𝑥 ∈ ∪ 𝐶(∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶 ∧ ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶)))
114	2, 88, 3, 12	isidl 33813	. . 3 ⊢ (𝑅 ∈ RingOps → (∪ 𝐶 ∈ (Idl‘𝑅) ↔ (∪ 𝐶 ⊆ ran (1st ‘𝑅) ∧ (GId‘(1st ‘𝑅)) ∈ ∪ 𝐶 ∧ ∀𝑥 ∈ ∪ 𝐶(∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶 ∧ ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶)))))
115	114	adantr 481	. 2 ⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → (∪ 𝐶 ∈ (Idl‘𝑅) ↔ (∪ 𝐶 ⊆ ran (1st ‘𝑅) ∧ (GId‘(1st ‘𝑅)) ∈ ∪ 𝐶 ∧ ∀𝑥 ∈ ∪ 𝐶(∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶 ∧ ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶)))))
116	11, 23, 113, 115	mpbir3and 1245	1 ⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → ∪ 𝐶 ∈ (Idl‘𝑅))

Syntax hints:   → wi 4   ↔ wb 196   ∨ wo 383   ∧ wa 384   ∧ w3a 1037   ∈ wcel 1990   ≠ wne 2794  ∀wral 2912  ∃wrex 2913   ⊆ wss 3574  ∅c0 3915  ∪ cuni 4436  ran crn 5115  ‘cfv 5888  (class class class)co 6650  1^st c1st 7166  2^nd c2nd 7167  GIdcgi 27344  RingOpscrngo 33693  Idlcidl 33806

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-iota 5851  df-fun 5890  df-fv 5896  df-ov 6653  df-idl 33809

This theorem is referenced by: (None)