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

Theorem intidl 34160
Description: The intersection of a nonempty collection of ideals is an ideal. (Contributed by Jeff Madsen, 10-Jun-2010.)
Assertion
Ref Expression
intidl ((𝑅 ∈ RingOps ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅)) → 𝐶 ∈ (Idl‘𝑅))

Proof of Theorem intidl
Dummy variables 𝑖 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 intssuni 4633 . . . 4 (𝐶 ≠ ∅ → 𝐶 𝐶)
213ad2ant2 1128 . . 3 ((𝑅 ∈ RingOps ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅)) → 𝐶 𝐶)
3 ssel2 3747 . . . . . . . 8 ((𝐶 ⊆ (Idl‘𝑅) ∧ 𝑖𝐶) → 𝑖 ∈ (Idl‘𝑅))
4 eqid 2771 . . . . . . . . 9 (1st𝑅) = (1st𝑅)
5 eqid 2771 . . . . . . . . 9 ran (1st𝑅) = ran (1st𝑅)
64, 5idlss 34147 . . . . . . . 8 ((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) → 𝑖 ⊆ ran (1st𝑅))
73, 6sylan2 580 . . . . . . 7 ((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑖𝐶)) → 𝑖 ⊆ ran (1st𝑅))
87anassrs 458 . . . . . 6 (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑖𝐶) → 𝑖 ⊆ ran (1st𝑅))
98ralrimiva 3115 . . . . 5 ((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∀𝑖𝐶 𝑖 ⊆ ran (1st𝑅))
1093adant2 1125 . . . 4 ((𝑅 ∈ RingOps ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∀𝑖𝐶 𝑖 ⊆ ran (1st𝑅))
11 unissb 4605 . . . 4 ( 𝐶 ⊆ ran (1st𝑅) ↔ ∀𝑖𝐶 𝑖 ⊆ ran (1st𝑅))
1210, 11sylibr 224 . . 3 ((𝑅 ∈ RingOps ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅)) → 𝐶 ⊆ ran (1st𝑅))
132, 12sstrd 3762 . 2 ((𝑅 ∈ RingOps ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅)) → 𝐶 ⊆ ran (1st𝑅))
14 eqid 2771 . . . . . . . 8 (GId‘(1st𝑅)) = (GId‘(1st𝑅))
154, 14idl0cl 34149 . . . . . . 7 ((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) → (GId‘(1st𝑅)) ∈ 𝑖)
163, 15sylan2 580 . . . . . 6 ((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑖𝐶)) → (GId‘(1st𝑅)) ∈ 𝑖)
1716anassrs 458 . . . . 5 (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑖𝐶) → (GId‘(1st𝑅)) ∈ 𝑖)
1817ralrimiva 3115 . . . 4 ((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∀𝑖𝐶 (GId‘(1st𝑅)) ∈ 𝑖)
19 fvex 6342 . . . . 5 (GId‘(1st𝑅)) ∈ V
2019elint2 4618 . . . 4 ((GId‘(1st𝑅)) ∈ 𝐶 ↔ ∀𝑖𝐶 (GId‘(1st𝑅)) ∈ 𝑖)
2118, 20sylibr 224 . . 3 ((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) → (GId‘(1st𝑅)) ∈ 𝐶)
22213adant2 1125 . 2 ((𝑅 ∈ RingOps ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅)) → (GId‘(1st𝑅)) ∈ 𝐶)
23 vex 3354 . . . . . 6 𝑥 ∈ V
2423elint2 4618 . . . . 5 (𝑥 𝐶 ↔ ∀𝑖𝐶 𝑥𝑖)
25 vex 3354 . . . . . . . . . 10 𝑦 ∈ V
2625elint2 4618 . . . . . . . . 9 (𝑦 𝐶 ↔ ∀𝑖𝐶 𝑦𝑖)
27 r19.26 3212 . . . . . . . . . . 11 (∀𝑖𝐶 (𝑥𝑖𝑦𝑖) ↔ (∀𝑖𝐶 𝑥𝑖 ∧ ∀𝑖𝐶 𝑦𝑖))
284idladdcl 34150 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ (𝑥𝑖𝑦𝑖)) → (𝑥(1st𝑅)𝑦) ∈ 𝑖)
2928ex 397 . . . . . . . . . . . . . . 15 ((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) → ((𝑥𝑖𝑦𝑖) → (𝑥(1st𝑅)𝑦) ∈ 𝑖))
303, 29sylan2 580 . . . . . . . . . . . . . 14 ((𝑅 ∈ RingOps ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑖𝐶)) → ((𝑥𝑖𝑦𝑖) → (𝑥(1st𝑅)𝑦) ∈ 𝑖))
3130anassrs 458 . . . . . . . . . . . . 13 (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑖𝐶) → ((𝑥𝑖𝑦𝑖) → (𝑥(1st𝑅)𝑦) ∈ 𝑖))
3231ralimdva 3111 . . . . . . . . . . . 12 ((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) → (∀𝑖𝐶 (𝑥𝑖𝑦𝑖) → ∀𝑖𝐶 (𝑥(1st𝑅)𝑦) ∈ 𝑖))
33 ovex 6823 . . . . . . . . . . . . 13 (𝑥(1st𝑅)𝑦) ∈ V
3433elint2 4618 . . . . . . . . . . . 12 ((𝑥(1st𝑅)𝑦) ∈ 𝐶 ↔ ∀𝑖𝐶 (𝑥(1st𝑅)𝑦) ∈ 𝑖)
3532, 34syl6ibr 242 . . . . . . . . . . 11 ((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) → (∀𝑖𝐶 (𝑥𝑖𝑦𝑖) → (𝑥(1st𝑅)𝑦) ∈ 𝐶))
3627, 35syl5bir 233 . . . . . . . . . 10 ((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) → ((∀𝑖𝐶 𝑥𝑖 ∧ ∀𝑖𝐶 𝑦𝑖) → (𝑥(1st𝑅)𝑦) ∈ 𝐶))
3736expdimp 440 . . . . . . . . 9 (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑖𝐶 𝑥𝑖) → (∀𝑖𝐶 𝑦𝑖 → (𝑥(1st𝑅)𝑦) ∈ 𝐶))
3826, 37syl5bi 232 . . . . . . . 8 (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑖𝐶 𝑥𝑖) → (𝑦 𝐶 → (𝑥(1st𝑅)𝑦) ∈ 𝐶))
3938ralrimiv 3114 . . . . . . 7 (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑖𝐶 𝑥𝑖) → ∀𝑦 𝐶(𝑥(1st𝑅)𝑦) ∈ 𝐶)
40 eqid 2771 . . . . . . . . . . . . . . . . . . . 20 (2nd𝑅) = (2nd𝑅)
414, 40, 5idllmulcl 34151 . . . . . . . . . . . . . . . . . . 19 (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ (𝑥𝑖𝑧 ∈ ran (1st𝑅))) → (𝑧(2nd𝑅)𝑥) ∈ 𝑖)
4241anass1rs 634 . . . . . . . . . . . . . . . . . 18 ((((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st𝑅)) ∧ 𝑥𝑖) → (𝑧(2nd𝑅)𝑥) ∈ 𝑖)
4342ex 397 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝑥𝑖 → (𝑧(2nd𝑅)𝑥) ∈ 𝑖))
4443an32s 631 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ RingOps ∧ 𝑧 ∈ ran (1st𝑅)) ∧ 𝑖 ∈ (Idl‘𝑅)) → (𝑥𝑖 → (𝑧(2nd𝑅)𝑥) ∈ 𝑖))
453, 44sylan2 580 . . . . . . . . . . . . . . 15 (((𝑅 ∈ RingOps ∧ 𝑧 ∈ ran (1st𝑅)) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑖𝐶)) → (𝑥𝑖 → (𝑧(2nd𝑅)𝑥) ∈ 𝑖))
4645an4s 639 . . . . . . . . . . . . . 14 (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑧 ∈ ran (1st𝑅) ∧ 𝑖𝐶)) → (𝑥𝑖 → (𝑧(2nd𝑅)𝑥) ∈ 𝑖))
4746anassrs 458 . . . . . . . . . . . . 13 ((((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st𝑅)) ∧ 𝑖𝐶) → (𝑥𝑖 → (𝑧(2nd𝑅)𝑥) ∈ 𝑖))
4847ralimdva 3111 . . . . . . . . . . . 12 (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st𝑅)) → (∀𝑖𝐶 𝑥𝑖 → ∀𝑖𝐶 (𝑧(2nd𝑅)𝑥) ∈ 𝑖))
4948imp 393 . . . . . . . . . . 11 ((((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st𝑅)) ∧ ∀𝑖𝐶 𝑥𝑖) → ∀𝑖𝐶 (𝑧(2nd𝑅)𝑥) ∈ 𝑖)
50 ovex 6823 . . . . . . . . . . . 12 (𝑧(2nd𝑅)𝑥) ∈ V
5150elint2 4618 . . . . . . . . . . 11 ((𝑧(2nd𝑅)𝑥) ∈ 𝐶 ↔ ∀𝑖𝐶 (𝑧(2nd𝑅)𝑥) ∈ 𝑖)
5249, 51sylibr 224 . . . . . . . . . 10 ((((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st𝑅)) ∧ ∀𝑖𝐶 𝑥𝑖) → (𝑧(2nd𝑅)𝑥) ∈ 𝐶)
534, 40, 5idlrmulcl 34152 . . . . . . . . . . . . . . . . . . 19 (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ (𝑥𝑖𝑧 ∈ ran (1st𝑅))) → (𝑥(2nd𝑅)𝑧) ∈ 𝑖)
5453anass1rs 634 . . . . . . . . . . . . . . . . . 18 ((((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st𝑅)) ∧ 𝑥𝑖) → (𝑥(2nd𝑅)𝑧) ∈ 𝑖)
5554ex 397 . . . . . . . . . . . . . . . . 17 (((𝑅 ∈ RingOps ∧ 𝑖 ∈ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st𝑅)) → (𝑥𝑖 → (𝑥(2nd𝑅)𝑧) ∈ 𝑖))
5655an32s 631 . . . . . . . . . . . . . . . 16 (((𝑅 ∈ RingOps ∧ 𝑧 ∈ ran (1st𝑅)) ∧ 𝑖 ∈ (Idl‘𝑅)) → (𝑥𝑖 → (𝑥(2nd𝑅)𝑧) ∈ 𝑖))
573, 56sylan2 580 . . . . . . . . . . . . . . 15 (((𝑅 ∈ RingOps ∧ 𝑧 ∈ ran (1st𝑅)) ∧ (𝐶 ⊆ (Idl‘𝑅) ∧ 𝑖𝐶)) → (𝑥𝑖 → (𝑥(2nd𝑅)𝑧) ∈ 𝑖))
5857an4s 639 . . . . . . . . . . . . . 14 (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ (𝑧 ∈ ran (1st𝑅) ∧ 𝑖𝐶)) → (𝑥𝑖 → (𝑥(2nd𝑅)𝑧) ∈ 𝑖))
5958anassrs 458 . . . . . . . . . . . . 13 ((((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st𝑅)) ∧ 𝑖𝐶) → (𝑥𝑖 → (𝑥(2nd𝑅)𝑧) ∈ 𝑖))
6059ralimdva 3111 . . . . . . . . . . . 12 (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st𝑅)) → (∀𝑖𝐶 𝑥𝑖 → ∀𝑖𝐶 (𝑥(2nd𝑅)𝑧) ∈ 𝑖))
6160imp 393 . . . . . . . . . . 11 ((((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st𝑅)) ∧ ∀𝑖𝐶 𝑥𝑖) → ∀𝑖𝐶 (𝑥(2nd𝑅)𝑧) ∈ 𝑖)
62 ovex 6823 . . . . . . . . . . . 12 (𝑥(2nd𝑅)𝑧) ∈ V
6362elint2 4618 . . . . . . . . . . 11 ((𝑥(2nd𝑅)𝑧) ∈ 𝐶 ↔ ∀𝑖𝐶 (𝑥(2nd𝑅)𝑧) ∈ 𝑖)
6461, 63sylibr 224 . . . . . . . . . 10 ((((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st𝑅)) ∧ ∀𝑖𝐶 𝑥𝑖) → (𝑥(2nd𝑅)𝑧) ∈ 𝐶)
6552, 64jca 501 . . . . . . . . 9 ((((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ 𝑧 ∈ ran (1st𝑅)) ∧ ∀𝑖𝐶 𝑥𝑖) → ((𝑧(2nd𝑅)𝑥) ∈ 𝐶 ∧ (𝑥(2nd𝑅)𝑧) ∈ 𝐶))
6665an32s 631 . . . . . . . 8 ((((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑖𝐶 𝑥𝑖) ∧ 𝑧 ∈ ran (1st𝑅)) → ((𝑧(2nd𝑅)𝑥) ∈ 𝐶 ∧ (𝑥(2nd𝑅)𝑧) ∈ 𝐶))
6766ralrimiva 3115 . . . . . . 7 (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑖𝐶 𝑥𝑖) → ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ 𝐶 ∧ (𝑥(2nd𝑅)𝑧) ∈ 𝐶))
6839, 67jca 501 . . . . . 6 (((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) ∧ ∀𝑖𝐶 𝑥𝑖) → (∀𝑦 𝐶(𝑥(1st𝑅)𝑦) ∈ 𝐶 ∧ ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ 𝐶 ∧ (𝑥(2nd𝑅)𝑧) ∈ 𝐶)))
6968ex 397 . . . . 5 ((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) → (∀𝑖𝐶 𝑥𝑖 → (∀𝑦 𝐶(𝑥(1st𝑅)𝑦) ∈ 𝐶 ∧ ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ 𝐶 ∧ (𝑥(2nd𝑅)𝑧) ∈ 𝐶))))
7024, 69syl5bi 232 . . . 4 ((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) → (𝑥 𝐶 → (∀𝑦 𝐶(𝑥(1st𝑅)𝑦) ∈ 𝐶 ∧ ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ 𝐶 ∧ (𝑥(2nd𝑅)𝑧) ∈ 𝐶))))
7170ralrimiv 3114 . . 3 ((𝑅 ∈ RingOps ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∀𝑥 𝐶(∀𝑦 𝐶(𝑥(1st𝑅)𝑦) ∈ 𝐶 ∧ ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ 𝐶 ∧ (𝑥(2nd𝑅)𝑧) ∈ 𝐶)))
72713adant2 1125 . 2 ((𝑅 ∈ RingOps ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅)) → ∀𝑥 𝐶(∀𝑦 𝐶(𝑥(1st𝑅)𝑦) ∈ 𝐶 ∧ ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ 𝐶 ∧ (𝑥(2nd𝑅)𝑧) ∈ 𝐶)))
734, 40, 5, 14isidl 34145 . . 3 (𝑅 ∈ RingOps → ( 𝐶 ∈ (Idl‘𝑅) ↔ ( 𝐶 ⊆ ran (1st𝑅) ∧ (GId‘(1st𝑅)) ∈ 𝐶 ∧ ∀𝑥 𝐶(∀𝑦 𝐶(𝑥(1st𝑅)𝑦) ∈ 𝐶 ∧ ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ 𝐶 ∧ (𝑥(2nd𝑅)𝑧) ∈ 𝐶)))))
74733ad2ant1 1127 . 2 ((𝑅 ∈ RingOps ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅)) → ( 𝐶 ∈ (Idl‘𝑅) ↔ ( 𝐶 ⊆ ran (1st𝑅) ∧ (GId‘(1st𝑅)) ∈ 𝐶 ∧ ∀𝑥 𝐶(∀𝑦 𝐶(𝑥(1st𝑅)𝑦) ∈ 𝐶 ∧ ∀𝑧 ∈ ran (1st𝑅)((𝑧(2nd𝑅)𝑥) ∈ 𝐶 ∧ (𝑥(2nd𝑅)𝑧) ∈ 𝐶)))))
7513, 22, 72, 74mpbir3and 1427 1 ((𝑅 ∈ RingOps ∧ 𝐶 ≠ ∅ ∧ 𝐶 ⊆ (Idl‘𝑅)) → 𝐶 ∈ (Idl‘𝑅))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382  w3a 1071  wcel 2145  wne 2943  wral 3061  wss 3723  c0 4063   cuni 4574   cint 4611  ran crn 5250  cfv 6031  (class class class)co 6793  1st c1st 7313  2nd c2nd 7314  GIdcgi 27684  RingOpscrngo 34025  Idlcidl 34138
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-int 4612  df-br 4787  df-opab 4847  df-mpt 4864  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-iota 5994  df-fun 6033  df-fv 6039  df-ov 6796  df-idl 34141
This theorem is referenced by:  inidl  34161  igenidl  34194
  Copyright terms: Public domain W3C validator