Theorem ucnprima

Description: The preimage by a uniformly continuous function F of an entourage W of Y is an entourage of X . Note of the definition 1 of BourbakiTop1 p. II.6. (Contributed by Thierry Arnoux, 19-Nov-2017)

	Ref	Expression
Hypotheses	ucnprima.1	⊢ ( 𝜑 → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
	ucnprima.2	⊢ ( 𝜑 → 𝑉 ∈ ( UnifOn ‘ 𝑌 ) )
	ucnprima.3	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑈 Cnu 𝑉 ) )
	ucnprima.4	⊢ ( 𝜑 → 𝑊 ∈ 𝑉 )
	ucnprima.5	⊢ 𝐺 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ )
Assertion	ucnprima	⊢ ( 𝜑 → ( ◡ 𝐺 “ 𝑊 ) ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		ucnprima.1	⊢ ( 𝜑 → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
2		ucnprima.2	⊢ ( 𝜑 → 𝑉 ∈ ( UnifOn ‘ 𝑌 ) )
3		ucnprima.3	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑈 Cnu 𝑉 ) )
4		ucnprima.4	⊢ ( 𝜑 → 𝑊 ∈ 𝑉 )
5		ucnprima.5	⊢ 𝐺 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ )
6	1 2 3 4 5	ucnima	⊢ ( 𝜑 → ∃ 𝑟 ∈ 𝑈 ( 𝐺 “ 𝑟 ) ⊆ 𝑊 )
7	5	mpofun	⊢ Fun 𝐺
8		ustssxp	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑟 ∈ 𝑈 ) → 𝑟 ⊆ ( 𝑋 × 𝑋 ) )
9	1 8	sylan	⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑈 ) → 𝑟 ⊆ ( 𝑋 × 𝑋 ) )
10		opex	⊢ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐹 ‘ 𝑦 ) ⟩ ∈ V
11	5 10	dmmpo	⊢ dom 𝐺 = ( 𝑋 × 𝑋 )
12	9 11	sseqtrrdi	⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑈 ) → 𝑟 ⊆ dom 𝐺 )
13		funimass3	⊢ ( ( Fun 𝐺 ∧ 𝑟 ⊆ dom 𝐺 ) → ( ( 𝐺 “ 𝑟 ) ⊆ 𝑊 ↔ 𝑟 ⊆ ( ◡ 𝐺 “ 𝑊 ) ) )
14	7 12 13	sylancr	⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑈 ) → ( ( 𝐺 “ 𝑟 ) ⊆ 𝑊 ↔ 𝑟 ⊆ ( ◡ 𝐺 “ 𝑊 ) ) )
15	14	rexbidva	⊢ ( 𝜑 → ( ∃ 𝑟 ∈ 𝑈 ( 𝐺 “ 𝑟 ) ⊆ 𝑊 ↔ ∃ 𝑟 ∈ 𝑈 𝑟 ⊆ ( ◡ 𝐺 “ 𝑊 ) ) )
16	6 15	mpbid	⊢ ( 𝜑 → ∃ 𝑟 ∈ 𝑈 𝑟 ⊆ ( ◡ 𝐺 “ 𝑊 ) )
17	1	adantr	⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑈 ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
18		simpr	⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑈 ) → 𝑟 ∈ 𝑈 )
19		cnvimass	⊢ ( ◡ 𝐺 “ 𝑊 ) ⊆ dom 𝐺
20	19 11	sseqtri	⊢ ( ◡ 𝐺 “ 𝑊 ) ⊆ ( 𝑋 × 𝑋 )
21	20	a1i	⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑈 ) → ( ◡ 𝐺 “ 𝑊 ) ⊆ ( 𝑋 × 𝑋 ) )
22		ustssel	⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑟 ∈ 𝑈 ∧ ( ◡ 𝐺 “ 𝑊 ) ⊆ ( 𝑋 × 𝑋 ) ) → ( 𝑟 ⊆ ( ◡ 𝐺 “ 𝑊 ) → ( ◡ 𝐺 “ 𝑊 ) ∈ 𝑈 ) )
23	17 18 21 22	syl3anc	⊢ ( ( 𝜑 ∧ 𝑟 ∈ 𝑈 ) → ( 𝑟 ⊆ ( ◡ 𝐺 “ 𝑊 ) → ( ◡ 𝐺 “ 𝑊 ) ∈ 𝑈 ) )
24	23	rexlimdva	⊢ ( 𝜑 → ( ∃ 𝑟 ∈ 𝑈 𝑟 ⊆ ( ◡ 𝐺 “ 𝑊 ) → ( ◡ 𝐺 “ 𝑊 ) ∈ 𝑈 ) )
25	16 24	mpd	⊢ ( 𝜑 → ( ◡ 𝐺 “ 𝑊 ) ∈ 𝑈 )