| Step |
Hyp |
Ref |
Expression |
| 1 |
|
zarclsx.1 |
⊢ 𝑉 = ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } ) |
| 2 |
|
crngring |
⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring ) |
| 3 |
2
|
ad4antr |
⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ) ∧ 𝑆 ≠ ∅ ) ∧ 𝑟 ∈ 𝒫 ( LIdeal ‘ 𝑅 ) ) ∧ 𝑆 = ( 𝑉 “ 𝑟 ) ) → 𝑅 ∈ Ring ) |
| 4 |
|
elpwi |
⊢ ( 𝑟 ∈ 𝒫 ( LIdeal ‘ 𝑅 ) → 𝑟 ⊆ ( LIdeal ‘ 𝑅 ) ) |
| 5 |
4
|
adantl |
⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ) ∧ 𝑆 ≠ ∅ ) ∧ 𝑟 ∈ 𝒫 ( LIdeal ‘ 𝑅 ) ) → 𝑟 ⊆ ( LIdeal ‘ 𝑅 ) ) |
| 6 |
5
|
adantr |
⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ) ∧ 𝑆 ≠ ∅ ) ∧ 𝑟 ∈ 𝒫 ( LIdeal ‘ 𝑅 ) ) ∧ 𝑆 = ( 𝑉 “ 𝑟 ) ) → 𝑟 ⊆ ( LIdeal ‘ 𝑅 ) ) |
| 7 |
6
|
sselda |
⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ) ∧ 𝑆 ≠ ∅ ) ∧ 𝑟 ∈ 𝒫 ( LIdeal ‘ 𝑅 ) ) ∧ 𝑆 = ( 𝑉 “ 𝑟 ) ) ∧ 𝑖 ∈ 𝑟 ) → 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ) |
| 8 |
|
eqid |
⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 ) |
| 9 |
|
eqid |
⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 ) |
| 10 |
8 9
|
lidlss |
⊢ ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) → 𝑖 ⊆ ( Base ‘ 𝑅 ) ) |
| 11 |
7 10
|
syl |
⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ) ∧ 𝑆 ≠ ∅ ) ∧ 𝑟 ∈ 𝒫 ( LIdeal ‘ 𝑅 ) ) ∧ 𝑆 = ( 𝑉 “ 𝑟 ) ) ∧ 𝑖 ∈ 𝑟 ) → 𝑖 ⊆ ( Base ‘ 𝑅 ) ) |
| 12 |
11
|
ralrimiva |
⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ) ∧ 𝑆 ≠ ∅ ) ∧ 𝑟 ∈ 𝒫 ( LIdeal ‘ 𝑅 ) ) ∧ 𝑆 = ( 𝑉 “ 𝑟 ) ) → ∀ 𝑖 ∈ 𝑟 𝑖 ⊆ ( Base ‘ 𝑅 ) ) |
| 13 |
|
unissb |
⊢ ( ∪ 𝑟 ⊆ ( Base ‘ 𝑅 ) ↔ ∀ 𝑖 ∈ 𝑟 𝑖 ⊆ ( Base ‘ 𝑅 ) ) |
| 14 |
12 13
|
sylibr |
⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ) ∧ 𝑆 ≠ ∅ ) ∧ 𝑟 ∈ 𝒫 ( LIdeal ‘ 𝑅 ) ) ∧ 𝑆 = ( 𝑉 “ 𝑟 ) ) → ∪ 𝑟 ⊆ ( Base ‘ 𝑅 ) ) |
| 15 |
|
eqid |
⊢ ( RSpan ‘ 𝑅 ) = ( RSpan ‘ 𝑅 ) |
| 16 |
15 8 9
|
rspcl |
⊢ ( ( 𝑅 ∈ Ring ∧ ∪ 𝑟 ⊆ ( Base ‘ 𝑅 ) ) → ( ( RSpan ‘ 𝑅 ) ‘ ∪ 𝑟 ) ∈ ( LIdeal ‘ 𝑅 ) ) |
| 17 |
3 14 16
|
syl2anc |
⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ) ∧ 𝑆 ≠ ∅ ) ∧ 𝑟 ∈ 𝒫 ( LIdeal ‘ 𝑅 ) ) ∧ 𝑆 = ( 𝑉 “ 𝑟 ) ) → ( ( RSpan ‘ 𝑅 ) ‘ ∪ 𝑟 ) ∈ ( LIdeal ‘ 𝑅 ) ) |
| 18 |
|
sseq1 |
⊢ ( 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ ∪ 𝑟 ) → ( 𝑖 ⊆ 𝑗 ↔ ( ( RSpan ‘ 𝑅 ) ‘ ∪ 𝑟 ) ⊆ 𝑗 ) ) |
| 19 |
18
|
rabbidv |
⊢ ( 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ ∪ 𝑟 ) → { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ ( ( RSpan ‘ 𝑅 ) ‘ ∪ 𝑟 ) ⊆ 𝑗 } ) |
| 20 |
19
|
eqeq2d |
⊢ ( 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ ∪ 𝑟 ) → ( ∩ 𝑆 = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } ↔ ∩ 𝑆 = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ ( ( RSpan ‘ 𝑅 ) ‘ ∪ 𝑟 ) ⊆ 𝑗 } ) ) |
| 21 |
20
|
adantl |
⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ) ∧ 𝑆 ≠ ∅ ) ∧ 𝑟 ∈ 𝒫 ( LIdeal ‘ 𝑅 ) ) ∧ 𝑆 = ( 𝑉 “ 𝑟 ) ) ∧ 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ ∪ 𝑟 ) ) → ( ∩ 𝑆 = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } ↔ ∩ 𝑆 = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ ( ( RSpan ‘ 𝑅 ) ‘ ∪ 𝑟 ) ⊆ 𝑗 } ) ) |
| 22 |
|
simpr |
⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ) ∧ 𝑆 ≠ ∅ ) ∧ 𝑟 ∈ 𝒫 ( LIdeal ‘ 𝑅 ) ) ∧ 𝑆 = ( 𝑉 “ 𝑟 ) ) → 𝑆 = ( 𝑉 “ 𝑟 ) ) |
| 23 |
22
|
inteqd |
⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ) ∧ 𝑆 ≠ ∅ ) ∧ 𝑟 ∈ 𝒫 ( LIdeal ‘ 𝑅 ) ) ∧ 𝑆 = ( 𝑉 “ 𝑟 ) ) → ∩ 𝑆 = ∩ ( 𝑉 “ 𝑟 ) ) |
| 24 |
1
|
funmpt2 |
⊢ Fun 𝑉 |
| 25 |
24
|
a1i |
⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ) ∧ 𝑆 ≠ ∅ ) ∧ 𝑟 ∈ 𝒫 ( LIdeal ‘ 𝑅 ) ) ∧ 𝑆 = ( 𝑉 “ 𝑟 ) ) → Fun 𝑉 ) |
| 26 |
|
fvex |
⊢ ( PrmIdeal ‘ 𝑅 ) ∈ V |
| 27 |
26
|
rabex |
⊢ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } ∈ V |
| 28 |
27 1
|
dmmpti |
⊢ dom 𝑉 = ( LIdeal ‘ 𝑅 ) |
| 29 |
6 28
|
sseqtrrdi |
⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ) ∧ 𝑆 ≠ ∅ ) ∧ 𝑟 ∈ 𝒫 ( LIdeal ‘ 𝑅 ) ) ∧ 𝑆 = ( 𝑉 “ 𝑟 ) ) → 𝑟 ⊆ dom 𝑉 ) |
| 30 |
|
intimafv |
⊢ ( ( Fun 𝑉 ∧ 𝑟 ⊆ dom 𝑉 ) → ∩ ( 𝑉 “ 𝑟 ) = ∩ 𝑙 ∈ 𝑟 ( 𝑉 ‘ 𝑙 ) ) |
| 31 |
25 29 30
|
syl2anc |
⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ) ∧ 𝑆 ≠ ∅ ) ∧ 𝑟 ∈ 𝒫 ( LIdeal ‘ 𝑅 ) ) ∧ 𝑆 = ( 𝑉 “ 𝑟 ) ) → ∩ ( 𝑉 “ 𝑟 ) = ∩ 𝑙 ∈ 𝑟 ( 𝑉 ‘ 𝑙 ) ) |
| 32 |
23 31
|
eqtrd |
⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ) ∧ 𝑆 ≠ ∅ ) ∧ 𝑟 ∈ 𝒫 ( LIdeal ‘ 𝑅 ) ) ∧ 𝑆 = ( 𝑉 “ 𝑟 ) ) → ∩ 𝑆 = ∩ 𝑙 ∈ 𝑟 ( 𝑉 ‘ 𝑙 ) ) |
| 33 |
|
simplr |
⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ) ∧ 𝑆 ≠ ∅ ) ∧ 𝑟 ∈ 𝒫 ( LIdeal ‘ 𝑅 ) ) ∧ 𝑆 = ( 𝑉 “ 𝑟 ) ) ∧ 𝑟 = ∅ ) → 𝑆 = ( 𝑉 “ 𝑟 ) ) |
| 34 |
|
simpr |
⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ) ∧ 𝑆 ≠ ∅ ) ∧ 𝑟 ∈ 𝒫 ( LIdeal ‘ 𝑅 ) ) ∧ 𝑆 = ( 𝑉 “ 𝑟 ) ) ∧ 𝑟 = ∅ ) → 𝑟 = ∅ ) |
| 35 |
34
|
imaeq2d |
⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ) ∧ 𝑆 ≠ ∅ ) ∧ 𝑟 ∈ 𝒫 ( LIdeal ‘ 𝑅 ) ) ∧ 𝑆 = ( 𝑉 “ 𝑟 ) ) ∧ 𝑟 = ∅ ) → ( 𝑉 “ 𝑟 ) = ( 𝑉 “ ∅ ) ) |
| 36 |
|
ima0 |
⊢ ( 𝑉 “ ∅ ) = ∅ |
| 37 |
35 36
|
eqtrdi |
⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ) ∧ 𝑆 ≠ ∅ ) ∧ 𝑟 ∈ 𝒫 ( LIdeal ‘ 𝑅 ) ) ∧ 𝑆 = ( 𝑉 “ 𝑟 ) ) ∧ 𝑟 = ∅ ) → ( 𝑉 “ 𝑟 ) = ∅ ) |
| 38 |
33 37
|
eqtrd |
⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ) ∧ 𝑆 ≠ ∅ ) ∧ 𝑟 ∈ 𝒫 ( LIdeal ‘ 𝑅 ) ) ∧ 𝑆 = ( 𝑉 “ 𝑟 ) ) ∧ 𝑟 = ∅ ) → 𝑆 = ∅ ) |
| 39 |
|
simp-4r |
⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ) ∧ 𝑆 ≠ ∅ ) ∧ 𝑟 ∈ 𝒫 ( LIdeal ‘ 𝑅 ) ) ∧ 𝑆 = ( 𝑉 “ 𝑟 ) ) ∧ 𝑟 = ∅ ) → 𝑆 ≠ ∅ ) |
| 40 |
39
|
neneqd |
⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ) ∧ 𝑆 ≠ ∅ ) ∧ 𝑟 ∈ 𝒫 ( LIdeal ‘ 𝑅 ) ) ∧ 𝑆 = ( 𝑉 “ 𝑟 ) ) ∧ 𝑟 = ∅ ) → ¬ 𝑆 = ∅ ) |
| 41 |
38 40
|
pm2.65da |
⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ) ∧ 𝑆 ≠ ∅ ) ∧ 𝑟 ∈ 𝒫 ( LIdeal ‘ 𝑅 ) ) ∧ 𝑆 = ( 𝑉 “ 𝑟 ) ) → ¬ 𝑟 = ∅ ) |
| 42 |
41
|
neqned |
⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ) ∧ 𝑆 ≠ ∅ ) ∧ 𝑟 ∈ 𝒫 ( LIdeal ‘ 𝑅 ) ) ∧ 𝑆 = ( 𝑉 “ 𝑟 ) ) → 𝑟 ≠ ∅ ) |
| 43 |
1 15
|
zarclsiin |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝑟 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑟 ≠ ∅ ) → ∩ 𝑙 ∈ 𝑟 ( 𝑉 ‘ 𝑙 ) = ( 𝑉 ‘ ( ( RSpan ‘ 𝑅 ) ‘ ∪ 𝑟 ) ) ) |
| 44 |
3 6 42 43
|
syl3anc |
⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ) ∧ 𝑆 ≠ ∅ ) ∧ 𝑟 ∈ 𝒫 ( LIdeal ‘ 𝑅 ) ) ∧ 𝑆 = ( 𝑉 “ 𝑟 ) ) → ∩ 𝑙 ∈ 𝑟 ( 𝑉 ‘ 𝑙 ) = ( 𝑉 ‘ ( ( RSpan ‘ 𝑅 ) ‘ ∪ 𝑟 ) ) ) |
| 45 |
1
|
a1i |
⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ) ∧ 𝑆 ≠ ∅ ) ∧ 𝑟 ∈ 𝒫 ( LIdeal ‘ 𝑅 ) ) ∧ 𝑆 = ( 𝑉 “ 𝑟 ) ) → 𝑉 = ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } ) ) |
| 46 |
19
|
adantl |
⊢ ( ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ) ∧ 𝑆 ≠ ∅ ) ∧ 𝑟 ∈ 𝒫 ( LIdeal ‘ 𝑅 ) ) ∧ 𝑆 = ( 𝑉 “ 𝑟 ) ) ∧ 𝑖 = ( ( RSpan ‘ 𝑅 ) ‘ ∪ 𝑟 ) ) → { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ ( ( RSpan ‘ 𝑅 ) ‘ ∪ 𝑟 ) ⊆ 𝑗 } ) |
| 47 |
26
|
rabex |
⊢ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ ( ( RSpan ‘ 𝑅 ) ‘ ∪ 𝑟 ) ⊆ 𝑗 } ∈ V |
| 48 |
47
|
a1i |
⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ) ∧ 𝑆 ≠ ∅ ) ∧ 𝑟 ∈ 𝒫 ( LIdeal ‘ 𝑅 ) ) ∧ 𝑆 = ( 𝑉 “ 𝑟 ) ) → { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ ( ( RSpan ‘ 𝑅 ) ‘ ∪ 𝑟 ) ⊆ 𝑗 } ∈ V ) |
| 49 |
45 46 17 48
|
fvmptd |
⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ) ∧ 𝑆 ≠ ∅ ) ∧ 𝑟 ∈ 𝒫 ( LIdeal ‘ 𝑅 ) ) ∧ 𝑆 = ( 𝑉 “ 𝑟 ) ) → ( 𝑉 ‘ ( ( RSpan ‘ 𝑅 ) ‘ ∪ 𝑟 ) ) = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ ( ( RSpan ‘ 𝑅 ) ‘ ∪ 𝑟 ) ⊆ 𝑗 } ) |
| 50 |
32 44 49
|
3eqtrd |
⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ) ∧ 𝑆 ≠ ∅ ) ∧ 𝑟 ∈ 𝒫 ( LIdeal ‘ 𝑅 ) ) ∧ 𝑆 = ( 𝑉 “ 𝑟 ) ) → ∩ 𝑆 = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ ( ( RSpan ‘ 𝑅 ) ‘ ∪ 𝑟 ) ⊆ 𝑗 } ) |
| 51 |
17 21 50
|
rspcedvd |
⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ) ∧ 𝑆 ≠ ∅ ) ∧ 𝑟 ∈ 𝒫 ( LIdeal ‘ 𝑅 ) ) ∧ 𝑆 = ( 𝑉 “ 𝑟 ) ) → ∃ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ∩ 𝑆 = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } ) |
| 52 |
|
intex |
⊢ ( 𝑆 ≠ ∅ ↔ ∩ 𝑆 ∈ V ) |
| 53 |
52
|
biimpi |
⊢ ( 𝑆 ≠ ∅ → ∩ 𝑆 ∈ V ) |
| 54 |
53
|
3ad2ant3 |
⊢ ( ( 𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ∧ 𝑆 ≠ ∅ ) → ∩ 𝑆 ∈ V ) |
| 55 |
1
|
elrnmpt |
⊢ ( ∩ 𝑆 ∈ V → ( ∩ 𝑆 ∈ ran 𝑉 ↔ ∃ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ∩ 𝑆 = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } ) ) |
| 56 |
54 55
|
syl |
⊢ ( ( 𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ∧ 𝑆 ≠ ∅ ) → ( ∩ 𝑆 ∈ ran 𝑉 ↔ ∃ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ∩ 𝑆 = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } ) ) |
| 57 |
56
|
ad5ant123 |
⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ) ∧ 𝑆 ≠ ∅ ) ∧ 𝑟 ∈ 𝒫 ( LIdeal ‘ 𝑅 ) ) ∧ 𝑆 = ( 𝑉 “ 𝑟 ) ) → ( ∩ 𝑆 ∈ ran 𝑉 ↔ ∃ 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ∩ 𝑆 = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } ) ) |
| 58 |
51 57
|
mpbird |
⊢ ( ( ( ( ( 𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ) ∧ 𝑆 ≠ ∅ ) ∧ 𝑟 ∈ 𝒫 ( LIdeal ‘ 𝑅 ) ) ∧ 𝑆 = ( 𝑉 “ 𝑟 ) ) → ∩ 𝑆 ∈ ran 𝑉 ) |
| 59 |
|
fvexd |
⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ) ∧ 𝑆 ≠ ∅ ) → ( LIdeal ‘ 𝑅 ) ∈ V ) |
| 60 |
24
|
a1i |
⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ) ∧ 𝑆 ≠ ∅ ) → Fun 𝑉 ) |
| 61 |
|
simplr |
⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ) ∧ 𝑆 ≠ ∅ ) → 𝑆 ⊆ ran 𝑉 ) |
| 62 |
27 1
|
fnmpti |
⊢ 𝑉 Fn ( LIdeal ‘ 𝑅 ) |
| 63 |
|
fnima |
⊢ ( 𝑉 Fn ( LIdeal ‘ 𝑅 ) → ( 𝑉 “ ( LIdeal ‘ 𝑅 ) ) = ran 𝑉 ) |
| 64 |
62 63
|
ax-mp |
⊢ ( 𝑉 “ ( LIdeal ‘ 𝑅 ) ) = ran 𝑉 |
| 65 |
61 64
|
sseqtrrdi |
⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ) ∧ 𝑆 ≠ ∅ ) → 𝑆 ⊆ ( 𝑉 “ ( LIdeal ‘ 𝑅 ) ) ) |
| 66 |
|
ssimaexg |
⊢ ( ( ( LIdeal ‘ 𝑅 ) ∈ V ∧ Fun 𝑉 ∧ 𝑆 ⊆ ( 𝑉 “ ( LIdeal ‘ 𝑅 ) ) ) → ∃ 𝑟 ( 𝑟 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑆 = ( 𝑉 “ 𝑟 ) ) ) |
| 67 |
59 60 65 66
|
syl3anc |
⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ) ∧ 𝑆 ≠ ∅ ) → ∃ 𝑟 ( 𝑟 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑆 = ( 𝑉 “ 𝑟 ) ) ) |
| 68 |
|
vex |
⊢ 𝑟 ∈ V |
| 69 |
68
|
a1i |
⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ) ∧ 𝑆 ≠ ∅ ) ∧ 𝑟 ⊆ ( LIdeal ‘ 𝑅 ) ) → 𝑟 ∈ V ) |
| 70 |
|
simpr |
⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ) ∧ 𝑆 ≠ ∅ ) ∧ 𝑟 ⊆ ( LIdeal ‘ 𝑅 ) ) → 𝑟 ⊆ ( LIdeal ‘ 𝑅 ) ) |
| 71 |
69 70
|
elpwd |
⊢ ( ( ( ( 𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ) ∧ 𝑆 ≠ ∅ ) ∧ 𝑟 ⊆ ( LIdeal ‘ 𝑅 ) ) → 𝑟 ∈ 𝒫 ( LIdeal ‘ 𝑅 ) ) |
| 72 |
71
|
ex |
⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ) ∧ 𝑆 ≠ ∅ ) → ( 𝑟 ⊆ ( LIdeal ‘ 𝑅 ) → 𝑟 ∈ 𝒫 ( LIdeal ‘ 𝑅 ) ) ) |
| 73 |
72
|
anim1d |
⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ) ∧ 𝑆 ≠ ∅ ) → ( ( 𝑟 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑆 = ( 𝑉 “ 𝑟 ) ) → ( 𝑟 ∈ 𝒫 ( LIdeal ‘ 𝑅 ) ∧ 𝑆 = ( 𝑉 “ 𝑟 ) ) ) ) |
| 74 |
73
|
eximdv |
⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ) ∧ 𝑆 ≠ ∅ ) → ( ∃ 𝑟 ( 𝑟 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑆 = ( 𝑉 “ 𝑟 ) ) → ∃ 𝑟 ( 𝑟 ∈ 𝒫 ( LIdeal ‘ 𝑅 ) ∧ 𝑆 = ( 𝑉 “ 𝑟 ) ) ) ) |
| 75 |
67 74
|
mpd |
⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ) ∧ 𝑆 ≠ ∅ ) → ∃ 𝑟 ( 𝑟 ∈ 𝒫 ( LIdeal ‘ 𝑅 ) ∧ 𝑆 = ( 𝑉 “ 𝑟 ) ) ) |
| 76 |
|
df-rex |
⊢ ( ∃ 𝑟 ∈ 𝒫 ( LIdeal ‘ 𝑅 ) 𝑆 = ( 𝑉 “ 𝑟 ) ↔ ∃ 𝑟 ( 𝑟 ∈ 𝒫 ( LIdeal ‘ 𝑅 ) ∧ 𝑆 = ( 𝑉 “ 𝑟 ) ) ) |
| 77 |
75 76
|
sylibr |
⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ) ∧ 𝑆 ≠ ∅ ) → ∃ 𝑟 ∈ 𝒫 ( LIdeal ‘ 𝑅 ) 𝑆 = ( 𝑉 “ 𝑟 ) ) |
| 78 |
58 77
|
r19.29a |
⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ) ∧ 𝑆 ≠ ∅ ) → ∩ 𝑆 ∈ ran 𝑉 ) |
| 79 |
78
|
3impa |
⊢ ( ( 𝑅 ∈ CRing ∧ 𝑆 ⊆ ran 𝑉 ∧ 𝑆 ≠ ∅ ) → ∩ 𝑆 ∈ ran 𝑉 ) |