Theorem rhmpreimacn 34026

Description: The function mapping a prime ideal to its preimage by a surjective ring homomorphism is continuous, when considering the Zariski topology. Corollary 1.2.3 of [EGA], p. 83. Notice that the direction of the continuous map 𝐺 is reverse: the original ring homomorphism 𝐹 goes from 𝑅 to 𝑆, but the continuous map 𝐺 goes from 𝐵 to 𝐴. This mapping is also called "induced map on prime spectra" or "pullback on primes". (Contributed by Thierry Arnoux, 8-Jul-2024.)

Hypotheses

Ref	Expression
rhmpreimacn.t	⊢ 𝑇 = (Spec‘𝑅)
rhmpreimacn.u	⊢ 𝑈 = (Spec‘𝑆)
rhmpreimacn.a	⊢ 𝐴 = (PrmIdeal‘𝑅)
rhmpreimacn.b	⊢ 𝐵 = (PrmIdeal‘𝑆)
rhmpreimacn.j	⊢ 𝐽 = (TopOpen‘𝑇)
rhmpreimacn.k	⊢ 𝐾 = (TopOpen‘𝑈)
rhmpreimacn.g	⊢ 𝐺 = (𝑖 ∈ 𝐵 ↦ (◡𝐹 “ 𝑖))
rhmpreimacn.r	⊢ (𝜑 → 𝑅 ∈ CRing)
rhmpreimacn.s	⊢ (𝜑 → 𝑆 ∈ CRing)
rhmpreimacn.f	⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆))
rhmpreimacn.1	⊢ (𝜑 → ran 𝐹 = (Base‘𝑆))

Assertion

Ref	Expression
rhmpreimacn	⊢ (𝜑 → 𝐺 ∈ (𝐾 Cn 𝐽))

Distinct variable groups:   𝑅,𝑖   𝑖,𝐽   𝑆,𝑖   𝜑,𝑖   𝑖,𝐺   𝐵,𝑖   𝐴,𝑖   𝑖,𝐹

Allowed substitution hints:   𝑇(𝑖)   𝑈(𝑖)   𝐾(𝑖)

Proof of Theorem rhmpreimacn

