Metamath Proof Explorer


Theorem ustinvel

Description: If V is an entourage, so is its inverse. Condition U_II of BourbakiTop1 p. II.1. (Contributed by Thierry Arnoux, 2-Dec-2017)

Ref Expression
Assertion ustinvel ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉𝑈 ) → 𝑉𝑈 )

Proof

Step Hyp Ref Expression
1 elfvex ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑋 ∈ V )
2 isust ( 𝑋 ∈ V → ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ↔ ( 𝑈 ⊆ 𝒫 ( 𝑋 × 𝑋 ) ∧ ( 𝑋 × 𝑋 ) ∈ 𝑈 ∧ ∀ 𝑣𝑈 ( ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣𝑤𝑤𝑈 ) ∧ ∀ 𝑤𝑈 ( 𝑣𝑤 ) ∈ 𝑈 ∧ ( ( I ↾ 𝑋 ) ⊆ 𝑣 𝑣𝑈 ∧ ∃ 𝑤𝑈 ( 𝑤𝑤 ) ⊆ 𝑣 ) ) ) ) )
3 1 2 syl ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ↔ ( 𝑈 ⊆ 𝒫 ( 𝑋 × 𝑋 ) ∧ ( 𝑋 × 𝑋 ) ∈ 𝑈 ∧ ∀ 𝑣𝑈 ( ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣𝑤𝑤𝑈 ) ∧ ∀ 𝑤𝑈 ( 𝑣𝑤 ) ∈ 𝑈 ∧ ( ( I ↾ 𝑋 ) ⊆ 𝑣 𝑣𝑈 ∧ ∃ 𝑤𝑈 ( 𝑤𝑤 ) ⊆ 𝑣 ) ) ) ) )
4 3 ibi ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝑈 ⊆ 𝒫 ( 𝑋 × 𝑋 ) ∧ ( 𝑋 × 𝑋 ) ∈ 𝑈 ∧ ∀ 𝑣𝑈 ( ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣𝑤𝑤𝑈 ) ∧ ∀ 𝑤𝑈 ( 𝑣𝑤 ) ∈ 𝑈 ∧ ( ( I ↾ 𝑋 ) ⊆ 𝑣 𝑣𝑈 ∧ ∃ 𝑤𝑈 ( 𝑤𝑤 ) ⊆ 𝑣 ) ) ) )
5 4 simp3d ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ∀ 𝑣𝑈 ( ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣𝑤𝑤𝑈 ) ∧ ∀ 𝑤𝑈 ( 𝑣𝑤 ) ∈ 𝑈 ∧ ( ( I ↾ 𝑋 ) ⊆ 𝑣 𝑣𝑈 ∧ ∃ 𝑤𝑈 ( 𝑤𝑤 ) ⊆ 𝑣 ) ) )
6 sseq1 ( 𝑣 = 𝑉 → ( 𝑣𝑤𝑉𝑤 ) )
7 6 imbi1d ( 𝑣 = 𝑉 → ( ( 𝑣𝑤𝑤𝑈 ) ↔ ( 𝑉𝑤𝑤𝑈 ) ) )
8 7 ralbidv ( 𝑣 = 𝑉 → ( ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣𝑤𝑤𝑈 ) ↔ ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑉𝑤𝑤𝑈 ) ) )
9 ineq1 ( 𝑣 = 𝑉 → ( 𝑣𝑤 ) = ( 𝑉𝑤 ) )
10 9 eleq1d ( 𝑣 = 𝑉 → ( ( 𝑣𝑤 ) ∈ 𝑈 ↔ ( 𝑉𝑤 ) ∈ 𝑈 ) )
11 10 ralbidv ( 𝑣 = 𝑉 → ( ∀ 𝑤𝑈 ( 𝑣𝑤 ) ∈ 𝑈 ↔ ∀ 𝑤𝑈 ( 𝑉𝑤 ) ∈ 𝑈 ) )
12 sseq2 ( 𝑣 = 𝑉 → ( ( I ↾ 𝑋 ) ⊆ 𝑣 ↔ ( I ↾ 𝑋 ) ⊆ 𝑉 ) )
13 cnveq ( 𝑣 = 𝑉 𝑣 = 𝑉 )
14 13 eleq1d ( 𝑣 = 𝑉 → ( 𝑣𝑈 𝑉𝑈 ) )
15 sseq2 ( 𝑣 = 𝑉 → ( ( 𝑤𝑤 ) ⊆ 𝑣 ↔ ( 𝑤𝑤 ) ⊆ 𝑉 ) )
16 15 rexbidv ( 𝑣 = 𝑉 → ( ∃ 𝑤𝑈 ( 𝑤𝑤 ) ⊆ 𝑣 ↔ ∃ 𝑤𝑈 ( 𝑤𝑤 ) ⊆ 𝑉 ) )
17 12 14 16 3anbi123d ( 𝑣 = 𝑉 → ( ( ( I ↾ 𝑋 ) ⊆ 𝑣 𝑣𝑈 ∧ ∃ 𝑤𝑈 ( 𝑤𝑤 ) ⊆ 𝑣 ) ↔ ( ( I ↾ 𝑋 ) ⊆ 𝑉 𝑉𝑈 ∧ ∃ 𝑤𝑈 ( 𝑤𝑤 ) ⊆ 𝑉 ) ) )
18 8 11 17 3anbi123d ( 𝑣 = 𝑉 → ( ( ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣𝑤𝑤𝑈 ) ∧ ∀ 𝑤𝑈 ( 𝑣𝑤 ) ∈ 𝑈 ∧ ( ( I ↾ 𝑋 ) ⊆ 𝑣 𝑣𝑈 ∧ ∃ 𝑤𝑈 ( 𝑤𝑤 ) ⊆ 𝑣 ) ) ↔ ( ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑉𝑤𝑤𝑈 ) ∧ ∀ 𝑤𝑈 ( 𝑉𝑤 ) ∈ 𝑈 ∧ ( ( I ↾ 𝑋 ) ⊆ 𝑉 𝑉𝑈 ∧ ∃ 𝑤𝑈 ( 𝑤𝑤 ) ⊆ 𝑉 ) ) ) )
19 18 rspcv ( 𝑉𝑈 → ( ∀ 𝑣𝑈 ( ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣𝑤𝑤𝑈 ) ∧ ∀ 𝑤𝑈 ( 𝑣𝑤 ) ∈ 𝑈 ∧ ( ( I ↾ 𝑋 ) ⊆ 𝑣 𝑣𝑈 ∧ ∃ 𝑤𝑈 ( 𝑤𝑤 ) ⊆ 𝑣 ) ) → ( ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑉𝑤𝑤𝑈 ) ∧ ∀ 𝑤𝑈 ( 𝑉𝑤 ) ∈ 𝑈 ∧ ( ( I ↾ 𝑋 ) ⊆ 𝑉 𝑉𝑈 ∧ ∃ 𝑤𝑈 ( 𝑤𝑤 ) ⊆ 𝑉 ) ) ) )
20 5 19 mpan9 ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉𝑈 ) → ( ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑉𝑤𝑤𝑈 ) ∧ ∀ 𝑤𝑈 ( 𝑉𝑤 ) ∈ 𝑈 ∧ ( ( I ↾ 𝑋 ) ⊆ 𝑉 𝑉𝑈 ∧ ∃ 𝑤𝑈 ( 𝑤𝑤 ) ⊆ 𝑉 ) ) )
21 20 simp3d ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉𝑈 ) → ( ( I ↾ 𝑋 ) ⊆ 𝑉 𝑉𝑈 ∧ ∃ 𝑤𝑈 ( 𝑤𝑤 ) ⊆ 𝑉 ) )
22 21 simp2d ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉𝑈 ) → 𝑉𝑈 )