Theorem unichnidl 36189

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 3909	. . . . 5 ⊢ (𝐶 ⊆ (Idl‘𝑅) ↔ ∀𝑖 ∈ 𝐶 𝑖 ∈ (Idl‘𝑅))
2		eqid 2738	. . . . . . . . 9 ⊢ (1st ‘𝑅) = (1st ‘𝑅)
3		eqid 2738	. . . . . . . . 9 ⊢ ran (1st ‘𝑅) = ran (1st ‘𝑅)
4	2, 3	idlss 36174	. . . . . . . 8 ⊢ ((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) → 𝑖 ⊆ ran (1st ‘𝑅))
5	4	ex 413	. . . . . . 7 ⊢ (𝑅 ∈ RingOps → (𝑖 ∈ (Idl‘𝑅) → 𝑖 ⊆ ran (1st ‘𝑅)))
6	5	ralimdv 3109	. . . . . 6 ⊢ (𝑅 ∈ RingOps → (∀𝑖 ∈ 𝐶 𝑖 ∈ (Idl‘𝑅) → ∀𝑖 ∈ 𝐶 𝑖 ⊆ ran (1st ‘𝑅)))
7	6	imp 407	. . . . 5 ⊢ ((𝑅 ∈ RingOps ∧ ∀𝑖 ∈ 𝐶 𝑖 ∈ (Idl‘𝑅)) → ∀𝑖 ∈ 𝐶 𝑖 ⊆ ran (1st ‘𝑅))
8	1, 7	sylan2b 594	. . . 4 ⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∀𝑖 ∈ 𝐶 𝑖 ⊆ ran (1st ‘𝑅))
9		unissb 4873	. . . 4 ⊢ (∪ 𝐶 ⊆ ran (1st ‘𝑅) ↔ ∀𝑖 ∈ 𝐶 𝑖 ⊆ ran (1st ‘𝑅))
10	8, 9	sylibr 233	. . 3 ⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∪ 𝐶 ⊆ ran (1st ‘𝑅))
11	10	3ad2antr2 1188	. 2 ⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → ∪ 𝐶 ⊆ ran (1st ‘𝑅))
12		eqid 2738	. . . . . . . . . . 11 ⊢ (GId‘(1st ‘𝑅)) = (GId‘(1st ‘𝑅))
13	2, 12	idl0cl 36176	. . . . . . . . . 10 ⊢ ((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) → (GId‘(1st ‘𝑅)) ∈ 𝑖)
14	13	ex 413	. . . . . . . . 9 ⊢ (𝑅 ∈ RingOps → (𝑖 ∈ (Idl‘𝑅) → (GId‘(1st ‘𝑅)) ∈ 𝑖))
15	14	ralimdv 3109	. . . . . . . 8 ⊢ (𝑅 ∈ RingOps → (∀𝑖 ∈ 𝐶 𝑖 ∈ (Idl‘𝑅) → ∀𝑖 ∈ 𝐶 (GId‘(1st ‘𝑅)) ∈ 𝑖))
16	15	imp 407	. . . . . . 7 ⊢ ((𝑅 ∈ RingOps ∧ ∀𝑖 ∈ 𝐶 𝑖 ∈ (Idl‘𝑅)) → ∀𝑖 ∈ 𝐶 (GId‘(1st ‘𝑅)) ∈ 𝑖)
17	1, 16	sylan2b 594	. . . . . 6 ⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∀𝑖 ∈ 𝐶 (GId‘(1st ‘𝑅)) ∈ 𝑖)
18		r19.2z 4425	. . . . . 6 ⊢ ((𝐶 ≠ ∅ ∧ ∀𝑖 ∈ 𝐶 (GId‘(1st ‘𝑅)) ∈ 𝑖) → ∃𝑖 ∈ 𝐶 (GId‘(1st ‘𝑅)) ∈ 𝑖)
19	17, 18	sylan2 593	. . . . 5 ⊢ ((𝐶 ≠ ∅ ∧ (𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅))) → ∃𝑖 ∈ 𝐶 (GId‘(1st ‘𝑅)) ∈ 𝑖)
20	19	an12s 646	. . . 4 ⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅))) → ∃𝑖 ∈ 𝐶 (GId‘(1st ‘𝑅)) ∈ 𝑖)
21		eluni2 4843	. . . 4 ⊢ ((GId‘(1st ‘𝑅)) ∈ ∪ 𝐶 ↔ ∃𝑖 ∈ 𝐶 (GId‘(1st ‘𝑅)) ∈ 𝑖)
22	20, 21	sylibr 233	. . 3 ⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅))) → (GId‘(1st ‘𝑅)) ∈ ∪ 𝐶)
23	22	3adantr3 1170	. 2 ⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → (GId‘(1st ‘𝑅)) ∈ ∪ 𝐶)
24		eluni2 4843	. . . 4 ⊢ (𝑥 ∈ ∪ 𝐶 ↔ ∃𝑘 ∈ 𝐶 𝑥 ∈ 𝑘)
25		sseq1 3946	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑘 → (𝑖 ⊆ 𝑗 ↔ 𝑘 ⊆ 𝑗))
26		sseq2 3947	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑘 → (𝑗 ⊆ 𝑖 ↔ 𝑗 ⊆ 𝑘))
27	25, 26	orbi12d 916	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑘 → ((𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖) ↔ (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)))
28	27	ralbidv 3112	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑘 → (∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖) ↔ ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)))
29	28	rspcv 3557	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ 𝐶 → (∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖) → ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)))
30	29	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘) → (∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖) → ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)))
31	30	ad2antlr 724	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) → (∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖) → ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)))
32	31	imp 407	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖)) → ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘))
33		eluni2 4843	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ∪ 𝐶 ↔ ∃𝑖 ∈ 𝐶 𝑦 ∈ 𝑖)
34		sseq2 3947	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝑖 → (𝑘 ⊆ 𝑗 ↔ 𝑘 ⊆ 𝑖))
35		sseq1 3946	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝑖 → (𝑗 ⊆ 𝑘 ↔ 𝑖 ⊆ 𝑘))
36	34, 35	orbi12d 916	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑖 → ((𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘) ↔ (𝑘 ⊆ 𝑖 ∨ 𝑖 ⊆ 𝑘)))
37	36	rspcv 3557	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 ∈ 𝐶 → (∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘) → (𝑘 ⊆ 𝑖 ∨ 𝑖 ⊆ 𝑘)))
38	37	ad2antrl 725	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖)) → (∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘) → (𝑘 ⊆ 𝑖 ∨ 𝑖 ⊆ 𝑘)))
39	38	imp 407	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖)) ∧ ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)) → (𝑘 ⊆ 𝑖 ∨ 𝑖 ⊆ 𝑘))
40		ssel2 3916	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ⊆ 𝑖 ∧ 𝑥 ∈ 𝑘) → 𝑥 ∈ 𝑖)
41	40	ancoms 459	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ 𝑘 ∧ 𝑘 ⊆ 𝑖) → 𝑥 ∈ 𝑖)
42	41	adantll 711	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘) ∧ 𝑘 ⊆ 𝑖) → 𝑥 ∈ 𝑖)
43		ssel2 3916	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐶 ⊆ (Idl‘𝑅) ∧ 𝑖 ∈ 𝐶) → 𝑖 ∈ (Idl‘𝑅))
44	2	idladdcl 36177	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ (𝑥 ∈ 𝑖 ∧ 𝑦 ∈ 𝑖)) → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑖)
45	44	ancom2s 647	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ (𝑦 ∈ 𝑖 ∧ 𝑥 ∈ 𝑖)) → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑖)
46	45	expr 457	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ 𝑦 ∈ 𝑖) → (𝑥 ∈ 𝑖 → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑖))
47	46	an32s 649	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑅 ∈ RingOps ∧ 𝑦 ∈ 𝑖) ∧ 𝑖 ∈ (Idl‘𝑅)) → (𝑥 ∈ 𝑖 → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑖))
48	43, 47	sylan2 593	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑅 ∈ RingOps ∧ 𝑦 ∈ 𝑖) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑖 ∈ 𝐶)) → (𝑥 ∈ 𝑖 → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑖))
49	48	an42s 658	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖)) → (𝑥 ∈ 𝑖 → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑖))
50	49	anasss 467	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖))) → (𝑥 ∈ 𝑖 → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑖))
51	50	imp 407	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖))) ∧ 𝑥 ∈ 𝑖) → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑖)
52		simprl 768	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖)) → 𝑖 ∈ 𝐶)
53	52	ad2antlr 724	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖))) ∧ 𝑥 ∈ 𝑖) → 𝑖 ∈ 𝐶)
54		elunii 4844	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥(1st ‘𝑅)𝑦) ∈ 𝑖 ∧ 𝑖 ∈ 𝐶) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
55	51, 53, 54	syl2anc 584	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖))) ∧ 𝑥 ∈ 𝑖) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
56	42, 55	sylan2 593	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖))) ∧ ((𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘) ∧ 𝑘 ⊆ 𝑖)) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
57	56	expr 457	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖))) ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) → (𝑘 ⊆ 𝑖 → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶))
58	57	an32s 649	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖))) → (𝑘 ⊆ 𝑖 → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶))
59	58	anassrs 468	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖)) → (𝑘 ⊆ 𝑖 → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶))
60	59	imp 407	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖)) ∧ 𝑘 ⊆ 𝑖) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
61		ssel2 3916	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ⊆ 𝑘 ∧ 𝑦 ∈ 𝑖) → 𝑦 ∈ 𝑘)
62	61	ancoms 459	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ 𝑖 ∧ 𝑖 ⊆ 𝑘) → 𝑦 ∈ 𝑘)
63	62	adantll 711	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖) ∧ 𝑖 ⊆ 𝑘) → 𝑦 ∈ 𝑘)
64		ssel2 3916	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘 ∈ 𝐶) → 𝑘 ∈ (Idl‘𝑅))
65	2	idladdcl 36177	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑅 ∈ RingOps ∧ 𝑘 ∈ (Idl‘𝑅)) ∧ (𝑥 ∈ 𝑘 ∧ 𝑦 ∈ 𝑘)) → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑘)
66	65	expr 457	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑅 ∈ RingOps ∧ 𝑘 ∈ (Idl‘𝑅)) ∧ 𝑥 ∈ 𝑘) → (𝑦 ∈ 𝑘 → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑘))
67	66	an32s 649	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ 𝑘 ∈ (Idl‘𝑅)) → (𝑦 ∈ 𝑘 → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑘))
68	64, 67	sylan2 593	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘 ∈ 𝐶)) → (𝑦 ∈ 𝑘 → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑘))
69	68	an42s 658	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) → (𝑦 ∈ 𝑘 → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑘))
70	69	an32s 649	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) → (𝑦 ∈ 𝑘 → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑘))
71	70	imp 407	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑦 ∈ 𝑘) → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑘)
72		simprl 768	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) → 𝑘 ∈ 𝐶)
73	72	ad2antrr 723	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑦 ∈ 𝑘) → 𝑘 ∈ 𝐶)
74		elunii 4844	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥(1st ‘𝑅)𝑦) ∈ 𝑘 ∧ 𝑘 ∈ 𝐶) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
75	71, 73, 74	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑦 ∈ 𝑘) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
76	63, 75	sylan2 593	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ((𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖) ∧ 𝑖 ⊆ 𝑘)) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
77	76	anassrs 468	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖)) ∧ 𝑖 ⊆ 𝑘) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
78	60, 77	jaodan 955	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖)) ∧ (𝑘 ⊆ 𝑖 ∨ 𝑖 ⊆ 𝑘)) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
79	39, 78	syldan 591	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖)) ∧ ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
80	79	an32s 649	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖)) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
81	80	rexlimdvaa 3214	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)) → (∃𝑖 ∈ 𝐶 𝑦 ∈ 𝑖 → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶))
82	33, 81	syl5bi 241	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)) → (𝑦 ∈ ∪ 𝐶 → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶))
83	82	ralrimiv 3102	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)) → ∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
84	32, 83	syldan 591	. . . . . . . . 9 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖)) → ∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
85	84	anasss 467	. . . . . . . 8 ⊢ (((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → ∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
86	85	3adantr1 1168	. . . . . . 7 ⊢ (((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → ∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
87	86	an32s 649	. . . . . 6 ⊢ (((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) → ∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
88		eqid 2738	. . . . . . . . . . . . . . . . . 18 ⊢ (2nd ‘𝑅) = (2nd ‘𝑅)
89	2, 88, 3	idllmulcl 36178	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ RingOps ∧ 𝑘 ∈ (Idl‘𝑅)) ∧ (𝑥 ∈ 𝑘 ∧ 𝑧 ∈ ran (1st ‘𝑅))) → (𝑧(2nd ‘𝑅)𝑥) ∈ 𝑘)
90	89	exp43 437	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ RingOps → (𝑘 ∈ (Idl‘𝑅) → (𝑥 ∈ 𝑘 → (𝑧 ∈ ran (1st ‘𝑅) → (𝑧(2nd ‘𝑅)𝑥) ∈ 𝑘))))
91	90	com23 86	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ RingOps → (𝑥 ∈ 𝑘 → (𝑘 ∈ (Idl‘𝑅) → (𝑧 ∈ ran (1st ‘𝑅) → (𝑧(2nd ‘𝑅)𝑥) ∈ 𝑘))))
92	91	imp41 426	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ 𝑘 ∈ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝑧(2nd ‘𝑅)𝑥) ∈ 𝑘)
93	64, 92	sylanl2 678	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘 ∈ 𝐶)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝑧(2nd ‘𝑅)𝑥) ∈ 𝑘)
94		simplrr 775	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘 ∈ 𝐶)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → 𝑘 ∈ 𝐶)
95		elunii 4844	. . . . . . . . . . . . 13 ⊢ (((𝑧(2nd ‘𝑅)𝑥) ∈ 𝑘 ∧ 𝑘 ∈ 𝐶) → (𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶)
96	93, 94, 95	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘 ∈ 𝐶)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶)
97	2, 88, 3	idlrmulcl 36179	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ RingOps ∧ 𝑘 ∈ (Idl‘𝑅)) ∧ (𝑥 ∈ 𝑘 ∧ 𝑧 ∈ ran (1st ‘𝑅))) → (𝑥(2nd ‘𝑅)𝑧) ∈ 𝑘)
98	97	exp43 437	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ RingOps → (𝑘 ∈ (Idl‘𝑅) → (𝑥 ∈ 𝑘 → (𝑧 ∈ ran (1st ‘𝑅) → (𝑥(2nd ‘𝑅)𝑧) ∈ 𝑘))))
99	98	com23 86	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ RingOps → (𝑥 ∈ 𝑘 → (𝑘 ∈ (Idl‘𝑅) → (𝑧 ∈ ran (1st ‘𝑅) → (𝑥(2nd ‘𝑅)𝑧) ∈ 𝑘))))
100	99	imp41 426	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ 𝑘 ∈ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝑥(2nd ‘𝑅)𝑧) ∈ 𝑘)
101	64, 100	sylanl2 678	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘 ∈ 𝐶)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝑥(2nd ‘𝑅)𝑧) ∈ 𝑘)
102		elunii 4844	. . . . . . . . . . . . 13 ⊢ (((𝑥(2nd ‘𝑅)𝑧) ∈ 𝑘 ∧ 𝑘 ∈ 𝐶) → (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶)
103	101, 94, 102	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘 ∈ 𝐶)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶)
104	96, 103	jca 512	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘 ∈ 𝐶)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → ((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶))
105	104	ralrimiva 3103	. . . . . . . . . 10 ⊢ (((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘 ∈ 𝐶)) → ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶))
106	105	an42s 658	. . . . . . . . 9 ⊢ (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) → ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶))
107	106	an32s 649	. . . . . . . 8 ⊢ (((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶))
108	107	3ad2antr2 1188	. . . . . . 7 ⊢ (((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶))
109	108	an32s 649	. . . . . 6 ⊢ (((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) → ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶))
110	87, 109	jca 512	. . . . 5 ⊢ (((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) → (∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶 ∧ ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶)))
111	110	rexlimdvaa 3214	. . . 4 ⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → (∃𝑘 ∈ 𝐶 𝑥 ∈ 𝑘 → (∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶 ∧ ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶))))
112	24, 111	syl5bi 241	. . 3 ⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → (𝑥 ∈ ∪ 𝐶 → (∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶 ∧ ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶))))
113	112	ralrimiv 3102	. 2 ⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → ∀𝑥 ∈ ∪ 𝐶(∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶 ∧ ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶)))
114	2, 88, 3, 12	isidl 36172	. . 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 1341	1 ⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → ∪ 𝐶 ∈ (Idl‘𝑅))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 844   ∧ w3a 1086   ∈ wcel 2106   ≠ wne 2943  ∀wral 3064  ∃wrex 3065   ⊆ wss 3887  ∅c0 4256  ∪ cuni 4839  ran crn 5590  ‘cfv 6433  (class class class)co 7275  1^st c1st 7829  2^nd c2nd 7830  GIdcgi 28852  RingOpscrngo 36052  Idlcidl 36165

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-iota 6391  df-fun 6435  df-fv 6441  df-ov 7278  df-idl 36168

This theorem is referenced by: (None)