Theorem unichnidl 38660

Description: Obsolete theorem, use unichnlidl 21343 instead. The union of a nonempty chain of ideals is an ideal. (Contributed by Jeff Madsen, 5-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

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 3927	. . . . 5 ⊢ (𝐶 ⊆ (Idl‘𝑅) ↔ ∀𝑖 ∈ 𝐶 𝑖 ∈ (Idl‘𝑅))
2		eqid 2763	. . . . . . . . 9 ⊢ (1st ‘𝑅) = (1st ‘𝑅)
3		eqid 2763	. . . . . . . . 9 ⊢ ran (1st ‘𝑅) = ran (1st ‘𝑅)
4	2, 3	idlss 38645	. . . . . . . 8 ⊢ ((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) → 𝑖 ⊆ ran (1st ‘𝑅))
5	4	ex 417	. . . . . . 7 ⊢ (𝑅 ∈ RingOps → (𝑖 ∈ (Idl‘𝑅) → 𝑖 ⊆ ran (1st ‘𝑅)))
6	5	ralimdv 3179	. . . . . 6 ⊢ (𝑅 ∈ RingOps → (∀𝑖 ∈ 𝐶 𝑖 ∈ (Idl‘𝑅) → ∀𝑖 ∈ 𝐶 𝑖 ⊆ ran (1st ‘𝑅)))
7	6	imp 411	. . . . 5 ⊢ ((𝑅 ∈ RingOps ∧ ∀𝑖 ∈ 𝐶 𝑖 ∈ (Idl‘𝑅)) → ∀𝑖 ∈ 𝐶 𝑖 ⊆ ran (1st ‘𝑅))
8	1, 7	sylan2b 605	. . . 4 ⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∀𝑖 ∈ 𝐶 𝑖 ⊆ ran (1st ‘𝑅))
9		unissb 4907	. . . 4 ⊢ (∪ 𝐶 ⊆ ran (1st ‘𝑅) ↔ ∀𝑖 ∈ 𝐶 𝑖 ⊆ ran (1st ‘𝑅))
10	8, 9	sylibr 237	. . 3 ⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∪ 𝐶 ⊆ ran (1st ‘𝑅))
11	10	3ad2antr2 1208	. 2 ⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → ∪ 𝐶 ⊆ ran (1st ‘𝑅))
12		eqid 2763	. . . . . . . . . . 11 ⊢ (GId‘(1st ‘𝑅)) = (GId‘(1st ‘𝑅))
13	2, 12	idl0cl 38647	. . . . . . . . . 10 ⊢ ((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) → (GId‘(1st ‘𝑅)) ∈ 𝑖)
14	13	ex 417	. . . . . . . . 9 ⊢ (𝑅 ∈ RingOps → (𝑖 ∈ (Idl‘𝑅) → (GId‘(1st ‘𝑅)) ∈ 𝑖))
15	14	ralimdv 3179	. . . . . . . 8 ⊢ (𝑅 ∈ RingOps → (∀𝑖 ∈ 𝐶 𝑖 ∈ (Idl‘𝑅) → ∀𝑖 ∈ 𝐶 (GId‘(1st ‘𝑅)) ∈ 𝑖))
16	15	imp 411	. . . . . . 7 ⊢ ((𝑅 ∈ RingOps ∧ ∀𝑖 ∈ 𝐶 𝑖 ∈ (Idl‘𝑅)) → ∀𝑖 ∈ 𝐶 (GId‘(1st ‘𝑅)) ∈ 𝑖)
17	1, 16	sylan2b 605	. . . . . 6 ⊢ ((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∀𝑖 ∈ 𝐶 (GId‘(1st ‘𝑅)) ∈ 𝑖)
18		r19.2z 4461	. . . . . 6 ⊢ ((𝐶 ≠ ∅ ∧ ∀𝑖 ∈ 𝐶 (GId‘(1st ‘𝑅)) ∈ 𝑖) → ∃𝑖 ∈ 𝐶 (GId‘(1st ‘𝑅)) ∈ 𝑖)
19	17, 18	sylan2 604	. . . . 5 ⊢ ((𝐶 ≠ ∅ ∧ (𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅))) → ∃𝑖 ∈ 𝐶 (GId‘(1st ‘𝑅)) ∈ 𝑖)
20	19	an12s 661	. . . 4 ⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅))) → ∃𝑖 ∈ 𝐶 (GId‘(1st ‘𝑅)) ∈ 𝑖)
21		eluni2 4877	. . . 4 ⊢ ((GId‘(1st ‘𝑅)) ∈ ∪ 𝐶 ↔ ∃𝑖 ∈ 𝐶 (GId‘(1st ‘𝑅)) ∈ 𝑖)
22	20, 21	sylibr 237	. . 3 ⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅))) → (GId‘(1st ‘𝑅)) ∈ ∪ 𝐶)
23	22	3adantr3 1190	. 2 ⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → (GId‘(1st ‘𝑅)) ∈ ∪ 𝐶)
24		eluni2 4877	. . . 4 ⊢ (𝑥 ∈ ∪ 𝐶 ↔ ∃𝑘 ∈ 𝐶 𝑥 ∈ 𝑘)
25		sseq1 3963	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑘 → (𝑖 ⊆ 𝑗 ↔ 𝑘 ⊆ 𝑗))
26		sseq2 3964	. . . . . . . . . . . . . . . 16 ⊢ (𝑖 = 𝑘 → (𝑗 ⊆ 𝑖 ↔ 𝑗 ⊆ 𝑘))
27	25, 26	orbi12d 931	. . . . . . . . . . . . . . 15 ⊢ (𝑖 = 𝑘 → ((𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖) ↔ (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)))
28	27	ralbidv 3188	. . . . . . . . . . . . . 14 ⊢ (𝑖 = 𝑘 → (∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖) ↔ ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)))
29	28	rspcv 3578	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ 𝐶 → (∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖) → ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)))
30	29	adantr 485	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘) → (∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖) → ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)))
31	30	ad2antlr 739	. . . . . . . . . . 11 ⊢ (((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) → (∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖) → ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)))
32	31	imp 411	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖)) → ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘))
33		eluni2 4877	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ∪ 𝐶 ↔ ∃𝑖 ∈ 𝐶 𝑦 ∈ 𝑖)
34		sseq2 3964	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝑖 → (𝑘 ⊆ 𝑗 ↔ 𝑘 ⊆ 𝑖))
35		sseq1 3963	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 = 𝑖 → (𝑗 ⊆ 𝑘 ↔ 𝑖 ⊆ 𝑘))
36	34, 35	orbi12d 931	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑗 = 𝑖 → ((𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘) ↔ (𝑘 ⊆ 𝑖 ∨ 𝑖 ⊆ 𝑘)))
37	36	rspcv 3578	. . . . . . . . . . . . . . . . 17 ⊢ (𝑖 ∈ 𝐶 → (∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘) → (𝑘 ⊆ 𝑖 ∨ 𝑖 ⊆ 𝑘)))
38	37	ad2antrl 740	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖)) → (∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘) → (𝑘 ⊆ 𝑖 ∨ 𝑖 ⊆ 𝑘)))
39	38	imp 411	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖)) ∧ ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)) → (𝑘 ⊆ 𝑖 ∨ 𝑖 ⊆ 𝑘))
40		ssel2 3933	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑘 ⊆ 𝑖 ∧ 𝑥 ∈ 𝑘) → 𝑥 ∈ 𝑖)
41	40	ancoms 463	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑥 ∈ 𝑘 ∧ 𝑘 ⊆ 𝑖) → 𝑥 ∈ 𝑖)
42	41	adantll 726	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘) ∧ 𝑘 ⊆ 𝑖) → 𝑥 ∈ 𝑖)
43		ssel2 3933	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝐶 ⊆ (Idl‘𝑅) ∧ 𝑖 ∈ 𝐶) → 𝑖 ∈ (Idl‘𝑅))
44	2	idladdcl 38648	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ (𝑥 ∈ 𝑖 ∧ 𝑦 ∈ 𝑖)) → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑖)
45	44	ancom2s 662	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ (𝑦 ∈ 𝑖 ∧ 𝑥 ∈ 𝑖)) → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑖)
46	45	expr 461	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ 𝑦 ∈ 𝑖) → (𝑥 ∈ 𝑖 → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑖))
47	46	an32s 664	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑅 ∈ RingOps ∧ 𝑦 ∈ 𝑖) ∧ 𝑖 ∈ (Idl‘𝑅)) → (𝑥 ∈ 𝑖 → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑖))
48	43, 47	sylan2 604	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑅 ∈ RingOps ∧ 𝑦 ∈ 𝑖) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑖 ∈ 𝐶)) → (𝑥 ∈ 𝑖 → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑖))
49	48	an42s 673	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖)) → (𝑥 ∈ 𝑖 → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑖))
50	49	anasss 471	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖))) → (𝑥 ∈ 𝑖 → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑖))
51	50	imp 411	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖))) ∧ 𝑥 ∈ 𝑖) → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑖)
52		simprl 782	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖)) → 𝑖 ∈ 𝐶)
53	52	ad2antlr 739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖))) ∧ 𝑥 ∈ 𝑖) → 𝑖 ∈ 𝐶)
54		elunii 4878	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑥(1st ‘𝑅)𝑦) ∈ 𝑖 ∧ 𝑖 ∈ 𝐶) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
55	51, 53, 54	syl2anc 595	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖))) ∧ 𝑥 ∈ 𝑖) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
56	42, 55	sylan2 604	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖))) ∧ ((𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘) ∧ 𝑘 ⊆ 𝑖)) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
57	56	expr 461	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖))) ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) → (𝑘 ⊆ 𝑖 → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶))
58	57	an32s 664	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖))) → (𝑘 ⊆ 𝑖 → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶))
59	58	anassrs 472	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖)) → (𝑘 ⊆ 𝑖 → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶))
60	59	imp 411	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖)) ∧ 𝑘 ⊆ 𝑖) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
61		ssel2 3933	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ⊆ 𝑘 ∧ 𝑦 ∈ 𝑖) → 𝑦 ∈ 𝑘)
62	61	ancoms 463	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ 𝑖 ∧ 𝑖 ⊆ 𝑘) → 𝑦 ∈ 𝑘)
63	62	adantll 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖) ∧ 𝑖 ⊆ 𝑘) → 𝑦 ∈ 𝑘)
64		ssel2 3933	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘 ∈ 𝐶) → 𝑘 ∈ (Idl‘𝑅))
65	2	idladdcl 38648	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑅 ∈ RingOps ∧ 𝑘 ∈ (Idl‘𝑅)) ∧ (𝑥 ∈ 𝑘 ∧ 𝑦 ∈ 𝑘)) → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑘)
66	65	expr 461	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑅 ∈ RingOps ∧ 𝑘 ∈ (Idl‘𝑅)) ∧ 𝑥 ∈ 𝑘) → (𝑦 ∈ 𝑘 → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑘))
67	66	an32s 664	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ 𝑘 ∈ (Idl‘𝑅)) → (𝑦 ∈ 𝑘 → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑘))
68	64, 67	sylan2 604	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘 ∈ 𝐶)) → (𝑦 ∈ 𝑘 → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑘))
69	68	an42s 673	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) → (𝑦 ∈ 𝑘 → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑘))
70	69	an32s 664	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) → (𝑦 ∈ 𝑘 → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑘))
71	70	imp 411	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑦 ∈ 𝑘) → (𝑥(1st ‘𝑅)𝑦) ∈ 𝑘)
72		simprl 782	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) → 𝑘 ∈ 𝐶)
73	72	ad2antrr 738	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑦 ∈ 𝑘) → 𝑘 ∈ 𝐶)
74		elunii 4878	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑥(1st ‘𝑅)𝑦) ∈ 𝑘 ∧ 𝑘 ∈ 𝐶) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
75	71, 73, 74	syl2anc 595	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑦 ∈ 𝑘) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
76	63, 75	sylan2 604	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ((𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖) ∧ 𝑖 ⊆ 𝑘)) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
77	76	anassrs 472	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖)) ∧ 𝑖 ⊆ 𝑘) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
78	60, 77	jaodan 972	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖)) ∧ (𝑘 ⊆ 𝑖 ∨ 𝑖 ⊆ 𝑘)) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
79	39, 78	syldan 602	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖)) ∧ ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
80	79	an32s 664	. . . . . . . . . . . . 13 ⊢ (((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)) ∧ (𝑖 ∈ 𝐶 ∧ 𝑦 ∈ 𝑖)) → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
81	80	rexlimdvaa 3167	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)) → (∃𝑖 ∈ 𝐶 𝑦 ∈ 𝑖 → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶))
82	33, 81	biimtrid 245	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)) → (𝑦 ∈ ∪ 𝐶 → (𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶))
83	82	ralrimiv 3156	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑗 ∈ 𝐶 (𝑘 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑘)) → ∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
84	32, 83	syldan 602	. . . . . . . . 9 ⊢ ((((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖)) → ∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
85	84	anasss 471	. . . . . . . 8 ⊢ (((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → ∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
86	85	3adantr1 1188	. . . . . . 7 ⊢ (((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → ∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
87	86	an32s 664	. . . . . 6 ⊢ (((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) → ∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶)
88		eqid 2763	. . . . . . . . . . . . . . . . . 18 ⊢ (2nd ‘𝑅) = (2nd ‘𝑅)
89	2, 88, 3	idllmulcl 38649	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ RingOps ∧ 𝑘 ∈ (Idl‘𝑅)) ∧ (𝑥 ∈ 𝑘 ∧ 𝑧 ∈ ran (1st ‘𝑅))) → (𝑧(2nd ‘𝑅)𝑥) ∈ 𝑘)
90	89	exp43 441	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ RingOps → (𝑘 ∈ (Idl‘𝑅) → (𝑥 ∈ 𝑘 → (𝑧 ∈ ran (1st ‘𝑅) → (𝑧(2nd ‘𝑅)𝑥) ∈ 𝑘))))
91	90	com23 87	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ RingOps → (𝑥 ∈ 𝑘 → (𝑘 ∈ (Idl‘𝑅) → (𝑧 ∈ ran (1st ‘𝑅) → (𝑧(2nd ‘𝑅)𝑥) ∈ 𝑘))))
92	91	imp41 430	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ 𝑘 ∈ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝑧(2nd ‘𝑅)𝑥) ∈ 𝑘)
93	64, 92	sylanl2 693	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘 ∈ 𝐶)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝑧(2nd ‘𝑅)𝑥) ∈ 𝑘)
94		simplrr 789	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘 ∈ 𝐶)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → 𝑘 ∈ 𝐶)
95		elunii 4878	. . . . . . . . . . . . 13 ⊢ (((𝑧(2nd ‘𝑅)𝑥) ∈ 𝑘 ∧ 𝑘 ∈ 𝐶) → (𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶)
96	93, 94, 95	syl2anc 595	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘 ∈ 𝐶)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶)
97	2, 88, 3	idlrmulcl 38650	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ RingOps ∧ 𝑘 ∈ (Idl‘𝑅)) ∧ (𝑥 ∈ 𝑘 ∧ 𝑧 ∈ ran (1st ‘𝑅))) → (𝑥(2nd ‘𝑅)𝑧) ∈ 𝑘)
98	97	exp43 441	. . . . . . . . . . . . . . . 16 ⊢ (𝑅 ∈ RingOps → (𝑘 ∈ (Idl‘𝑅) → (𝑥 ∈ 𝑘 → (𝑧 ∈ ran (1st ‘𝑅) → (𝑥(2nd ‘𝑅)𝑧) ∈ 𝑘))))
99	98	com23 87	. . . . . . . . . . . . . . 15 ⊢ (𝑅 ∈ RingOps → (𝑥 ∈ 𝑘 → (𝑘 ∈ (Idl‘𝑅) → (𝑧 ∈ ran (1st ‘𝑅) → (𝑥(2nd ‘𝑅)𝑧) ∈ 𝑘))))
100	99	imp41 430	. . . . . . . . . . . . . 14 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ 𝑘 ∈ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝑥(2nd ‘𝑅)𝑧) ∈ 𝑘)
101	64, 100	sylanl2 693	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘 ∈ 𝐶)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝑥(2nd ‘𝑅)𝑧) ∈ 𝑘)
102		elunii 4878	. . . . . . . . . . . . 13 ⊢ (((𝑥(2nd ‘𝑅)𝑧) ∈ 𝑘 ∧ 𝑘 ∈ 𝐶) → (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶)
103	101, 94, 102	syl2anc 595	. . . . . . . . . . . 12 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘 ∈ 𝐶)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶)
104	96, 103	jca 520	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘 ∈ 𝐶)) ∧ 𝑧 ∈ ran (1st ‘𝑅)) → ((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶))
105	104	ralrimiva 3157	. . . . . . . . . 10 ⊢ (((𝑅 ∈ RingOps ∧ 𝑥 ∈ 𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘 ∈ 𝐶)) → ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶))
106	105	an42s 673	. . . . . . . . 9 ⊢ (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) → ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶))
107	106	an32s 664	. . . . . . . 8 ⊢ (((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶))
108	107	3ad2antr2 1208	. . . . . . 7 ⊢ (((𝑅 ∈ RingOps ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶))
109	108	an32s 664	. . . . . 6 ⊢ (((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) → ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶))
110	87, 109	jca 520	. . . . 5 ⊢ (((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) ∧ (𝑘 ∈ 𝐶 ∧ 𝑥 ∈ 𝑘)) → (∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶 ∧ ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶)))
111	110	rexlimdvaa 3167	. . . 4 ⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → (∃𝑘 ∈ 𝐶 𝑥 ∈ 𝑘 → (∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶 ∧ ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶))))
112	24, 111	biimtrid 245	. . 3 ⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → (𝑥 ∈ ∪ 𝐶 → (∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶 ∧ ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶))))
113	112	ralrimiv 3156	. 2 ⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → ∀𝑥 ∈ ∪ 𝐶(∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶 ∧ ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶)))
114	2, 88, 3, 12	isidl 38643	. . 3 ⊢ (𝑅 ∈ RingOps → (∪ 𝐶 ∈ (Idl‘𝑅) ↔ (∪ 𝐶 ⊆ ran (1st ‘𝑅) ∧ (GId‘(1st ‘𝑅)) ∈ ∪ 𝐶 ∧ ∀𝑥 ∈ ∪ 𝐶(∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶 ∧ ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶)))))
115	114	adantr 485	. 2 ⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → (∪ 𝐶 ∈ (Idl‘𝑅) ↔ (∪ 𝐶 ⊆ ran (1st ‘𝑅) ∧ (GId‘(1st ‘𝑅)) ∈ ∪ 𝐶 ∧ ∀𝑥 ∈ ∪ 𝐶(∀𝑦 ∈ ∪ 𝐶(𝑥(1st ‘𝑅)𝑦) ∈ ∪ 𝐶 ∧ ∀𝑧 ∈ ran (1st ‘𝑅)((𝑧(2nd ‘𝑅)𝑥) ∈ ∪ 𝐶 ∧ (𝑥(2nd ‘𝑅)𝑧) ∈ ∪ 𝐶)))))
116	11, 23, 113, 115	mpbir3and 1361	1 ⊢ ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖 ∈ 𝐶 ∀𝑗 ∈ 𝐶 (𝑖 ⊆ 𝑗 ∨ 𝑗 ⊆ 𝑖))) → ∪ 𝐶 ∈ (Idl‘𝑅))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 860   ∧ w3a 1103   ∈ wcel 2143   ≠ wne 2958  ∀wral 3079  ∃wrex 3089   ⊆ wss 3906  ∅c0 4287  ∪ cuni 4873  ran crn 5664  ‘cfv 6538  (class class class)co 7412  1^st c1st 7985  2^nd c2nd 7986  GIdcgi 30820  RingOpscrngo 38523  Idlcidl 38636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pow 5338  ax-pr 5406  ax-un 7734

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-iota 6494  df-fun 6540  df-fv 6546  df-ov 7415  df-idl 38639

This theorem is referenced by: (None)