Users' Mathboxes Mathbox for Jeff Madsen < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  unichnidl Structured version   Visualization version   GIF version

Theorem unichnidl 33497
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.
StepHypRef Expression
1 dfss3 3577 . . . . 5 (𝐶 ⊆ (Idl‘𝑅) ↔ ∀𝑖𝐶 𝑖 ∈ (Idl‘𝑅))
2 eqid 2621 . . . . . . . . 9 (1st𝑅) = (1st𝑅)
3 eqid 2621 . . . . . . . . 9 ran (1st𝑅) = ran (1st𝑅)
42, 3idlss 33482 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) → 𝑖 ⊆ ran (1st𝑅))
54ex 450 . . . . . . 7 (𝑅 ∈ RingOps → (𝑖 ∈ (Idl‘𝑅) → 𝑖 ⊆ ran (1st𝑅)))
65ralimdv 2958 . . . . . 6 (𝑅 ∈ RingOps → (∀𝑖𝐶 𝑖 ∈ (Idl‘𝑅) → ∀𝑖𝐶 𝑖 ⊆ ran (1st𝑅)))
76imp 445 . . . . 5 ((𝑅 ∈ RingOps ∧ ∀𝑖𝐶 𝑖 ∈ (Idl‘𝑅)) → ∀𝑖𝐶 𝑖 ⊆ ran (1st𝑅))
81, 7sylan2b 492 . . . 4 ((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∀𝑖𝐶 𝑖 ⊆ ran (1st𝑅))
9 unissb 4440 . . . 4 ( 𝐶 ⊆ ran (1st𝑅) ↔ ∀𝑖𝐶 𝑖 ⊆ ran (1st𝑅))
108, 9sylibr 224 . . 3 ((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) → 𝐶 ⊆ ran (1st𝑅))
11103ad2antr2 1225 . 2 ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖))) → 𝐶 ⊆ ran (1st𝑅))
12 eqid 2621 . . . . . . . . . . 11 (GId‘(1st𝑅)) = (GId‘(1st𝑅))
132, 12idl0cl 33484 . . . . . . . . . 10 ((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) → (GId‘(1st𝑅)) ∈ 𝑖)
1413ex 450 . . . . . . . . 9 (𝑅 ∈ RingOps → (𝑖 ∈ (Idl‘𝑅) → (GId‘(1st𝑅)) ∈ 𝑖))
1514ralimdv 2958 . . . . . . . 8 (𝑅 ∈ RingOps → (∀𝑖𝐶 𝑖 ∈ (Idl‘𝑅) → ∀𝑖𝐶 (GId‘(1st𝑅)) ∈ 𝑖))
1615imp 445 . . . . . . 7 ((𝑅 ∈ RingOps ∧ ∀𝑖𝐶 𝑖 ∈ (Idl‘𝑅)) → ∀𝑖𝐶 (GId‘(1st𝑅)) ∈ 𝑖)
171, 16sylan2b 492 . . . . . 6 ((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∀𝑖𝐶 (GId‘(1st𝑅)) ∈ 𝑖)
18 r19.2z 4037 . . . . . 6 ((𝐶 ≠ ∅ ∧ ∀𝑖𝐶 (GId‘(1st𝑅)) ∈ 𝑖) → ∃𝑖𝐶 (GId‘(1st𝑅)) ∈ 𝑖)
1917, 18sylan2 491 . . . . 5 ((𝐶 ≠ ∅ ∧ (𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅))) → ∃𝑖𝐶 (GId‘(1st𝑅)) ∈ 𝑖)
2019an12s 842 . . . 4 ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅))) → ∃𝑖𝐶 (GId‘(1st𝑅)) ∈ 𝑖)
21 eluni2 4411 . . . 4 ((GId‘(1st𝑅)) ∈ 𝐶 ↔ ∃𝑖𝐶 (GId‘(1st𝑅)) ∈ 𝑖)
2220, 21sylibr 224 . . 3 ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅))) → (GId‘(1st𝑅)) ∈ 𝐶)
23223adantr3 1220 . 2 ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖))) → (GId‘(1st𝑅)) ∈ 𝐶)
24 eluni2 4411 . . . 4 (𝑥 𝐶 ↔ ∃𝑘𝐶 𝑥𝑘)
25 sseq1 3610 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑘 → (𝑖𝑗𝑘𝑗))
26 sseq2 3611 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑘 → (𝑗𝑖𝑗𝑘))
2725, 26orbi12d 745 . . . . . . . . . . . . . . 15 (𝑖 = 𝑘 → ((𝑖𝑗𝑗𝑖) ↔ (𝑘𝑗𝑗𝑘)))
2827ralbidv 2981 . . . . . . . . . . . . . 14 (𝑖 = 𝑘 → (∀𝑗𝐶 (𝑖𝑗𝑗𝑖) ↔ ∀𝑗𝐶 (𝑘𝑗𝑗𝑘)))
2928rspcv 3294 . . . . . . . . . . . . 13 (𝑘𝐶 → (∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖) → ∀𝑗𝐶 (𝑘𝑗𝑗𝑘)))
3029adantr 481 . . . . . . . . . . . 12 ((𝑘𝐶𝑥𝑘) → (∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖) → ∀𝑗𝐶 (𝑘𝑗𝑗𝑘)))
3130ad2antlr 762 . . . . . . . . . . 11 (((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) → (∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖) → ∀𝑗𝐶 (𝑘𝑗𝑗𝑘)))
3231imp 445 . . . . . . . . . 10 ((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖)) → ∀𝑗𝐶 (𝑘𝑗𝑗𝑘))
33 eluni2 4411 . . . . . . . . . . . 12 (𝑦 𝐶 ↔ ∃𝑖𝐶 𝑦𝑖)
34 sseq2 3611 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑖 → (𝑘𝑗𝑘𝑖))
35 sseq1 3610 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑖 → (𝑗𝑘𝑖𝑘))
3634, 35orbi12d 745 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑖 → ((𝑘𝑗𝑗𝑘) ↔ (𝑘𝑖𝑖𝑘)))
3736rspcv 3294 . . . . . . . . . . . . . . . . 17 (𝑖𝐶 → (∀𝑗𝐶 (𝑘𝑗𝑗𝑘) → (𝑘𝑖𝑖𝑘)))
3837ad2antrl 763 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖𝐶𝑦𝑖)) → (∀𝑗𝐶 (𝑘𝑗𝑗𝑘) → (𝑘𝑖𝑖𝑘)))
3938imp 445 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖𝐶𝑦𝑖)) ∧ ∀𝑗𝐶 (𝑘𝑗𝑗𝑘)) → (𝑘𝑖𝑖𝑘))
40 ssel2 3582 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘𝑖𝑥𝑘) → 𝑥𝑖)
4140ancoms 469 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥𝑘𝑘𝑖) → 𝑥𝑖)
4241adantll 749 . . . . . . . . . . . . . . . . . . . . 21 (((𝑘𝐶𝑥𝑘) ∧ 𝑘𝑖) → 𝑥𝑖)
43 ssel2 3582 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐶 ⊆ (Idl‘𝑅) ∧ 𝑖𝐶) → 𝑖 ∈ (Idl‘𝑅))
442idladdcl 33485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ (𝑥𝑖𝑦𝑖)) → (𝑥(1st𝑅)𝑦) ∈ 𝑖)
4544ancom2s 843 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ (𝑦𝑖𝑥𝑖)) → (𝑥(1st𝑅)𝑦) ∈ 𝑖)
4645expr 642 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ 𝑦𝑖) → (𝑥𝑖 → (𝑥(1st𝑅)𝑦) ∈ 𝑖))
4746an32s 845 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑅 ∈ RingOps ∧ 𝑦𝑖) ∧ 𝑖 ∈ (Idl‘𝑅)) → (𝑥𝑖 → (𝑥(1st𝑅)𝑦) ∈ 𝑖))
4843, 47sylan2 491 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑅 ∈ RingOps ∧ 𝑦𝑖) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑖𝐶)) → (𝑥𝑖 → (𝑥(1st𝑅)𝑦) ∈ 𝑖))
4948an42s 869 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖𝐶𝑦𝑖)) → (𝑥𝑖 → (𝑥(1st𝑅)𝑦) ∈ 𝑖))
5049anasss 678 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖𝐶𝑦𝑖))) → (𝑥𝑖 → (𝑥(1st𝑅)𝑦) ∈ 𝑖))
5150imp 445 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖𝐶𝑦𝑖))) ∧ 𝑥𝑖) → (𝑥(1st𝑅)𝑦) ∈ 𝑖)
52 simprl 793 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖𝐶𝑦𝑖)) → 𝑖𝐶)
5352ad2antlr 762 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖𝐶𝑦𝑖))) ∧ 𝑥𝑖) → 𝑖𝐶)
54 elunii 4412 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑥(1st𝑅)𝑦) ∈ 𝑖𝑖𝐶) → (𝑥(1st𝑅)𝑦) ∈ 𝐶)
5551, 53, 54syl2anc 692 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖𝐶𝑦𝑖))) ∧ 𝑥𝑖) → (𝑥(1st𝑅)𝑦) ∈ 𝐶)
5642, 55sylan2 491 . . . . . . . . . . . . . . . . . . . 20 (((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖𝐶𝑦𝑖))) ∧ ((𝑘𝐶𝑥𝑘) ∧ 𝑘𝑖)) → (𝑥(1st𝑅)𝑦) ∈ 𝐶)
5756expr 642 . . . . . . . . . . . . . . . . . . 19 (((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖𝐶𝑦𝑖))) ∧ (𝑘𝐶𝑥𝑘)) → (𝑘𝑖 → (𝑥(1st𝑅)𝑦) ∈ 𝐶))
5857an32s 845 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖𝐶𝑦𝑖))) → (𝑘𝑖 → (𝑥(1st𝑅)𝑦) ∈ 𝐶))
5958anassrs 679 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖𝐶𝑦𝑖)) → (𝑘𝑖 → (𝑥(1st𝑅)𝑦) ∈ 𝐶))
6059imp 445 . . . . . . . . . . . . . . . 16 (((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖𝐶𝑦𝑖)) ∧ 𝑘𝑖) → (𝑥(1st𝑅)𝑦) ∈ 𝐶)
61 ssel2 3582 . . . . . . . . . . . . . . . . . . . 20 ((𝑖𝑘𝑦𝑖) → 𝑦𝑘)
6261ancoms 469 . . . . . . . . . . . . . . . . . . 19 ((𝑦𝑖𝑖𝑘) → 𝑦𝑘)
6362adantll 749 . . . . . . . . . . . . . . . . . 18 (((𝑖𝐶𝑦𝑖) ∧ 𝑖𝑘) → 𝑦𝑘)
64 ssel2 3582 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘𝐶) → 𝑘 ∈ (Idl‘𝑅))
652idladdcl 33485 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑅 ∈ RingOps ∧ 𝑘 ∈ (Idl‘𝑅)) ∧ (𝑥𝑘𝑦𝑘)) → (𝑥(1st𝑅)𝑦) ∈ 𝑘)
6665expr 642 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑅 ∈ RingOps ∧ 𝑘 ∈ (Idl‘𝑅)) ∧ 𝑥𝑘) → (𝑦𝑘 → (𝑥(1st𝑅)𝑦) ∈ 𝑘))
6766an32s 845 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑅 ∈ RingOps ∧ 𝑥𝑘) ∧ 𝑘 ∈ (Idl‘𝑅)) → (𝑦𝑘 → (𝑥(1st𝑅)𝑦) ∈ 𝑘))
6864, 67sylan2 491 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑅 ∈ RingOps ∧ 𝑥𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘𝐶)) → (𝑦𝑘 → (𝑥(1st𝑅)𝑦) ∈ 𝑘))
6968an42s 869 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑘𝐶𝑥𝑘)) → (𝑦𝑘 → (𝑥(1st𝑅)𝑦) ∈ 𝑘))
7069an32s 845 . . . . . . . . . . . . . . . . . . . 20 (((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) → (𝑦𝑘 → (𝑥(1st𝑅)𝑦) ∈ 𝑘))
7170imp 445 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑦𝑘) → (𝑥(1st𝑅)𝑦) ∈ 𝑘)
72 simprl 793 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) → 𝑘𝐶)
7372ad2antrr 761 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑦𝑘) → 𝑘𝐶)
74 elunii 4412 . . . . . . . . . . . . . . . . . . 19 (((𝑥(1st𝑅)𝑦) ∈ 𝑘𝑘𝐶) → (𝑥(1st𝑅)𝑦) ∈ 𝐶)
7571, 73, 74syl2anc 692 . . . . . . . . . . . . . . . . . 18 ((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑦𝑘) → (𝑥(1st𝑅)𝑦) ∈ 𝐶)
7663, 75sylan2 491 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ((𝑖𝐶𝑦𝑖) ∧ 𝑖𝑘)) → (𝑥(1st𝑅)𝑦) ∈ 𝐶)
7776anassrs 679 . . . . . . . . . . . . . . . 16 (((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖𝐶𝑦𝑖)) ∧ 𝑖𝑘) → (𝑥(1st𝑅)𝑦) ∈ 𝐶)
7860, 77jaodan 825 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖𝐶𝑦𝑖)) ∧ (𝑘𝑖𝑖𝑘)) → (𝑥(1st𝑅)𝑦) ∈ 𝐶)
7939, 78syldan 487 . . . . . . . . . . . . . 14 (((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖𝐶𝑦𝑖)) ∧ ∀𝑗𝐶 (𝑘𝑗𝑗𝑘)) → (𝑥(1st𝑅)𝑦) ∈ 𝐶)
8079an32s 845 . . . . . . . . . . . . 13 (((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑗𝐶 (𝑘𝑗𝑗𝑘)) ∧ (𝑖𝐶𝑦𝑖)) → (𝑥(1st𝑅)𝑦) ∈ 𝐶)
8180rexlimdvaa 3026 . . . . . . . . . . . 12 ((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑗𝐶 (𝑘𝑗𝑗𝑘)) → (∃𝑖𝐶 𝑦𝑖 → (𝑥(1st𝑅)𝑦) ∈ 𝐶))
8233, 81syl5bi 232 . . . . . . . . . . 11 ((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑗𝐶 (𝑘𝑗𝑗𝑘)) → (𝑦 𝐶 → (𝑥(1st𝑅)𝑦) ∈ 𝐶))
8382ralrimiv 2960 . . . . . . . . . 10 ((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑗𝐶 (𝑘𝑗𝑗𝑘)) → ∀𝑦 𝐶(𝑥(1st𝑅)𝑦) ∈ 𝐶)
8432, 83syldan 487 . . . . . . . . 9 ((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖)) → ∀𝑦 𝐶(𝑥(1st𝑅)𝑦) ∈ 𝐶)
8584anasss 678 . . . . . . . 8 (((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖))) → ∀𝑦 𝐶(𝑥(1st𝑅)𝑦) ∈ 𝐶)
86853adantr1 1218 . . . . . . 7 (((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖))) → ∀𝑦 𝐶(𝑥(1st𝑅)𝑦) ∈ 𝐶)
8786an32s 845 . . . . . 6 (((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖))) ∧ (𝑘𝐶𝑥𝑘)) → ∀𝑦 𝐶(𝑥(1st𝑅)𝑦) ∈ 𝐶)
88 eqid 2621 . . . . . . . . . . . . . . . . . 18 (2nd𝑅) = (2nd𝑅)
892, 88, 3idllmulcl 33486 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ RingOps ∧ 𝑘 ∈ (Idl‘𝑅)) ∧ (𝑥𝑘𝑧 ∈ ran (1st𝑅))) → (𝑧(2nd𝑅)𝑥) ∈ 𝑘)
9089exp43 639 . . . . . . . . . . . . . . . 16 (𝑅 ∈ RingOps → (𝑘 ∈ (Idl‘𝑅) → (𝑥𝑘 → (𝑧 ∈ ran (1st𝑅) → (𝑧(2nd𝑅)𝑥) ∈ 𝑘))))
9190com23 86 . . . . . . . . . . . . . . 15 (𝑅 ∈ RingOps → (𝑥𝑘 → (𝑘 ∈ (Idl‘𝑅) → (𝑧 ∈ ran (1st𝑅) → (𝑧(2nd𝑅)𝑥) ∈ 𝑘))))
9291imp41 618 . . . . . . . . . . . . . 14 ((((𝑅 ∈ RingOps ∧ 𝑥𝑘) ∧ 𝑘 ∈ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝑧(2nd𝑅)𝑥) ∈ 𝑘)
9364, 92sylanl2 682 . . . . . . . . . . . . 13 ((((𝑅 ∈ RingOps ∧ 𝑥𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘𝐶)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝑧(2nd𝑅)𝑥) ∈ 𝑘)
94 simplrr 800 . . . . . . . . . . . . 13 ((((𝑅 ∈ RingOps ∧ 𝑥𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘𝐶)) ∧ 𝑧 ∈ ran (1st𝑅)) → 𝑘𝐶)
95 elunii 4412 . . . . . . . . . . . . 13 (((𝑧(2nd𝑅)𝑥) ∈ 𝑘𝑘𝐶) → (𝑧(2nd𝑅)𝑥) ∈ 𝐶)
9693, 94, 95syl2anc 692 . . . . . . . . . . . 12 ((((𝑅 ∈ RingOps ∧ 𝑥𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘𝐶)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝑧(2nd𝑅)𝑥) ∈ 𝐶)
972, 88, 3idlrmulcl 33487 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ RingOps ∧ 𝑘 ∈ (Idl‘𝑅)) ∧ (𝑥𝑘𝑧 ∈ ran (1st𝑅))) → (𝑥(2nd𝑅)𝑧) ∈ 𝑘)
9897exp43 639 . . . . . . . . . . . . . . . 16 (𝑅 ∈ RingOps → (𝑘 ∈ (Idl‘𝑅) → (𝑥𝑘 → (𝑧 ∈ ran (1st𝑅) → (𝑥(2nd𝑅)𝑧) ∈ 𝑘))))
9998com23 86 . . . . . . . . . . . . . . 15 (𝑅 ∈ RingOps → (𝑥𝑘 → (𝑘 ∈ (Idl‘𝑅) → (𝑧 ∈ ran (1st𝑅) → (𝑥(2nd𝑅)𝑧) ∈ 𝑘))))
10099imp41 618 . . . . . . . . . . . . . 14 ((((𝑅 ∈ RingOps ∧ 𝑥𝑘) ∧ 𝑘 ∈ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝑥(2nd𝑅)𝑧) ∈ 𝑘)
10164, 100sylanl2 682 . . . . . . . . . . . . 13 ((((𝑅 ∈ RingOps ∧ 𝑥𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘𝐶)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝑥(2nd𝑅)𝑧) ∈ 𝑘)
102 elunii 4412 . . . . . . . . . . . . 13 (((𝑥(2nd𝑅)𝑧) ∈ 𝑘𝑘𝐶) → (𝑥(2nd𝑅)𝑧) ∈ 𝐶)
103101, 94, 102syl2anc 692 . . . . . . . . . . . 12 ((((𝑅 ∈ RingOps ∧ 𝑥𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘𝐶)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝑥(2nd𝑅)𝑧) ∈ 𝐶)
10496, 103jca 554 . . . . . . . . . . 11 ((((𝑅 ∈ RingOps ∧ 𝑥𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘𝐶)) ∧ 𝑧 ∈ ran (1st𝑅)) → ((𝑧(2nd𝑅)𝑥) ∈ 𝐶 ∧ (𝑥(2nd𝑅)𝑧) ∈ 𝐶))
105104ralrimiva 2961 . . . . . . . . . 10 (((𝑅 ∈ RingOps ∧ 𝑥𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘𝐶)) → ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ 𝐶 ∧ (𝑥(2nd𝑅)𝑧) ∈ 𝐶))
106105an42s 869 . . . . . . . . 9 (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑘𝐶𝑥𝑘)) → ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ 𝐶 ∧ (𝑥(2nd𝑅)𝑧) ∈ 𝐶))
107106an32s 845 . . . . . . . 8 (((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ 𝐶 ∧ (𝑥(2nd𝑅)𝑧) ∈ 𝐶))
1081073ad2antr2 1225 . . . . . . 7 (((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖))) → ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ 𝐶 ∧ (𝑥(2nd𝑅)𝑧) ∈ 𝐶))
109108an32s 845 . . . . . 6 (((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖))) ∧ (𝑘𝐶𝑥𝑘)) → ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ 𝐶 ∧ (𝑥(2nd𝑅)𝑧) ∈ 𝐶))
11087, 109jca 554 . . . . 5 (((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖))) ∧ (𝑘𝐶𝑥𝑘)) → (∀𝑦 𝐶(𝑥(1st𝑅)𝑦) ∈ 𝐶 ∧ ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ 𝐶 ∧ (𝑥(2nd𝑅)𝑧) ∈ 𝐶)))
111110rexlimdvaa 3026 . . . 4 ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖))) → (∃𝑘𝐶 𝑥𝑘 → (∀𝑦 𝐶(𝑥(1st𝑅)𝑦) ∈ 𝐶 ∧ ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ 𝐶 ∧ (𝑥(2nd𝑅)𝑧) ∈ 𝐶))))
11224, 111syl5bi 232 . . 3 ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖))) → (𝑥 𝐶 → (∀𝑦 𝐶(𝑥(1st𝑅)𝑦) ∈ 𝐶 ∧ ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ 𝐶 ∧ (𝑥(2nd𝑅)𝑧) ∈ 𝐶))))
113112ralrimiv 2960 . 2 ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖))) → ∀𝑥 𝐶(∀𝑦 𝐶(𝑥(1st𝑅)𝑦) ∈ 𝐶 ∧ ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ 𝐶 ∧ (𝑥(2nd𝑅)𝑧) ∈ 𝐶)))
1142, 88, 3, 12isidl 33480 . . 3 (𝑅 ∈ RingOps → ( 𝐶 ∈ (Idl‘𝑅) ↔ ( 𝐶 ⊆ ran (1st𝑅) ∧ (GId‘(1st𝑅)) ∈ 𝐶 ∧ ∀𝑥 𝐶(∀𝑦 𝐶(𝑥(1st𝑅)𝑦) ∈ 𝐶 ∧ ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ 𝐶 ∧ (𝑥(2nd𝑅)𝑧) ∈ 𝐶)))))
115114adantr 481 . 2 ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖))) → ( 𝐶 ∈ (Idl‘𝑅) ↔ ( 𝐶 ⊆ ran (1st𝑅) ∧ (GId‘(1st𝑅)) ∈ 𝐶 ∧ ∀𝑥 𝐶(∀𝑦 𝐶(𝑥(1st𝑅)𝑦) ∈ 𝐶 ∧ ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ 𝐶 ∧ (𝑥(2nd𝑅)𝑧) ∈ 𝐶)))))
11611, 23, 113, 115mpbir3and 1243 1 ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖))) → 𝐶 ∈ (Idl‘𝑅))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wo 383  wa 384  w3a 1036  wcel 1987  wne 2790  wral 2907  wrex 2908  wss 3559  c0 3896   cuni 4407  ran crn 5080  cfv 5852  (class class class)co 6610  1st c1st 7118  2nd c2nd 7119  GIdcgi 27214  RingOpscrngo 33360  Idlcidl 33473
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3191  df-sbc 3422  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-br 4619  df-opab 4679  df-mpt 4680  df-id 4994  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-iota 5815  df-fun 5854  df-fv 5860  df-ov 6613  df-idl 33476
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator