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 ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ) → ◡ 𝑉 ∈ 𝑈 )