Dummy variables 𝑎 𝑏 𝑘 𝑙 𝑗 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		rhmpreimacn.s	. . 3 ⊢ (𝜑 → 𝑆 ∈ CRing)
2		rhmpreimacn.u	. . . 4 ⊢ 𝑈 = (Spec‘𝑆)
3		rhmpreimacn.k	. . . 4 ⊢ 𝐾 = (TopOpen‘𝑈)
4		rhmpreimacn.b	. . . 4 ⊢ 𝐵 = (PrmIdeal‘𝑆)
5	2, 3, 4	zartopon 34018	. . 3 ⊢ (𝑆 ∈ CRing → 𝐾 ∈ (TopOn‘𝐵))
6	1, 5	syl 17	. 2 ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝐵))
7		rhmpreimacn.r	. . 3 ⊢ (𝜑 → 𝑅 ∈ CRing)
8		rhmpreimacn.t	. . . 4 ⊢ 𝑇 = (Spec‘𝑅)
9		rhmpreimacn.j	. . . 4 ⊢ 𝐽 = (TopOpen‘𝑇)
10		rhmpreimacn.a	. . . 4 ⊢ 𝐴 = (PrmIdeal‘𝑅)
11	8, 9, 10	zartopon 34018	. . 3 ⊢ (𝑅 ∈ CRing → 𝐽 ∈ (TopOn‘𝐴))
12	7, 11	syl 17	. 2 ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝐴))
13	1	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐵) → 𝑆 ∈ CRing)
14		rhmpreimacn.f	. . . . 5 ⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆))
15	14	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐵) → 𝐹 ∈ (𝑅 RingHom 𝑆))
16		simpr 484	. . . . 5 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐵) → 𝑖 ∈ 𝐵)
17	16, 4	eleqtrdi 2847	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐵) → 𝑖 ∈ (PrmIdeal‘𝑆))
18	10	rhmpreimaprmidl 33508	. . . 4 ⊢ (((𝑆 ∈ CRing ∧ 𝐹 ∈ (𝑅 RingHom 𝑆)) ∧ 𝑖 ∈ (PrmIdeal‘𝑆)) → (◡𝐹 “ 𝑖) ∈ 𝐴)
19	13, 15, 17, 18	syl21anc 838	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐵) → (◡𝐹 “ 𝑖) ∈ 𝐴)
20		rhmpreimacn.g	. . 3 ⊢ 𝐺 = (𝑖 ∈ 𝐵 ↦ (◡𝐹 “ 𝑖))
21	19, 20	fmptd 7064	. 2 ⊢ (𝜑 → 𝐺:𝐵⟶𝐴)
22	4	fvexi 6852	. . . . . . 7 ⊢ 𝐵 ∈ V
23	22	rabex 5279	. . . . . 6 ⊢ {𝑘 ∈ 𝐵 ∣ 𝑗 ⊆ 𝑘} ∈ V
24		sseq1 3948	. . . . . . . 8 ⊢ (𝑙 = 𝑗 → (𝑙 ⊆ 𝑘 ↔ 𝑗 ⊆ 𝑘))
25	24	rabbidv 3397	. . . . . . 7 ⊢ (𝑙 = 𝑗 → {𝑘 ∈ 𝐵 ∣ 𝑙 ⊆ 𝑘} = {𝑘 ∈ 𝐵 ∣ 𝑗 ⊆ 𝑘})
26	25	cbvmptv 5190	. . . . . 6 ⊢ (𝑙 ∈ (LIdeal‘𝑆) ↦ {𝑘 ∈ 𝐵 ∣ 𝑙 ⊆ 𝑘}) = (𝑗 ∈ (LIdeal‘𝑆) ↦ {𝑘 ∈ 𝐵 ∣ 𝑗 ⊆ 𝑘})
27	23, 26	fnmpti 6639	. . . . 5 ⊢ (𝑙 ∈ (LIdeal‘𝑆) ↦ {𝑘 ∈ 𝐵 ∣ 𝑙 ⊆ 𝑘}) Fn (LIdeal‘𝑆)
28	14	ad3antrrr 731	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Clsd‘𝐽)) ∧ 𝑎 ∈ (LIdeal‘𝑅)) ∧ ((𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘})‘𝑎) = 𝑥) → 𝐹 ∈ (𝑅 RingHom 𝑆))
29		rhmpreimacn.1	. . . . . . . . 9 ⊢ (𝜑 → ran 𝐹 = (Base‘𝑆))
30	29	ad3antrrr 731	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Clsd‘𝐽)) ∧ 𝑎 ∈ (LIdeal‘𝑅)) ∧ ((𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘})‘𝑎) = 𝑥) → ran 𝐹 = (Base‘𝑆))
31		simplr 769	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Clsd‘𝐽)) ∧ 𝑎 ∈ (LIdeal‘𝑅)) ∧ ((𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘})‘𝑎) = 𝑥) → 𝑎 ∈ (LIdeal‘𝑅))
32		eqid 2737	. . . . . . . . 9 ⊢ (Base‘𝑆) = (Base‘𝑆)
33		eqid 2737	. . . . . . . . 9 ⊢ (LIdeal‘𝑅) = (LIdeal‘𝑅)
34		eqid 2737	. . . . . . . . 9 ⊢ (LIdeal‘𝑆) = (LIdeal‘𝑆)
35	32, 33, 34	rhmimaidl 33489	. . . . . . . 8 ⊢ ((𝐹 ∈ (𝑅 RingHom 𝑆) ∧ ran 𝐹 = (Base‘𝑆) ∧ 𝑎 ∈ (LIdeal‘𝑅)) → (𝐹 “ 𝑎) ∈ (LIdeal‘𝑆))
36	28, 30, 31, 35	syl3anc 1374	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Clsd‘𝐽)) ∧ 𝑎 ∈ (LIdeal‘𝑅)) ∧ ((𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘})‘𝑎) = 𝑥) → (𝐹 “ 𝑎) ∈ (LIdeal‘𝑆))
37		fveqeq2 6847	. . . . . . . 8 ⊢ (𝑏 = (𝐹 “ 𝑎) → (((𝑙 ∈ (LIdeal‘𝑆) ↦ {𝑘 ∈ 𝐵 ∣ 𝑙 ⊆ 𝑘})‘𝑏) = (◡𝐺 “ 𝑥) ↔ ((𝑙 ∈ (LIdeal‘𝑆) ↦ {𝑘 ∈ 𝐵 ∣ 𝑙 ⊆ 𝑘})‘(𝐹 “ 𝑎)) = (◡𝐺 “ 𝑥)))
38	37	adantl 481	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝑥 ∈ (Clsd‘𝐽)) ∧ 𝑎 ∈ (LIdeal‘𝑅)) ∧ ((𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘})‘𝑎) = 𝑥) ∧ 𝑏 = (𝐹 “ 𝑎)) → (((𝑙 ∈ (LIdeal‘𝑆) ↦ {𝑘 ∈ 𝐵 ∣ 𝑙 ⊆ 𝑘})‘𝑏) = (◡𝐺 “ 𝑥) ↔ ((𝑙 ∈ (LIdeal‘𝑆) ↦ {𝑘 ∈ 𝐵 ∣ 𝑙 ⊆ 𝑘})‘(𝐹 “ 𝑎)) = (◡𝐺 “ 𝑥)))
39	7	ad3antrrr 731	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Clsd‘𝐽)) ∧ 𝑎 ∈ (LIdeal‘𝑅)) ∧ ((𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘})‘𝑎) = 𝑥) → 𝑅 ∈ CRing)
40	1	ad3antrrr 731	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Clsd‘𝐽)) ∧ 𝑎 ∈ (LIdeal‘𝑅)) ∧ ((𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘})‘𝑎) = 𝑥) → 𝑆 ∈ CRing)
41	24	rabbidv 3397	. . . . . . . . . 10 ⊢ (𝑙 = 𝑗 → {𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘} = {𝑘 ∈ 𝐴 ∣ 𝑗 ⊆ 𝑘})
42	41	cbvmptv 5190	. . . . . . . . 9 ⊢ (𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘}) = (𝑗 ∈ (LIdeal‘𝑅) ↦ {𝑘 ∈ 𝐴 ∣ 𝑗 ⊆ 𝑘})
43	8, 2, 10, 4, 9, 3, 20, 39, 40, 28, 30, 31, 42, 26	rhmpreimacnlem 34025	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Clsd‘𝐽)) ∧ 𝑎 ∈ (LIdeal‘𝑅)) ∧ ((𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘})‘𝑎) = 𝑥) → ((𝑙 ∈ (LIdeal‘𝑆) ↦ {𝑘 ∈ 𝐵 ∣ 𝑙 ⊆ 𝑘})‘(𝐹 “ 𝑎)) = (◡𝐺 “ ((𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘})‘𝑎)))
44		simpr 484	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Clsd‘𝐽)) ∧ 𝑎 ∈ (LIdeal‘𝑅)) ∧ ((𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘})‘𝑎) = 𝑥) → ((𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘})‘𝑎) = 𝑥)
45	44	imaeq2d 6023	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Clsd‘𝐽)) ∧ 𝑎 ∈ (LIdeal‘𝑅)) ∧ ((𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘})‘𝑎) = 𝑥) → (◡𝐺 “ ((𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘})‘𝑎)) = (◡𝐺 “ 𝑥))
46	43, 45	eqtrd 2772	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Clsd‘𝐽)) ∧ 𝑎 ∈ (LIdeal‘𝑅)) ∧ ((𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘})‘𝑎) = 𝑥) → ((𝑙 ∈ (LIdeal‘𝑆) ↦ {𝑘 ∈ 𝐵 ∣ 𝑙 ⊆ 𝑘})‘(𝐹 “ 𝑎)) = (◡𝐺 “ 𝑥))
47	36, 38, 46	rspcedvd 3567	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑥 ∈ (Clsd‘𝐽)) ∧ 𝑎 ∈ (LIdeal‘𝑅)) ∧ ((𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘})‘𝑎) = 𝑥) → ∃𝑏 ∈ (LIdeal‘𝑆)((𝑙 ∈ (LIdeal‘𝑆) ↦ {𝑘 ∈ 𝐵 ∣ 𝑙 ⊆ 𝑘})‘𝑏) = (◡𝐺 “ 𝑥))
48	10	fvexi 6852	. . . . . . . . 9 ⊢ 𝐴 ∈ V
49	48	rabex 5279	. . . . . . . 8 ⊢ {𝑘 ∈ 𝐴 ∣ 𝑗 ⊆ 𝑘} ∈ V
50	49, 42	fnmpti 6639	. . . . . . 7 ⊢ (𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘}) Fn (LIdeal‘𝑅)
51		simpr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Clsd‘𝐽)) → 𝑥 ∈ (Clsd‘𝐽))
52	7	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (Clsd‘𝐽)) → 𝑅 ∈ CRing)
53	8, 9, 10, 42	zartopn 34016	. . . . . . . . . 10 ⊢ (𝑅 ∈ CRing → (𝐽 ∈ (TopOn‘𝐴) ∧ ran (𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘}) = (Clsd‘𝐽)))
54	53	simprd 495	. . . . . . . . 9 ⊢ (𝑅 ∈ CRing → ran (𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘}) = (Clsd‘𝐽))
55	52, 54	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (Clsd‘𝐽)) → ran (𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘}) = (Clsd‘𝐽))
56	51, 55	eleqtrrd 2840	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑥 ∈ (Clsd‘𝐽)) → 𝑥 ∈ ran (𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘}))
57		fvelrnb 6898	. . . . . . . 8 ⊢ ((𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘}) Fn (LIdeal‘𝑅) → (𝑥 ∈ ran (𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘}) ↔ ∃𝑎 ∈ (LIdeal‘𝑅)((𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘})‘𝑎) = 𝑥))
58	57	biimpa 476	. . . . . . 7 ⊢ (((𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘}) Fn (LIdeal‘𝑅) ∧ 𝑥 ∈ ran (𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘})) → ∃𝑎 ∈ (LIdeal‘𝑅)((𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘})‘𝑎) = 𝑥)
59	50, 56, 58	sylancr 588	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ (Clsd‘𝐽)) → ∃𝑎 ∈ (LIdeal‘𝑅)((𝑙 ∈ (LIdeal‘𝑅) ↦ {𝑘 ∈ 𝐴 ∣ 𝑙 ⊆ 𝑘})‘𝑎) = 𝑥)
60	47, 59	r19.29a 3146	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ (Clsd‘𝐽)) → ∃𝑏 ∈ (LIdeal‘𝑆)((𝑙 ∈ (LIdeal‘𝑆) ↦ {𝑘 ∈ 𝐵 ∣ 𝑙 ⊆ 𝑘})‘𝑏) = (◡𝐺 “ 𝑥))
61		fvelrnb 6898	. . . . . 6 ⊢ ((𝑙 ∈ (LIdeal‘𝑆) ↦ {𝑘 ∈ 𝐵 ∣ 𝑙 ⊆ 𝑘}) Fn (LIdeal‘𝑆) → ((◡𝐺 “ 𝑥) ∈ ran (𝑙 ∈ (LIdeal‘𝑆) ↦ {𝑘 ∈ 𝐵 ∣ 𝑙 ⊆ 𝑘}) ↔ ∃𝑏 ∈ (LIdeal‘𝑆)((𝑙 ∈ (LIdeal‘𝑆) ↦ {𝑘 ∈ 𝐵 ∣ 𝑙 ⊆ 𝑘})‘𝑏) = (◡𝐺 “ 𝑥)))
62	61	biimpar 477	. . . . 5 ⊢ (((𝑙 ∈ (LIdeal‘𝑆) ↦ {𝑘 ∈ 𝐵 ∣ 𝑙 ⊆ 𝑘}) Fn (LIdeal‘𝑆) ∧ ∃𝑏 ∈ (LIdeal‘𝑆)((𝑙 ∈ (LIdeal‘𝑆) ↦ {𝑘 ∈ 𝐵 ∣ 𝑙 ⊆ 𝑘})‘𝑏) = (◡𝐺 “ 𝑥)) → (◡𝐺 “ 𝑥) ∈ ran (𝑙 ∈ (LIdeal‘𝑆) ↦ {𝑘 ∈ 𝐵 ∣ 𝑙 ⊆ 𝑘}))
63	27, 60, 62	sylancr 588	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (Clsd‘𝐽)) → (◡𝐺 “ 𝑥) ∈ ran (𝑙 ∈ (LIdeal‘𝑆) ↦ {𝑘 ∈ 𝐵 ∣ 𝑙 ⊆ 𝑘}))
64	2, 3, 4, 26	zartopn 34016	. . . . . . 7 ⊢ (𝑆 ∈ CRing → (𝐾 ∈ (TopOn‘𝐵) ∧ ran (𝑙 ∈ (LIdeal‘𝑆) ↦ {𝑘 ∈ 𝐵 ∣ 𝑙 ⊆ 𝑘}) = (Clsd‘𝐾)))
65	64	simprd 495	. . . . . 6 ⊢ (𝑆 ∈ CRing → ran (𝑙 ∈ (LIdeal‘𝑆) ↦ {𝑘 ∈ 𝐵 ∣ 𝑙 ⊆ 𝑘}) = (Clsd‘𝐾))
66	1, 65	syl 17	. . . . 5 ⊢ (𝜑 → ran (𝑙 ∈ (LIdeal‘𝑆) ↦ {𝑘 ∈ 𝐵 ∣ 𝑙 ⊆ 𝑘}) = (Clsd‘𝐾))
67	66	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ (Clsd‘𝐽)) → ran (𝑙 ∈ (LIdeal‘𝑆) ↦ {𝑘 ∈ 𝐵 ∣ 𝑙 ⊆ 𝑘}) = (Clsd‘𝐾))
68	63, 67	eleqtrd 2839	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ (Clsd‘𝐽)) → (◡𝐺 “ 𝑥) ∈ (Clsd‘𝐾))
69	68	ralrimiva 3130	. 2 ⊢ (𝜑 → ∀𝑥 ∈ (Clsd‘𝐽)(◡𝐺 “ 𝑥) ∈ (Clsd‘𝐾))
70		iscncl 23231	. . 3 ⊢ ((𝐾 ∈ (TopOn‘𝐵) ∧ 𝐽 ∈ (TopOn‘𝐴)) → (𝐺 ∈ (𝐾 Cn 𝐽) ↔ (𝐺:𝐵⟶𝐴 ∧ ∀𝑥 ∈ (Clsd‘𝐽)(◡𝐺 “ 𝑥) ∈ (Clsd‘𝐾))))
71	70	biimpar 477	. 2 ⊢ (((𝐾 ∈ (TopOn‘𝐵) ∧ 𝐽 ∈ (TopOn‘𝐴)) ∧ (𝐺:𝐵⟶𝐴 ∧ ∀𝑥 ∈ (Clsd‘𝐽)(◡𝐺 “ 𝑥) ∈ (Clsd‘𝐾))) → 𝐺 ∈ (𝐾 Cn 𝐽))
72	6, 12, 21, 69, 71	syl22anc 839	1 ⊢ (𝜑 → 𝐺 ∈ (𝐾 Cn 𝐽))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∀wral 3052  ∃wrex 3062  {crab 3390   ⊆ wss 3890   ↦ cmpt 5167  ^◡ccnv 5627  ran crn 5629   “ cima 5631   Fn wfn 6491  ⟶wf 6492  ‘cfv 6496  (class class class)co 7364  Basecbs 17176  TopOpenctopn 17381  CRingccrg 20212   RingHom crh 20446  LIdealclidl 21201  TopOnctopon 22872  Clsdccld 22978   Cn ccn 23186  PrmIdealcprmidl 33492  Speccrspec 34003

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5213  ax-sep 5232  ax-nul 5242  ax-pow 5306  ax-pr 5374  ax-un 7686  ax-ac2 10382  ax-cnex 11091  ax-resscn 11092  ax-1cn 11093  ax-icn 11094  ax-addcl 11095  ax-addrcl 11096  ax-mulcl 11097  ax-mulrcl 11098  ax-mulcom 11099  ax-addass 11100  ax-mulass 11101  ax-distr 11102  ax-i2m1 11103  ax-1ne0 11104  ax-1rid 11105  ax-rnegex 11106  ax-rrecex 11107  ax-cnre 11108  ax-pre-lttri 11109  ax-pre-lttrn 11110  ax-pre-ltadd 11111  ax-pre-mulgt0 11112

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-tp 4573  df-op 4575  df-uni 4852  df-int 4891  df-iun 4936  df-iin 4937  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5523  df-eprel 5528  df-po 5536  df-so 5537  df-fr 5581  df-se 5582  df-we 5583  df-xp 5634  df-rel 5635  df-cnv 5636  df-co 5637  df-dm 5638  df-rn 5639  df-res 5640  df-ima 5641  df-pred 6263  df-ord 6324  df-on 6325  df-lim 6326  df-suc 6327  df-iota 6452  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7321  df-ov 7367  df-oprab 7368  df-mpo 7369  df-rpss 7674  df-om 7815  df-1st 7939  df-2nd 7940  df-frecs 8228  df-wrecs 8259  df-recs 8308  df-rdg 8346  df-1o 8402  df-oadd 8406  df-er 8640  df-map 8772  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-dju 9822  df-card 9860  df-ac 10035  df-pnf 11178  df-mnf 11179  df-xr 11180  df-ltxr 11181  df-le 11182  df-sub 11376  df-neg 11377  df-nn 12172  df-2 12241  df-3 12242  df-4 12243  df-5 12244  df-6 12245  df-7 12246  df-8 12247  df-9 12248  df-n0 12435  df-z 12522  df-dec 12642  df-uz 12786  df-fz 13459  df-struct 17114  df-sets 17131  df-slot 17149  df-ndx 17161  df-base 17177  df-ress 17198  df-plusg 17230  df-mulr 17231  df-sca 17233  df-vsca 17234  df-ip 17235  df-tset 17236  df-ple 17237  df-rest 17382  df-topn 17383  df-0g 17401  df-mre 17545  df-mgm 18605  df-sgrp 18684  df-mnd 18700  df-mhm 18748  df-submnd 18749  df-grp 18909  df-minusg 18910  df-sbg 18911  df-subg 19096  df-ghm 19185  df-cntz 19289  df-lsm 19608  df-cmn 19754  df-abl 19755  df-mgp 20119  df-rng 20131  df-ur 20160  df-ring 20213  df-cring 20214  df-rhm 20449  df-subrg 20544  df-lmod 20854  df-lss 20924  df-lsp 20964  df-sra 21165  df-rgmod 21166  df-lidl 21203  df-rsp 21204  df-lpidl 21317  df-top 22856  df-topon 22873  df-cld 22981  df-cn 23189  df-prmidl 33493  df-mxidl 33517  df-idlsrg 33558  df-rspec 34004

This theorem is referenced by: (None)