Metamath Proof Explorer

Theorem zarclsiin

Description: In a Zariski topology, the intersection of the closures of a family of ideals is the closure of the span of their union. (Contributed by Thierry Arnoux, 16-Jun-2024)

Ref Expression
Hypotheses zarclsx.1 ⊢ 𝑉 = ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } )
zarclsiin.1 ⊢ 𝐾 = ( RSpan ‘ 𝑅 )
Assertion zarclsiin ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) → ∩ 𝑙 ∈ 𝑇 ( 𝑉 ‘ 𝑙 ) = ( 𝑉 ‘ ( 𝐾 ‘ ∪ 𝑇 ) ) )

Proof

Step Hyp Ref Expression
1 zarclsx.1 ⊢ 𝑉 = ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } )
2 zarclsiin.1 ⊢ 𝐾 = ( RSpan ‘ 𝑅 )
3 sseq2 ⊢ ( 𝑗 = 𝑝 → ( ( 𝐾 ‘ ∪ 𝑇 ) ⊆ 𝑗 ↔ ( 𝐾 ‘ ∪ 𝑇 ) ⊆ 𝑝 ) )
4 simpl3 ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 ( 𝑉 ‘ 𝑙 ) ) → 𝑇 ≠ ∅ )
5 1 a1i ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑙 ∈ 𝑇 ) → 𝑉 = ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } ) )
6 sseq1 ⊢ ( 𝑖 = 𝑙 → ( 𝑖 ⊆ 𝑗 ↔ 𝑙 ⊆ 𝑗 ) )
7 6 rabbidv ⊢ ( 𝑖 = 𝑙 → { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑙 ⊆ 𝑗 } )
8 7 adantl ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑙 ∈ 𝑇 ) ∧ 𝑖 = 𝑙 ) → { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑙 ⊆ 𝑗 } )
9 simp2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) → 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) )
10 9 sselda ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑙 ∈ 𝑇 ) → 𝑙 ∈ ( LIdeal ‘ 𝑅 ) )
11 fvex ⊢ ( PrmIdeal ‘ 𝑅 ) ∈ V
12 11 rabex ⊢ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑙 ⊆ 𝑗 } ∈ V
13 12 a1i ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑙 ∈ 𝑇 ) → { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑙 ⊆ 𝑗 } ∈ V )
14 5 8 10 13 fvmptd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑙 ∈ 𝑇 ) → ( 𝑉 ‘ 𝑙 ) = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑙 ⊆ 𝑗 } )
15 ssrab2 ⊢ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑙 ⊆ 𝑗 } ⊆ ( PrmIdeal ‘ 𝑅 )
16 15 a1i ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑙 ∈ 𝑇 ) → { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑙 ⊆ 𝑗 } ⊆ ( PrmIdeal ‘ 𝑅 ) )
17 14 16 eqsstrd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑙 ∈ 𝑇 ) → ( 𝑉 ‘ 𝑙 ) ⊆ ( PrmIdeal ‘ 𝑅 ) )
18 17 sseld ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑙 ∈ 𝑇 ) → ( 𝑝 ∈ ( 𝑉 ‘ 𝑙 ) → 𝑝 ∈ ( PrmIdeal ‘ 𝑅 ) ) )
19 18 ralimdva ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) → ( ∀ 𝑙 ∈ 𝑇 𝑝 ∈ ( 𝑉 ‘ 𝑙 ) → ∀ 𝑙 ∈ 𝑇 𝑝 ∈ ( PrmIdeal ‘ 𝑅 ) ) )
20 eliin ⊢ ( 𝑝 ∈ V → ( 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 ( 𝑉 ‘ 𝑙 ) ↔ ∀ 𝑙 ∈ 𝑇 𝑝 ∈ ( 𝑉 ‘ 𝑙 ) ) )
21 20 elv ⊢ ( 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 ( 𝑉 ‘ 𝑙 ) ↔ ∀ 𝑙 ∈ 𝑇 𝑝 ∈ ( 𝑉 ‘ 𝑙 ) )
22 21 biimpi ⊢ ( 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 ( 𝑉 ‘ 𝑙 ) → ∀ 𝑙 ∈ 𝑇 𝑝 ∈ ( 𝑉 ‘ 𝑙 ) )
23 19 22 impel ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 ( 𝑉 ‘ 𝑙 ) ) → ∀ 𝑙 ∈ 𝑇 𝑝 ∈ ( PrmIdeal ‘ 𝑅 ) )
24 rspn0 ⊢ ( 𝑇 ≠ ∅ → ( ∀ 𝑙 ∈ 𝑇 𝑝 ∈ ( PrmIdeal ‘ 𝑅 ) → 𝑝 ∈ ( PrmIdeal ‘ 𝑅 ) ) )
25 24 imp ⊢ ( ( 𝑇 ≠ ∅ ∧ ∀ 𝑙 ∈ 𝑇 𝑝 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝑝 ∈ ( PrmIdeal ‘ 𝑅 ) )
26 4 23 25 syl2anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 ( 𝑉 ‘ 𝑙 ) ) → 𝑝 ∈ ( PrmIdeal ‘ 𝑅 ) )
27 simp1 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) → 𝑅 ∈ Ring )
28 27 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 ( 𝑉 ‘ 𝑙 ) ) → 𝑅 ∈ Ring )
29 prmidlidl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑝 ∈ ( PrmIdeal ‘ 𝑅 ) ) → 𝑝 ∈ ( LIdeal ‘ 𝑅 ) )
30 28 26 29 syl2anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 ( 𝑉 ‘ 𝑙 ) ) → 𝑝 ∈ ( LIdeal ‘ 𝑅 ) )
31 nfv ⊢ Ⅎ 𝑙 ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ )
32 nfcv ⊢ Ⅎ 𝑙 𝑝
33 nfii1 ⊢ Ⅎ 𝑙 ∩ 𝑙 ∈ 𝑇 ( 𝑉 ‘ 𝑙 )
34 32 33 nfel ⊢ Ⅎ 𝑙 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 ( 𝑉 ‘ 𝑙 )
35 31 34 nfan ⊢ Ⅎ 𝑙 ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 ( 𝑉 ‘ 𝑙 ) )
36 21 bilani ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 ( 𝑉 ‘ 𝑙 ) ) → ∀ 𝑙 ∈ 𝑇 𝑝 ∈ ( 𝑉 ‘ 𝑙 ) )
37 36 adantr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 ( 𝑉 ‘ 𝑙 ) ) ∧ 𝑙 ∈ 𝑇 ) → ∀ 𝑙 ∈ 𝑇 𝑝 ∈ ( 𝑉 ‘ 𝑙 ) )
38 simpr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 ( 𝑉 ‘ 𝑙 ) ) ∧ 𝑙 ∈ 𝑇 ) → 𝑙 ∈ 𝑇 )
39 rspa ⊢ ( ( ∀ 𝑙 ∈ 𝑇 𝑝 ∈ ( 𝑉 ‘ 𝑙 ) ∧ 𝑙 ∈ 𝑇 ) → 𝑝 ∈ ( 𝑉 ‘ 𝑙 ) )
40 37 38 39 syl2anc ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 ( 𝑉 ‘ 𝑙 ) ) ∧ 𝑙 ∈ 𝑇 ) → 𝑝 ∈ ( 𝑉 ‘ 𝑙 ) )
41 14 adantlr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 ( 𝑉 ‘ 𝑙 ) ) ∧ 𝑙 ∈ 𝑇 ) → ( 𝑉 ‘ 𝑙 ) = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑙 ⊆ 𝑗 } )
42 40 41 eleqtrd ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 ( 𝑉 ‘ 𝑙 ) ) ∧ 𝑙 ∈ 𝑇 ) → 𝑝 ∈ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑙 ⊆ 𝑗 } )
43 sseq2 ⊢ ( 𝑗 = 𝑝 → ( 𝑙 ⊆ 𝑗 ↔ 𝑙 ⊆ 𝑝 ) )
44 43 elrab ⊢ ( 𝑝 ∈ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑙 ⊆ 𝑗 } ↔ ( 𝑝 ∈ ( PrmIdeal ‘ 𝑅 ) ∧ 𝑙 ⊆ 𝑝 ) )
45 42 44 sylib ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 ( 𝑉 ‘ 𝑙 ) ) ∧ 𝑙 ∈ 𝑇 ) → ( 𝑝 ∈ ( PrmIdeal ‘ 𝑅 ) ∧ 𝑙 ⊆ 𝑝 ) )
46 45 simprd ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 ( 𝑉 ‘ 𝑙 ) ) ∧ 𝑙 ∈ 𝑇 ) → 𝑙 ⊆ 𝑝 )
47 46 ex ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 ( 𝑉 ‘ 𝑙 ) ) → ( 𝑙 ∈ 𝑇 → 𝑙 ⊆ 𝑝 ) )
48 35 47 ralrimi ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 ( 𝑉 ‘ 𝑙 ) ) → ∀ 𝑙 ∈ 𝑇 𝑙 ⊆ 𝑝 )
49 unissb ⊢ ( ∪ 𝑇 ⊆ 𝑝 ↔ ∀ 𝑙 ∈ 𝑇 𝑙 ⊆ 𝑝 )
50 48 49 sylibr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 ( 𝑉 ‘ 𝑙 ) ) → ∪ 𝑇 ⊆ 𝑝 )
51 eqid ⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
52 2 51 rspssp ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∧ ∪ 𝑇 ⊆ 𝑝 ) → ( 𝐾 ‘ ∪ 𝑇 ) ⊆ 𝑝 )
53 28 30 50 52 syl3anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 ( 𝑉 ‘ 𝑙 ) ) → ( 𝐾 ‘ ∪ 𝑇 ) ⊆ 𝑝 )
54 3 26 53 elrabd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 ( 𝑉 ‘ 𝑙 ) ) → 𝑝 ∈ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ ( 𝐾 ‘ ∪ 𝑇 ) ⊆ 𝑗 } )
55 1 a1i ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) → 𝑉 = ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } ) )
56 sseq1 ⊢ ( 𝑖 = ( 𝐾 ‘ ∪ 𝑇 ) → ( 𝑖 ⊆ 𝑗 ↔ ( 𝐾 ‘ ∪ 𝑇 ) ⊆ 𝑗 ) )
57 56 rabbidv ⊢ ( 𝑖 = ( 𝐾 ‘ ∪ 𝑇 ) → { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ ( 𝐾 ‘ ∪ 𝑇 ) ⊆ 𝑗 } )
58 57 adantl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑖 = ( 𝐾 ‘ ∪ 𝑇 ) ) → { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ ( 𝐾 ‘ ∪ 𝑇 ) ⊆ 𝑗 } )
59 9 sselda ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑖 ∈ 𝑇 ) → 𝑖 ∈ ( LIdeal ‘ 𝑅 ) )
60 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
61 60 51 lidlss ⊢ ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) → 𝑖 ⊆ ( Base ‘ 𝑅 ) )
62 59 61 syl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑖 ∈ 𝑇 ) → 𝑖 ⊆ ( Base ‘ 𝑅 ) )
63 62 ralrimiva ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) → ∀ 𝑖 ∈ 𝑇 𝑖 ⊆ ( Base ‘ 𝑅 ) )
64 unissb ⊢ ( ∪ 𝑇 ⊆ ( Base ‘ 𝑅 ) ↔ ∀ 𝑖 ∈ 𝑇 𝑖 ⊆ ( Base ‘ 𝑅 ) )
65 63 64 sylibr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) → ∪ 𝑇 ⊆ ( Base ‘ 𝑅 ) )
66 2 60 51 rspcl ⊢ ( ( 𝑅 ∈ Ring ∧ ∪ 𝑇 ⊆ ( Base ‘ 𝑅 ) ) → ( 𝐾 ‘ ∪ 𝑇 ) ∈ ( LIdeal ‘ 𝑅 ) )
67 27 65 66 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) → ( 𝐾 ‘ ∪ 𝑇 ) ∈ ( LIdeal ‘ 𝑅 ) )
68 11 rabex ⊢ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ ( 𝐾 ‘ ∪ 𝑇 ) ⊆ 𝑗 } ∈ V
69 68 a1i ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) → { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ ( 𝐾 ‘ ∪ 𝑇 ) ⊆ 𝑗 } ∈ V )
70 55 58 67 69 fvmptd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) → ( 𝑉 ‘ ( 𝐾 ‘ ∪ 𝑇 ) ) = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ ( 𝐾 ‘ ∪ 𝑇 ) ⊆ 𝑗 } )
71 70 eleq2d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) → ( 𝑝 ∈ ( 𝑉 ‘ ( 𝐾 ‘ ∪ 𝑇 ) ) ↔ 𝑝 ∈ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ ( 𝐾 ‘ ∪ 𝑇 ) ⊆ 𝑗 } ) )
72 71 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 ( 𝑉 ‘ 𝑙 ) ) → ( 𝑝 ∈ ( 𝑉 ‘ ( 𝐾 ‘ ∪ 𝑇 ) ) ↔ 𝑝 ∈ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ ( 𝐾 ‘ ∪ 𝑇 ) ⊆ 𝑗 } ) )
73 54 72 mpbird ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 ( 𝑉 ‘ 𝑙 ) ) → 𝑝 ∈ ( 𝑉 ‘ ( 𝐾 ‘ ∪ 𝑇 ) ) )
74 71 biimpa ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ( 𝑉 ‘ ( 𝐾 ‘ ∪ 𝑇 ) ) ) → 𝑝 ∈ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ ( 𝐾 ‘ ∪ 𝑇 ) ⊆ 𝑗 } )
75 3 elrab ⊢ ( 𝑝 ∈ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ ( 𝐾 ‘ ∪ 𝑇 ) ⊆ 𝑗 } ↔ ( 𝑝 ∈ ( PrmIdeal ‘ 𝑅 ) ∧ ( 𝐾 ‘ ∪ 𝑇 ) ⊆ 𝑝 ) )
76 74 75 sylib ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ( 𝑉 ‘ ( 𝐾 ‘ ∪ 𝑇 ) ) ) → ( 𝑝 ∈ ( PrmIdeal ‘ 𝑅 ) ∧ ( 𝐾 ‘ ∪ 𝑇 ) ⊆ 𝑝 ) )
77 76 simpld ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ( 𝑉 ‘ ( 𝐾 ‘ ∪ 𝑇 ) ) ) → 𝑝 ∈ ( PrmIdeal ‘ 𝑅 ) )
78 77 adantr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ( 𝑉 ‘ ( 𝐾 ‘ ∪ 𝑇 ) ) ) ∧ 𝑙 ∈ 𝑇 ) → 𝑝 ∈ ( PrmIdeal ‘ 𝑅 ) )
79 elssuni ⊢ ( 𝑙 ∈ 𝑇 → 𝑙 ⊆ ∪ 𝑇 )
80 79 adantl ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ( 𝑉 ‘ ( 𝐾 ‘ ∪ 𝑇 ) ) ) ∧ 𝑙 ∈ 𝑇 ) → 𝑙 ⊆ ∪ 𝑇 )
81 simpll ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ( 𝑉 ‘ ( 𝐾 ‘ ∪ 𝑇 ) ) ) ∧ 𝑙 ∈ 𝑇 ) → ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) )
82 2 60 rspssid ⊢ ( ( 𝑅 ∈ Ring ∧ ∪ 𝑇 ⊆ ( Base ‘ 𝑅 ) ) → ∪ 𝑇 ⊆ ( 𝐾 ‘ ∪ 𝑇 ) )
83 27 65 82 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) → ∪ 𝑇 ⊆ ( 𝐾 ‘ ∪ 𝑇 ) )
84 81 83 syl ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ( 𝑉 ‘ ( 𝐾 ‘ ∪ 𝑇 ) ) ) ∧ 𝑙 ∈ 𝑇 ) → ∪ 𝑇 ⊆ ( 𝐾 ‘ ∪ 𝑇 ) )
85 80 84 sstrd ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ( 𝑉 ‘ ( 𝐾 ‘ ∪ 𝑇 ) ) ) ∧ 𝑙 ∈ 𝑇 ) → 𝑙 ⊆ ( 𝐾 ‘ ∪ 𝑇 ) )
86 76 simprd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ( 𝑉 ‘ ( 𝐾 ‘ ∪ 𝑇 ) ) ) → ( 𝐾 ‘ ∪ 𝑇 ) ⊆ 𝑝 )
87 86 adantr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ( 𝑉 ‘ ( 𝐾 ‘ ∪ 𝑇 ) ) ) ∧ 𝑙 ∈ 𝑇 ) → ( 𝐾 ‘ ∪ 𝑇 ) ⊆ 𝑝 )
88 85 87 sstrd ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ( 𝑉 ‘ ( 𝐾 ‘ ∪ 𝑇 ) ) ) ∧ 𝑙 ∈ 𝑇 ) → 𝑙 ⊆ 𝑝 )
89 43 78 88 elrabd ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ( 𝑉 ‘ ( 𝐾 ‘ ∪ 𝑇 ) ) ) ∧ 𝑙 ∈ 𝑇 ) → 𝑝 ∈ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑙 ⊆ 𝑗 } )
90 9 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ( 𝑉 ‘ ( 𝐾 ‘ ∪ 𝑇 ) ) ) → 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) )
91 90 sselda ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ( 𝑉 ‘ ( 𝐾 ‘ ∪ 𝑇 ) ) ) ∧ 𝑙 ∈ 𝑇 ) → 𝑙 ∈ ( LIdeal ‘ 𝑅 ) )
92 1 a1i ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑙 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝑉 = ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } ) )
93 7 adantl ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑙 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑖 = 𝑙 ) → { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑙 ⊆ 𝑗 } )
94 simpr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑙 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝑙 ∈ ( LIdeal ‘ 𝑅 ) )
95 12 a1i ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑙 ∈ ( LIdeal ‘ 𝑅 ) ) → { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑙 ⊆ 𝑗 } ∈ V )
96 92 93 94 95 fvmptd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑙 ∈ ( LIdeal ‘ 𝑅 ) ) → ( 𝑉 ‘ 𝑙 ) = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑙 ⊆ 𝑗 } )
97 81 91 96 syl2anc ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ( 𝑉 ‘ ( 𝐾 ‘ ∪ 𝑇 ) ) ) ∧ 𝑙 ∈ 𝑇 ) → ( 𝑉 ‘ 𝑙 ) = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑙 ⊆ 𝑗 } )
98 89 97 eleqtrrd ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ( 𝑉 ‘ ( 𝐾 ‘ ∪ 𝑇 ) ) ) ∧ 𝑙 ∈ 𝑇 ) → 𝑝 ∈ ( 𝑉 ‘ 𝑙 ) )
99 98 ralrimiva ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ( 𝑉 ‘ ( 𝐾 ‘ ∪ 𝑇 ) ) ) → ∀ 𝑙 ∈ 𝑇 𝑝 ∈ ( 𝑉 ‘ 𝑙 ) )
100 21 a1i ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ( 𝑉 ‘ ( 𝐾 ‘ ∪ 𝑇 ) ) ) → ( 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 ( 𝑉 ‘ 𝑙 ) ↔ ∀ 𝑙 ∈ 𝑇 𝑝 ∈ ( 𝑉 ‘ 𝑙 ) ) )
101 99 100 mpbird ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ( 𝑉 ‘ ( 𝐾 ‘ ∪ 𝑇 ) ) ) → 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 ( 𝑉 ‘ 𝑙 ) )
102 73 101 impbida ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) → ( 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 ( 𝑉 ‘ 𝑙 ) ↔ 𝑝 ∈ ( 𝑉 ‘ ( 𝐾 ‘ ∪ 𝑇 ) ) ) )
103 102 eqrdv ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) → ∩ 𝑙 ∈ 𝑇 ( 𝑉 ‘ 𝑙 ) = ( 𝑉 ‘ ( 𝐾 ‘ ∪ 𝑇 ) ) )