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 36985
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 3970 . . . . 5 (𝐶 ⊆ (Idl‘𝑅) ↔ ∀𝑖𝐶 𝑖 ∈ (Idl‘𝑅))
2 eqid 2732 . . . . . . . . 9 (1st𝑅) = (1st𝑅)
3 eqid 2732 . . . . . . . . 9 ran (1st𝑅) = ran (1st𝑅)
42, 3idlss 36970 . . . . . . . 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 4943 . . . 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 36972 . . . . . . . . . 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 4494 . . . . . 6 ((𝐶 ≠ ∅ ∧ ∀𝑖𝐶 (GId‘(1st𝑅)) ∈ 𝑖) → ∃𝑖𝐶 (GId‘(1st𝑅)) ∈ 𝑖)
1917, 18sylan2 593 . . . . 5 ((𝐶 ≠ ∅ ∧ (𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅))) → ∃𝑖𝐶 (GId‘(1st𝑅)) ∈ 𝑖)
2019an12s 647 . . . 4 ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅))) → ∃𝑖𝐶 (GId‘(1st𝑅)) ∈ 𝑖)
21 eluni2 4912 . . . 4 ((GId‘(1st𝑅)) ∈ 𝐶 ↔ ∃𝑖𝐶 (GId‘(1st𝑅)) ∈ 𝑖)
2220, 21sylibr 233 . . 3 ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅))) → (GId‘(1st𝑅)) ∈ 𝐶)
23223adantr3 1171 . 2 ((𝑅 ∈ RingOps ∧ (𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅) ∧ ∀𝑖𝐶𝑗𝐶 (𝑖𝑗𝑗𝑖))) → (GId‘(1st𝑅)) ∈ 𝐶)
24 eluni2 4912 . . . 4 (𝑥 𝐶 ↔ ∃𝑘𝐶 𝑥𝑘)
25 sseq1 4007 . . . . . . . . . . . . . . . 16 (𝑖 = 𝑘 → (𝑖𝑗𝑘𝑗))
26 sseq2 4008 . . . . . . . . . . . . . . . 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 4912 . . . . . . . . . . . 12 (𝑦 𝐶 ↔ ∃𝑖𝐶 𝑦𝑖)
34 sseq2 4008 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑖 → (𝑘𝑗𝑘𝑖))
35 sseq1 4007 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝑖 → (𝑗𝑘𝑖𝑘))
3634, 35orbi12d 917 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝑖 → ((𝑘𝑗𝑗𝑘) ↔ (𝑘𝑖𝑖𝑘)))
3736rspcv 3608 . . . . . . . . . . . . . . . . 17 (𝑖𝐶 → (∀𝑗𝐶 (𝑘𝑗𝑗𝑘) → (𝑘𝑖𝑖𝑘)))
3837ad2antrl 726 . . . . . . . . . . . . . . . 16 ((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖𝐶𝑦𝑖)) → (∀𝑗𝐶 (𝑘𝑗𝑗𝑘) → (𝑘𝑖𝑖𝑘)))
3938imp 407 . . . . . . . . . . . . . . 15 (((((𝑅 ∈ RingOps ∧ (𝑘𝐶𝑥𝑘)) ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑖𝐶𝑦𝑖)) ∧ ∀𝑗𝐶 (𝑘𝑗𝑗𝑘)) → (𝑘𝑖𝑖𝑘))
40 ssel2 3977 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑘𝑖𝑥𝑘) → 𝑥𝑖)
4140ancoms 459 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥𝑘𝑘𝑖) → 𝑥𝑖)
4241adantll 712 . . . . . . . . . . . . . . . . . . . . 21 (((𝑘𝐶𝑥𝑘) ∧ 𝑘𝑖) → 𝑥𝑖)
43 ssel2 3977 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐶 ⊆ (Idl‘𝑅) ∧ 𝑖𝐶) → 𝑖 ∈ (Idl‘𝑅))
442idladdcl 36973 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 4913 . . . . . . . . . . . . . . . . . . . . . 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 3977 . . . . . . . . . . . . . . . . . . . 20 ((𝑖𝑘𝑦𝑖) → 𝑦𝑘)
6261ancoms 459 . . . . . . . . . . . . . . . . . . 19 ((𝑦𝑖𝑖𝑘) → 𝑦𝑘)
6362adantll 712 . . . . . . . . . . . . . . . . . 18 (((𝑖𝐶𝑦𝑖) ∧ 𝑖𝑘) → 𝑦𝑘)
64 ssel2 3977 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘𝐶) → 𝑘 ∈ (Idl‘𝑅))
652idladdcl 36973 . . . . . . . . . . . . . . . . . . . . . . . . 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 4913 . . . . . . . . . . . . . . . . . . 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 36974 . . . . . . . . . . . . . . . . 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 4913 . . . . . . . . . . . . 13 (((𝑧(2nd𝑅)𝑥) ∈ 𝑘𝑘𝐶) → (𝑧(2nd𝑅)𝑥) ∈ 𝐶)
9693, 94, 95syl2anc 584 . . . . . . . . . . . 12 ((((𝑅 ∈ RingOps ∧ 𝑥𝑘) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑘𝐶)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝑧(2nd𝑅)𝑥) ∈ 𝐶)
972, 88, 3idlrmulcl 36975 . . . . . . . . . . . . . . . . 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 4913 . . . . . . . . . . . . 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 36968 . . 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 3948  c0 4322   cuni 4908  ran crn 5677  cfv 6543  (class class class)co 7411  1st c1st 7975  2nd c2nd 7976  GIdcgi 29781  RingOpscrngo 36848  Idlcidl 36961
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 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727
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 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-iota 6495  df-fun 6545  df-fv 6551  df-ov 7414  df-idl 36964
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator