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 22 a1i ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) → ( 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 ( 𝑉 ‘ 𝑙 ) → ∀ 𝑙 ∈ 𝑇 𝑝 ∈ ( 𝑉 ‘ 𝑙 ) ) )
37 36 imp ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 ( 𝑉 ‘ 𝑙 ) ) → ∀ 𝑙 ∈ 𝑇 𝑝 ∈ ( 𝑉 ‘ 𝑙 ) )
38 37 adantr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 ( 𝑉 ‘ 𝑙 ) ) ∧ 𝑙 ∈ 𝑇 ) → ∀ 𝑙 ∈ 𝑇 𝑝 ∈ ( 𝑉 ‘ 𝑙 ) )
39 simpr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 ( 𝑉 ‘ 𝑙 ) ) ∧ 𝑙 ∈ 𝑇 ) → 𝑙 ∈ 𝑇 )
40 rspa ⊢ ( ( ∀ 𝑙 ∈ 𝑇 𝑝 ∈ ( 𝑉 ‘ 𝑙 ) ∧ 𝑙 ∈ 𝑇 ) → 𝑝 ∈ ( 𝑉 ‘ 𝑙 ) )
41 38 39 40 syl2anc ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 ( 𝑉 ‘ 𝑙 ) ) ∧ 𝑙 ∈ 𝑇 ) → 𝑝 ∈ ( 𝑉 ‘ 𝑙 ) )
42 14 adantlr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 ( 𝑉 ‘ 𝑙 ) ) ∧ 𝑙 ∈ 𝑇 ) → ( 𝑉 ‘ 𝑙 ) = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑙 ⊆ 𝑗 } )
43 41 42 eleqtrd ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 ( 𝑉 ‘ 𝑙 ) ) ∧ 𝑙 ∈ 𝑇 ) → 𝑝 ∈ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑙 ⊆ 𝑗 } )
44 sseq2 ⊢ ( 𝑗 = 𝑝 → ( 𝑙 ⊆ 𝑗 ↔ 𝑙 ⊆ 𝑝 ) )
45 44 elrab ⊢ ( 𝑝 ∈ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑙 ⊆ 𝑗 } ↔ ( 𝑝 ∈ ( PrmIdeal ‘ 𝑅 ) ∧ 𝑙 ⊆ 𝑝 ) )
46 43 45 sylib ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 ( 𝑉 ‘ 𝑙 ) ) ∧ 𝑙 ∈ 𝑇 ) → ( 𝑝 ∈ ( PrmIdeal ‘ 𝑅 ) ∧ 𝑙 ⊆ 𝑝 ) )
47 46 simprd ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 ( 𝑉 ‘ 𝑙 ) ) ∧ 𝑙 ∈ 𝑇 ) → 𝑙 ⊆ 𝑝 )
48 47 ex ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 ( 𝑉 ‘ 𝑙 ) ) → ( 𝑙 ∈ 𝑇 → 𝑙 ⊆ 𝑝 ) )
49 35 48 ralrimi ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 ( 𝑉 ‘ 𝑙 ) ) → ∀ 𝑙 ∈ 𝑇 𝑙 ⊆ 𝑝 )
50 unissb ⊢ ( ∪ 𝑇 ⊆ 𝑝 ↔ ∀ 𝑙 ∈ 𝑇 𝑙 ⊆ 𝑝 )
51 49 50 sylibr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 ( 𝑉 ‘ 𝑙 ) ) → ∪ 𝑇 ⊆ 𝑝 )
52 eqid ⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
53 2 52 rspssp ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑝 ∈ ( LIdeal ‘ 𝑅 ) ∧ ∪ 𝑇 ⊆ 𝑝 ) → ( 𝐾 ‘ ∪ 𝑇 ) ⊆ 𝑝 )
54 28 30 51 53 syl3anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 ( 𝑉 ‘ 𝑙 ) ) → ( 𝐾 ‘ ∪ 𝑇 ) ⊆ 𝑝 )
55 3 26 54 elrabd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 ( 𝑉 ‘ 𝑙 ) ) → 𝑝 ∈ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ ( 𝐾 ‘ ∪ 𝑇 ) ⊆ 𝑗 } )
56 1 a1i ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) → 𝑉 = ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } ) )
57 sseq1 ⊢ ( 𝑖 = ( 𝐾 ‘ ∪ 𝑇 ) → ( 𝑖 ⊆ 𝑗 ↔ ( 𝐾 ‘ ∪ 𝑇 ) ⊆ 𝑗 ) )
58 57 rabbidv ⊢ ( 𝑖 = ( 𝐾 ‘ ∪ 𝑇 ) → { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ ( 𝐾 ‘ ∪ 𝑇 ) ⊆ 𝑗 } )
59 58 adantl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑖 = ( 𝐾 ‘ ∪ 𝑇 ) ) → { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ ( 𝐾 ‘ ∪ 𝑇 ) ⊆ 𝑗 } )
60 9 sselda ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑖 ∈ 𝑇 ) → 𝑖 ∈ ( LIdeal ‘ 𝑅 ) )
61 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
62 61 52 lidlss ⊢ ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) → 𝑖 ⊆ ( Base ‘ 𝑅 ) )
63 60 62 syl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑖 ∈ 𝑇 ) → 𝑖 ⊆ ( Base ‘ 𝑅 ) )
64 63 ralrimiva ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) → ∀ 𝑖 ∈ 𝑇 𝑖 ⊆ ( Base ‘ 𝑅 ) )
65 unissb ⊢ ( ∪ 𝑇 ⊆ ( Base ‘ 𝑅 ) ↔ ∀ 𝑖 ∈ 𝑇 𝑖 ⊆ ( Base ‘ 𝑅 ) )
66 64 65 sylibr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) → ∪ 𝑇 ⊆ ( Base ‘ 𝑅 ) )
67 2 61 52 rspcl ⊢ ( ( 𝑅 ∈ Ring ∧ ∪ 𝑇 ⊆ ( Base ‘ 𝑅 ) ) → ( 𝐾 ‘ ∪ 𝑇 ) ∈ ( LIdeal ‘ 𝑅 ) )
68 27 66 67 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) → ( 𝐾 ‘ ∪ 𝑇 ) ∈ ( LIdeal ‘ 𝑅 ) )
69 11 rabex ⊢ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ ( 𝐾 ‘ ∪ 𝑇 ) ⊆ 𝑗 } ∈ V
70 69 a1i ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) → { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ ( 𝐾 ‘ ∪ 𝑇 ) ⊆ 𝑗 } ∈ V )
71 56 59 68 70 fvmptd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) → ( 𝑉 ‘ ( 𝐾 ‘ ∪ 𝑇 ) ) = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ ( 𝐾 ‘ ∪ 𝑇 ) ⊆ 𝑗 } )
72 71 eleq2d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) → ( 𝑝 ∈ ( 𝑉 ‘ ( 𝐾 ‘ ∪ 𝑇 ) ) ↔ 𝑝 ∈ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ ( 𝐾 ‘ ∪ 𝑇 ) ⊆ 𝑗 } ) )
73 72 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 ( 𝑉 ‘ 𝑙 ) ) → ( 𝑝 ∈ ( 𝑉 ‘ ( 𝐾 ‘ ∪ 𝑇 ) ) ↔ 𝑝 ∈ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ ( 𝐾 ‘ ∪ 𝑇 ) ⊆ 𝑗 } ) )
74 55 73 mpbird ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 ( 𝑉 ‘ 𝑙 ) ) → 𝑝 ∈ ( 𝑉 ‘ ( 𝐾 ‘ ∪ 𝑇 ) ) )
75 72 biimpa ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ( 𝑉 ‘ ( 𝐾 ‘ ∪ 𝑇 ) ) ) → 𝑝 ∈ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ ( 𝐾 ‘ ∪ 𝑇 ) ⊆ 𝑗 } )
76 3 elrab ⊢ ( 𝑝 ∈ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ ( 𝐾 ‘ ∪ 𝑇 ) ⊆ 𝑗 } ↔ ( 𝑝 ∈ ( PrmIdeal ‘ 𝑅 ) ∧ ( 𝐾 ‘ ∪ 𝑇 ) ⊆ 𝑝 ) )
77 75 76 sylib ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ( 𝑉 ‘ ( 𝐾 ‘ ∪ 𝑇 ) ) ) → ( 𝑝 ∈ ( PrmIdeal ‘ 𝑅 ) ∧ ( 𝐾 ‘ ∪ 𝑇 ) ⊆ 𝑝 ) )
78 77 simpld ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ( 𝑉 ‘ ( 𝐾 ‘ ∪ 𝑇 ) ) ) → 𝑝 ∈ ( PrmIdeal ‘ 𝑅 ) )
79 78 adantr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ( 𝑉 ‘ ( 𝐾 ‘ ∪ 𝑇 ) ) ) ∧ 𝑙 ∈ 𝑇 ) → 𝑝 ∈ ( PrmIdeal ‘ 𝑅 ) )
80 elssuni ⊢ ( 𝑙 ∈ 𝑇 → 𝑙 ⊆ ∪ 𝑇 )
81 80 adantl ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ( 𝑉 ‘ ( 𝐾 ‘ ∪ 𝑇 ) ) ) ∧ 𝑙 ∈ 𝑇 ) → 𝑙 ⊆ ∪ 𝑇 )
82 simpll ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ( 𝑉 ‘ ( 𝐾 ‘ ∪ 𝑇 ) ) ) ∧ 𝑙 ∈ 𝑇 ) → ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) )
83 2 61 rspssid ⊢ ( ( 𝑅 ∈ Ring ∧ ∪ 𝑇 ⊆ ( Base ‘ 𝑅 ) ) → ∪ 𝑇 ⊆ ( 𝐾 ‘ ∪ 𝑇 ) )
84 27 66 83 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) → ∪ 𝑇 ⊆ ( 𝐾 ‘ ∪ 𝑇 ) )
85 82 84 syl ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ( 𝑉 ‘ ( 𝐾 ‘ ∪ 𝑇 ) ) ) ∧ 𝑙 ∈ 𝑇 ) → ∪ 𝑇 ⊆ ( 𝐾 ‘ ∪ 𝑇 ) )
86 81 85 sstrd ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ( 𝑉 ‘ ( 𝐾 ‘ ∪ 𝑇 ) ) ) ∧ 𝑙 ∈ 𝑇 ) → 𝑙 ⊆ ( 𝐾 ‘ ∪ 𝑇 ) )
87 77 simprd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ( 𝑉 ‘ ( 𝐾 ‘ ∪ 𝑇 ) ) ) → ( 𝐾 ‘ ∪ 𝑇 ) ⊆ 𝑝 )
88 87 adantr ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ( 𝑉 ‘ ( 𝐾 ‘ ∪ 𝑇 ) ) ) ∧ 𝑙 ∈ 𝑇 ) → ( 𝐾 ‘ ∪ 𝑇 ) ⊆ 𝑝 )
89 86 88 sstrd ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ( 𝑉 ‘ ( 𝐾 ‘ ∪ 𝑇 ) ) ) ∧ 𝑙 ∈ 𝑇 ) → 𝑙 ⊆ 𝑝 )
90 44 79 89 elrabd ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ( 𝑉 ‘ ( 𝐾 ‘ ∪ 𝑇 ) ) ) ∧ 𝑙 ∈ 𝑇 ) → 𝑝 ∈ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑙 ⊆ 𝑗 } )
91 9 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ( 𝑉 ‘ ( 𝐾 ‘ ∪ 𝑇 ) ) ) → 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) )
92 91 sselda ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ( 𝑉 ‘ ( 𝐾 ‘ ∪ 𝑇 ) ) ) ∧ 𝑙 ∈ 𝑇 ) → 𝑙 ∈ ( LIdeal ‘ 𝑅 ) )
93 1 a1i ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑙 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝑉 = ( 𝑖 ∈ ( LIdeal ‘ 𝑅 ) ↦ { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } ) )
94 7 adantl ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑙 ∈ ( LIdeal ‘ 𝑅 ) ) ∧ 𝑖 = 𝑙 ) → { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑖 ⊆ 𝑗 } = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑙 ⊆ 𝑗 } )
95 simpr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑙 ∈ ( LIdeal ‘ 𝑅 ) ) → 𝑙 ∈ ( LIdeal ‘ 𝑅 ) )
96 12 a1i ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑙 ∈ ( LIdeal ‘ 𝑅 ) ) → { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑙 ⊆ 𝑗 } ∈ V )
97 93 94 95 96 fvmptd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑙 ∈ ( LIdeal ‘ 𝑅 ) ) → ( 𝑉 ‘ 𝑙 ) = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑙 ⊆ 𝑗 } )
98 82 92 97 syl2anc ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ( 𝑉 ‘ ( 𝐾 ‘ ∪ 𝑇 ) ) ) ∧ 𝑙 ∈ 𝑇 ) → ( 𝑉 ‘ 𝑙 ) = { 𝑗 ∈ ( PrmIdeal ‘ 𝑅 ) ∣ 𝑙 ⊆ 𝑗 } )
99 90 98 eleqtrrd ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ( 𝑉 ‘ ( 𝐾 ‘ ∪ 𝑇 ) ) ) ∧ 𝑙 ∈ 𝑇 ) → 𝑝 ∈ ( 𝑉 ‘ 𝑙 ) )
100 99 ralrimiva ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ( 𝑉 ‘ ( 𝐾 ‘ ∪ 𝑇 ) ) ) → ∀ 𝑙 ∈ 𝑇 𝑝 ∈ ( 𝑉 ‘ 𝑙 ) )
101 21 a1i ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ( 𝑉 ‘ ( 𝐾 ‘ ∪ 𝑇 ) ) ) → ( 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 ( 𝑉 ‘ 𝑙 ) ↔ ∀ 𝑙 ∈ 𝑇 𝑝 ∈ ( 𝑉 ‘ 𝑙 ) ) )
102 100 101 mpbird ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) ∧ 𝑝 ∈ ( 𝑉 ‘ ( 𝐾 ‘ ∪ 𝑇 ) ) ) → 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 ( 𝑉 ‘ 𝑙 ) )
103 74 102 impbida ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) → ( 𝑝 ∈ ∩ 𝑙 ∈ 𝑇 ( 𝑉 ‘ 𝑙 ) ↔ 𝑝 ∈ ( 𝑉 ‘ ( 𝐾 ‘ ∪ 𝑇 ) ) ) )
104 103 eqrdv ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑇 ⊆ ( LIdeal ‘ 𝑅 ) ∧ 𝑇 ≠ ∅ ) → ∩ 𝑙 ∈ 𝑇 ( 𝑉 ‘ 𝑙 ) = ( 𝑉 ‘ ( 𝐾 ‘ ∪ 𝑇 ) ) )