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 36887
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 3969 . . . . 5 (𝐶 ⊆ (Idl‘𝑅) ↔ ∀𝑖𝐶 𝑖 ∈ (Idl‘𝑅))
2 eqid 2732 . . . . . . . . 9 (1st𝑅) = (1st𝑅)
3 eqid 2732 . . . . . . . . 9 ran (1st𝑅) = ran (1st𝑅)
42, 3idlss 36872 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) → 𝑖 ⊆ ran (1st𝑅))
54ex 413 . . . . . . 7 (𝑅 ∈ RingOps → (𝑖 ∈ (Idl‘𝑅) → 𝑖 ⊆ ran (1st𝑅)))
65ralimdv 3169 . . . . . 6 (𝑅 ∈ RingOps → (∀𝑖𝐶 𝑖 ∈ (Idl‘𝑅) → ∀𝑖𝐶 𝑖 ⊆ ran (1st𝑅)))
76imp 407 . . . . 5 ((𝑅 ∈ RingOps ∧ ∀𝑖𝐶 𝑖 ∈ (Idl‘𝑅)) → ∀𝑖𝐶 𝑖 ⊆ ran (1st𝑅))
81, 7sylan2b 594 . . . 4 ((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∀𝑖𝐶 𝑖 ⊆ ran (1st𝑅))
9 unissb 4942 . . . 4 ( 𝐶 ⊆ ran (1st𝑅) ↔ ∀𝑖𝐶 𝑖 ⊆ ran (1st𝑅))
108, 9sylibr 233 . . 3 ((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) → 𝐶 ⊆ ran (1st𝑅))
11103ad2antr2 1189 . 2 ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖))) → 𝐶 ⊆ ran (1st𝑅))
12 eqid 2732 . . . . . . . . . . 11 (GId‘(1st𝑅)) = (GId‘(1st𝑅))
132, 12idl0cl 36874 . . . . . . . . . 10 ((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) → (GId‘(1st𝑅)) ∈ 𝑖)
1413ex 413 . . . . . . . . 9 (𝑅 ∈ RingOps → (𝑖 ∈ (Idl‘𝑅) → (GId‘(1st𝑅)) ∈ 𝑖))
1514ralimdv 3169 . . . . . . . 8 (𝑅 ∈ RingOps → (∀𝑖𝐶 𝑖 ∈ (Idl‘𝑅) → ∀𝑖𝐶 (GId‘(1st𝑅)) ∈ 𝑖))
1615imp 407 . . . . . . 7 ((𝑅 ∈ RingOps ∧ ∀𝑖𝐶 𝑖 ∈ (Idl‘𝑅)) → ∀𝑖𝐶 (GId‘(1st𝑅)) ∈ 𝑖)
171, 16sylan2b 594 . . . . . 6 ((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∀𝑖𝐶 (GId‘(1st𝑅)) ∈ 𝑖)
18 r19.2z 4493 . . . . . 6 ((𝐶 ≠ ∅ ∧ ∀𝑖𝐶 (GId‘(1st𝑅)) ∈ 𝑖) → ∃𝑖𝐶 (GId‘(1st𝑅)) ∈ 𝑖)
1917, 18sylan2 593 . . . . 5 ((𝐶 ≠ ∅ ∧ (𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅))) → ∃𝑖𝐶 (GId‘(1st𝑅)) ∈ 𝑖)
2019an12s 647 . . . 4 ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅))) → ∃𝑖𝐶 (GId‘(1st𝑅)) ∈ 𝑖)
21 eluni2 4911 . . . 4 ((GId‘(1st𝑅)) ∈ 𝐶 ↔ ∃𝑖𝐶 (GId‘(1st𝑅)) ∈ 𝑖)
2220, 21sylibr 233 . . 3 ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅))) → (GId‘(1st𝑅)) ∈ 𝐶)
23223adantr3 1171 . 2 ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖))) → (GId‘(1st𝑅)) ∈ 𝐶)
24 eluni2 4911 . . . 4 (𝑥 𝐶 ↔ ∃𝑘𝐶 𝑥𝑘)
25 sseq1 4006 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑘 → (𝑖𝑗𝑘𝑗))
26 sseq2 4007 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑘 → (𝑗𝑖𝑗𝑘))
2725, 26orbi12d 917 . . . . . . . . . . . . . . 15 (𝑖 = 𝑘 → ((𝑖𝑗𝑗𝑖) ↔ (𝑘𝑗𝑗𝑘)))
2827ralbidv 3177 . . . . . . . . . . . . . 14 (𝑖 = 𝑘 → (∀𝑗𝐶 (𝑖𝑗𝑗𝑖) ↔ ∀𝑗𝐶 (𝑘𝑗𝑗𝑘)))
2928rspcv 3608 . . . . . . . . . . . . 13 (𝑘𝐶 → (∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖) → ∀𝑗𝐶 (𝑘𝑗𝑗𝑘)))
3029adantr 481 . . . . . . . . . . . 12 ((𝑘𝐶𝑥𝑘) → (∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖) → ∀𝑗𝐶 (𝑘𝑗𝑗𝑘)))
3130ad2antlr 725 . . . . . . . . . . 11 (((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) → (∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖) → ∀𝑗𝐶 (𝑘𝑗𝑗𝑘)))
3231imp 407 . . . . . . . . . 10 ((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖)) → ∀𝑗𝐶 (𝑘𝑗𝑗𝑘))
33 eluni2 4911 . . . . . . . . . . . 12 (𝑦 𝐶 ↔ ∃𝑖𝐶 𝑦𝑖)
34 sseq2 4007 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑖 → (𝑘𝑗𝑘𝑖))
35 sseq1 4006 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑖 → (𝑗𝑘𝑖𝑘))
3634, 35orbi12d 917 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑖 → ((𝑘𝑗𝑗𝑘) ↔ (𝑘𝑖𝑖𝑘)))
3736rspcv 3608 . . . . . . . . . . . . . . . . 17 (𝑖𝐶 → (∀𝑗𝐶 (𝑘𝑗𝑗𝑘) → (𝑘𝑖𝑖𝑘)))
3837ad2antrl 726 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖𝐶𝑦𝑖)) → (∀𝑗𝐶 (𝑘𝑗𝑗𝑘) → (𝑘𝑖𝑖𝑘)))
3938imp 407 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖𝐶𝑦𝑖)) ∧ ∀𝑗𝐶 (𝑘𝑗𝑗𝑘)) → (𝑘𝑖𝑖𝑘))
40 ssel2 3976 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘𝑖𝑥𝑘) → 𝑥𝑖)
4140ancoms 459 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥𝑘𝑘𝑖) → 𝑥𝑖)
4241adantll 712 . . . . . . . . . . . . . . . . . . . . 21 (((𝑘𝐶𝑥𝑘) ∧ 𝑘𝑖) → 𝑥𝑖)
43 ssel2 3976 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐶 ⊆ (Idl‘𝑅) ∧ 𝑖𝐶) → 𝑖 ∈ (Idl‘𝑅))
442idladdcl 36875 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ (𝑥𝑖𝑦𝑖)) → (𝑥(1st𝑅)𝑦) ∈ 𝑖)
4544ancom2s 648 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ (𝑦𝑖𝑥𝑖)) → (𝑥(1st𝑅)𝑦) ∈ 𝑖)
4645expr 457 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ 𝑦𝑖) → (𝑥𝑖 → (𝑥(1st𝑅)𝑦) ∈ 𝑖))
4746an32s 650 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑅 ∈ RingOps ∧ 𝑦𝑖) ∧ 𝑖 ∈ (Idl‘𝑅)) → (𝑥𝑖 → (𝑥(1st𝑅)𝑦) ∈ 𝑖))
4843, 47sylan2 593 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑅 ∈ RingOps ∧ 𝑦𝑖) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑖𝐶)) → (𝑥𝑖 → (𝑥(1st𝑅)𝑦) ∈ 𝑖))
4948an42s 659 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖𝐶𝑦𝑖)) → (𝑥𝑖 → (𝑥(1st𝑅)𝑦) ∈ 𝑖))
5049anasss 467 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖𝐶𝑦𝑖))) → (𝑥𝑖 → (𝑥(1st𝑅)𝑦) ∈ 𝑖))
5150imp 407 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖𝐶𝑦𝑖))) ∧ 𝑥𝑖) → (𝑥(1st𝑅)𝑦) ∈ 𝑖)
52 simprl 769 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖𝐶𝑦𝑖)) → 𝑖𝐶)
5352ad2antlr 725 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖𝐶𝑦𝑖))) ∧ 𝑥𝑖) → 𝑖𝐶)
54 elunii 4912 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑥(1st𝑅)𝑦) ∈ 𝑖𝑖𝐶) → (𝑥(1st𝑅)𝑦) ∈ 𝐶)
5551, 53, 54syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖𝐶𝑦𝑖))) ∧ 𝑥𝑖) → (𝑥(1st𝑅)𝑦) ∈ 𝐶)
5642, 55sylan2 593 . . . . . . . . . . . . . . . . . . . 20 (((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖𝐶𝑦𝑖))) ∧ ((𝑘𝐶𝑥𝑘) ∧ 𝑘𝑖)) → (𝑥(1st𝑅)𝑦) ∈ 𝐶)
5756expr 457 . . . . . . . . . . . . . . . . . . 19 (((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖𝐶𝑦𝑖))) ∧ (𝑘𝐶𝑥𝑘)) → (𝑘𝑖 → (𝑥(1st𝑅)𝑦) ∈ 𝐶))
5857an32s 650 . . . . . . . . . . . . . . . . . 18 (((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ (𝑖𝐶𝑦𝑖))) → (𝑘𝑖 → (𝑥(1st𝑅)𝑦) ∈ 𝐶))
5958anassrs 468 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖𝐶𝑦𝑖)) → (𝑘𝑖 → (𝑥(1st𝑅)𝑦) ∈ 𝐶))
6059imp 407 . . . . . . . . . . . . . . . 16 (((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖𝐶𝑦𝑖)) ∧ 𝑘𝑖) → (𝑥(1st𝑅)𝑦) ∈ 𝐶)
61 ssel2 3976 . . . . . . . . . . . . . . . . . . . 20 ((𝑖𝑘𝑦𝑖) → 𝑦𝑘)
6261ancoms 459 . . . . . . . . . . . . . . . . . . 19 ((𝑦𝑖𝑖𝑘) → 𝑦𝑘)
6362adantll 712 . . . . . . . . . . . . . . . . . 18 (((𝑖𝐶𝑦𝑖) ∧ 𝑖𝑘) → 𝑦𝑘)
64 ssel2 3976 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘𝐶) → 𝑘 ∈ (Idl‘𝑅))
652idladdcl 36875 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑅 ∈ RingOps ∧ 𝑘 ∈ (Idl‘𝑅)) ∧ (𝑥𝑘𝑦𝑘)) → (𝑥(1st𝑅)𝑦) ∈ 𝑘)
6665expr 457 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑅 ∈ RingOps ∧ 𝑘 ∈ (Idl‘𝑅)) ∧ 𝑥𝑘) → (𝑦𝑘 → (𝑥(1st𝑅)𝑦) ∈ 𝑘))
6766an32s 650 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑅 ∈ RingOps ∧ 𝑥𝑘) ∧ 𝑘 ∈ (Idl‘𝑅)) → (𝑦𝑘 → (𝑥(1st𝑅)𝑦) ∈ 𝑘))
6864, 67sylan2 593 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑅 ∈ RingOps ∧ 𝑥𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘𝐶)) → (𝑦𝑘 → (𝑥(1st𝑅)𝑦) ∈ 𝑘))
6968an42s 659 . . . . . . . . . . . . . . . . . . . . 21 (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑘𝐶𝑥𝑘)) → (𝑦𝑘 → (𝑥(1st𝑅)𝑦) ∈ 𝑘))
7069an32s 650 . . . . . . . . . . . . . . . . . . . 20 (((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) → (𝑦𝑘 → (𝑥(1st𝑅)𝑦) ∈ 𝑘))
7170imp 407 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑦𝑘) → (𝑥(1st𝑅)𝑦) ∈ 𝑘)
72 simprl 769 . . . . . . . . . . . . . . . . . . . 20 ((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) → 𝑘𝐶)
7372ad2antrr 724 . . . . . . . . . . . . . . . . . . 19 ((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑦𝑘) → 𝑘𝐶)
74 elunii 4912 . . . . . . . . . . . . . . . . . . 19 (((𝑥(1st𝑅)𝑦) ∈ 𝑘𝑘𝐶) → (𝑥(1st𝑅)𝑦) ∈ 𝐶)
7571, 73, 74syl2anc 584 . . . . . . . . . . . . . . . . . 18 ((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑦𝑘) → (𝑥(1st𝑅)𝑦) ∈ 𝐶)
7663, 75sylan2 593 . . . . . . . . . . . . . . . . 17 ((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ((𝑖𝐶𝑦𝑖) ∧ 𝑖𝑘)) → (𝑥(1st𝑅)𝑦) ∈ 𝐶)
7776anassrs 468 . . . . . . . . . . . . . . . 16 (((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖𝐶𝑦𝑖)) ∧ 𝑖𝑘) → (𝑥(1st𝑅)𝑦) ∈ 𝐶)
7860, 77jaodan 956 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖𝐶𝑦𝑖)) ∧ (𝑘𝑖𝑖𝑘)) → (𝑥(1st𝑅)𝑦) ∈ 𝐶)
7939, 78syldan 591 . . . . . . . . . . . . . 14 (((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖𝐶𝑦𝑖)) ∧ ∀𝑗𝐶 (𝑘𝑗𝑗𝑘)) → (𝑥(1st𝑅)𝑦) ∈ 𝐶)
8079an32s 650 . . . . . . . . . . . . 13 (((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑗𝐶 (𝑘𝑗𝑗𝑘)) ∧ (𝑖𝐶𝑦𝑖)) → (𝑥(1st𝑅)𝑦) ∈ 𝐶)
8180rexlimdvaa 3156 . . . . . . . . . . . 12 ((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑗𝐶 (𝑘𝑗𝑗𝑘)) → (∃𝑖𝐶 𝑦𝑖 → (𝑥(1st𝑅)𝑦) ∈ 𝐶))
8233, 81biimtrid 241 . . . . . . . . . . 11 ((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑗𝐶 (𝑘𝑗𝑗𝑘)) → (𝑦 𝐶 → (𝑥(1st𝑅)𝑦) ∈ 𝐶))
8382ralrimiv 3145 . . . . . . . . . 10 ((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑗𝐶 (𝑘𝑗𝑗𝑘)) → ∀𝑦 𝐶(𝑥(1st𝑅)𝑦) ∈ 𝐶)
8432, 83syldan 591 . . . . . . . . 9 ((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖)) → ∀𝑦 𝐶(𝑥(1st𝑅)𝑦) ∈ 𝐶)
8584anasss 467 . . . . . . . 8 (((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖))) → ∀𝑦 𝐶(𝑥(1st𝑅)𝑦) ∈ 𝐶)
86853adantr1 1169 . . . . . . 7 (((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖))) → ∀𝑦 𝐶(𝑥(1st𝑅)𝑦) ∈ 𝐶)
8786an32s 650 . . . . . 6 (((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖))) ∧ (𝑘𝐶𝑥𝑘)) → ∀𝑦 𝐶(𝑥(1st𝑅)𝑦) ∈ 𝐶)
88 eqid 2732 . . . . . . . . . . . . . . . . . 18 (2nd𝑅) = (2nd𝑅)
892, 88, 3idllmulcl 36876 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ RingOps ∧ 𝑘 ∈ (Idl‘𝑅)) ∧ (𝑥𝑘𝑧 ∈ ran (1st𝑅))) → (𝑧(2nd𝑅)𝑥) ∈ 𝑘)
9089exp43 437 . . . . . . . . . . . . . . . 16 (𝑅 ∈ RingOps → (𝑘 ∈ (Idl‘𝑅) → (𝑥𝑘 → (𝑧 ∈ ran (1st𝑅) → (𝑧(2nd𝑅)𝑥) ∈ 𝑘))))
9190com23 86 . . . . . . . . . . . . . . 15 (𝑅 ∈ RingOps → (𝑥𝑘 → (𝑘 ∈ (Idl‘𝑅) → (𝑧 ∈ ran (1st𝑅) → (𝑧(2nd𝑅)𝑥) ∈ 𝑘))))
9291imp41 426 . . . . . . . . . . . . . 14 ((((𝑅 ∈ RingOps ∧ 𝑥𝑘) ∧ 𝑘 ∈ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝑧(2nd𝑅)𝑥) ∈ 𝑘)
9364, 92sylanl2 679 . . . . . . . . . . . . 13 ((((𝑅 ∈ RingOps ∧ 𝑥𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘𝐶)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝑧(2nd𝑅)𝑥) ∈ 𝑘)
94 simplrr 776 . . . . . . . . . . . . 13 ((((𝑅 ∈ RingOps ∧ 𝑥𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘𝐶)) ∧ 𝑧 ∈ ran (1st𝑅)) → 𝑘𝐶)
95 elunii 4912 . . . . . . . . . . . . 13 (((𝑧(2nd𝑅)𝑥) ∈ 𝑘𝑘𝐶) → (𝑧(2nd𝑅)𝑥) ∈ 𝐶)
9693, 94, 95syl2anc 584 . . . . . . . . . . . 12 ((((𝑅 ∈ RingOps ∧ 𝑥𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘𝐶)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝑧(2nd𝑅)𝑥) ∈ 𝐶)
972, 88, 3idlrmulcl 36877 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ RingOps ∧ 𝑘 ∈ (Idl‘𝑅)) ∧ (𝑥𝑘𝑧 ∈ ran (1st𝑅))) → (𝑥(2nd𝑅)𝑧) ∈ 𝑘)
9897exp43 437 . . . . . . . . . . . . . . . 16 (𝑅 ∈ RingOps → (𝑘 ∈ (Idl‘𝑅) → (𝑥𝑘 → (𝑧 ∈ ran (1st𝑅) → (𝑥(2nd𝑅)𝑧) ∈ 𝑘))))
9998com23 86 . . . . . . . . . . . . . . 15 (𝑅 ∈ RingOps → (𝑥𝑘 → (𝑘 ∈ (Idl‘𝑅) → (𝑧 ∈ ran (1st𝑅) → (𝑥(2nd𝑅)𝑧) ∈ 𝑘))))
10099imp41 426 . . . . . . . . . . . . . 14 ((((𝑅 ∈ RingOps ∧ 𝑥𝑘) ∧ 𝑘 ∈ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝑥(2nd𝑅)𝑧) ∈ 𝑘)
10164, 100sylanl2 679 . . . . . . . . . . . . 13 ((((𝑅 ∈ RingOps ∧ 𝑥𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘𝐶)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝑥(2nd𝑅)𝑧) ∈ 𝑘)
102 elunii 4912 . . . . . . . . . . . . 13 (((𝑥(2nd𝑅)𝑧) ∈ 𝑘𝑘𝐶) → (𝑥(2nd𝑅)𝑧) ∈ 𝐶)
103101, 94, 102syl2anc 584 . . . . . . . . . . . 12 ((((𝑅 ∈ RingOps ∧ 𝑥𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘𝐶)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝑥(2nd𝑅)𝑧) ∈ 𝐶)
10496, 103jca 512 . . . . . . . . . . 11 ((((𝑅 ∈ RingOps ∧ 𝑥𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘𝐶)) ∧ 𝑧 ∈ ran (1st𝑅)) → ((𝑧(2nd𝑅)𝑥) ∈ 𝐶 ∧ (𝑥(2nd𝑅)𝑧) ∈ 𝐶))
105104ralrimiva 3146 . . . . . . . . . 10 (((𝑅 ∈ RingOps ∧ 𝑥𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘𝐶)) → ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ 𝐶 ∧ (𝑥(2nd𝑅)𝑧) ∈ 𝐶))
106105an42s 659 . . . . . . . . 9 (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑘𝐶𝑥𝑘)) → ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ 𝐶 ∧ (𝑥(2nd𝑅)𝑧) ∈ 𝐶))
107106an32s 650 . . . . . . . 8 (((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ 𝐶 ∧ (𝑥(2nd𝑅)𝑧) ∈ 𝐶))
1081073ad2antr2 1189 . . . . . . 7 (((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖))) → ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ 𝐶 ∧ (𝑥(2nd𝑅)𝑧) ∈ 𝐶))
109108an32s 650 . . . . . 6 (((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖))) ∧ (𝑘𝐶𝑥𝑘)) → ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ 𝐶 ∧ (𝑥(2nd𝑅)𝑧) ∈ 𝐶))
11087, 109jca 512 . . . . 5 (((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖))) ∧ (𝑘𝐶𝑥𝑘)) → (∀𝑦 𝐶(𝑥(1st𝑅)𝑦) ∈ 𝐶 ∧ ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ 𝐶 ∧ (𝑥(2nd𝑅)𝑧) ∈ 𝐶)))
111110rexlimdvaa 3156 . . . 4 ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖))) → (∃𝑘𝐶 𝑥𝑘 → (∀𝑦 𝐶(𝑥(1st𝑅)𝑦) ∈ 𝐶 ∧ ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ 𝐶 ∧ (𝑥(2nd𝑅)𝑧) ∈ 𝐶))))
11224, 111biimtrid 241 . . 3 ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖))) → (𝑥 𝐶 → (∀𝑦 𝐶(𝑥(1st𝑅)𝑦) ∈ 𝐶 ∧ ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ 𝐶 ∧ (𝑥(2nd𝑅)𝑧) ∈ 𝐶))))
113112ralrimiv 3145 . 2 ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖))) → ∀𝑥 𝐶(∀𝑦 𝐶(𝑥(1st𝑅)𝑦) ∈ 𝐶 ∧ ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ 𝐶 ∧ (𝑥(2nd𝑅)𝑧) ∈ 𝐶)))
1142, 88, 3, 12isidl 36870 . . 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 1342 1 ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖))) → 𝐶 ∈ (Idl‘𝑅))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  wo 845  w3a 1087  wcel 2106  wne 2940  wral 3061  wrex 3070  wss 3947  c0 4321   cuni 4907  ran crn 5676  cfv 6540  (class class class)co 7405  1st c1st 7969  2nd c2nd 7970  GIdcgi 29730  RingOpscrngo 36750  Idlcidl 36863
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  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 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-iota 6492  df-fun 6542  df-fv 6548  df-ov 7408  df-idl 36866
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator