This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ustssel

Description: A uniform structure is upward closed. Condition F_I of BourbakiTop1 p. I.36. (Contributed by Thierry Arnoux, 19-Nov-2017) (Proof shortened by AV, 17-Sep-2021)

Ref Expression
Assertion ustssel ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ∧ 𝑊 ⊆ ( 𝑋 × 𝑋 ) ) → ( 𝑉 ⊆ 𝑊 → 𝑊 ∈ 𝑈 ) )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ∧ 𝑊 ⊆ ( 𝑋 × 𝑋 ) ) → 𝑈 ∈ ( UnifOn ‘ 𝑋 ) )
2 1 elfvexd ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ∧ 𝑊 ⊆ ( 𝑋 × 𝑋 ) ) → 𝑋 ∈ V )
3 isust ⊢ ( 𝑋 ∈ V → ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ↔ ( 𝑈 ⊆ 𝒫 ( 𝑋 × 𝑋 ) ∧ ( 𝑋 × 𝑋 ) ∈ 𝑈 ∧ ∀ 𝑣 ∈ 𝑈 ( ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈 ) ∧ ∀ 𝑤 ∈ 𝑈 ( 𝑣 ∩ 𝑤 ) ∈ 𝑈 ∧ ( ( I ↾ 𝑋 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑈 ∧ ∃ 𝑤 ∈ 𝑈 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) ) )
4 2 3 syl ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ∧ 𝑊 ⊆ ( 𝑋 × 𝑋 ) ) → ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ↔ ( 𝑈 ⊆ 𝒫 ( 𝑋 × 𝑋 ) ∧ ( 𝑋 × 𝑋 ) ∈ 𝑈 ∧ ∀ 𝑣 ∈ 𝑈 ( ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈 ) ∧ ∀ 𝑤 ∈ 𝑈 ( 𝑣 ∩ 𝑤 ) ∈ 𝑈 ∧ ( ( I ↾ 𝑋 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑈 ∧ ∃ 𝑤 ∈ 𝑈 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) ) )
5 1 4 mpbid ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ∧ 𝑊 ⊆ ( 𝑋 × 𝑋 ) ) → ( 𝑈 ⊆ 𝒫 ( 𝑋 × 𝑋 ) ∧ ( 𝑋 × 𝑋 ) ∈ 𝑈 ∧ ∀ 𝑣 ∈ 𝑈 ( ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈 ) ∧ ∀ 𝑤 ∈ 𝑈 ( 𝑣 ∩ 𝑤 ) ∈ 𝑈 ∧ ( ( I ↾ 𝑋 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑈 ∧ ∃ 𝑤 ∈ 𝑈 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) )
6 5 simp3d ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ∧ 𝑊 ⊆ ( 𝑋 × 𝑋 ) ) → ∀ 𝑣 ∈ 𝑈 ( ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈 ) ∧ ∀ 𝑤 ∈ 𝑈 ( 𝑣 ∩ 𝑤 ) ∈ 𝑈 ∧ ( ( I ↾ 𝑋 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑈 ∧ ∃ 𝑤 ∈ 𝑈 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) )
7 simp1 ⊢ ( ( ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈 ) ∧ ∀ 𝑤 ∈ 𝑈 ( 𝑣 ∩ 𝑤 ) ∈ 𝑈 ∧ ( ( I ↾ 𝑋 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑈 ∧ ∃ 𝑤 ∈ 𝑈 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) → ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈 ) )
8 7 ralimi ⊢ ( ∀ 𝑣 ∈ 𝑈 ( ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈 ) ∧ ∀ 𝑤 ∈ 𝑈 ( 𝑣 ∩ 𝑤 ) ∈ 𝑈 ∧ ( ( I ↾ 𝑋 ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑈 ∧ ∃ 𝑤 ∈ 𝑈 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) → ∀ 𝑣 ∈ 𝑈 ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈 ) )
9 6 8 syl ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ∧ 𝑊 ⊆ ( 𝑋 × 𝑋 ) ) → ∀ 𝑣 ∈ 𝑈 ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈 ) )
10 simp2 ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ∧ 𝑊 ⊆ ( 𝑋 × 𝑋 ) ) → 𝑉 ∈ 𝑈 )
11 2 2 xpexd ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ∧ 𝑊 ⊆ ( 𝑋 × 𝑋 ) ) → ( 𝑋 × 𝑋 ) ∈ V )
12 simp3 ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ∧ 𝑊 ⊆ ( 𝑋 × 𝑋 ) ) → 𝑊 ⊆ ( 𝑋 × 𝑋 ) )
13 11 12 sselpwd ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ∧ 𝑊 ⊆ ( 𝑋 × 𝑋 ) ) → 𝑊 ∈ 𝒫 ( 𝑋 × 𝑋 ) )
14 sseq1 ⊢ ( 𝑣 = 𝑉 → ( 𝑣 ⊆ 𝑤 ↔ 𝑉 ⊆ 𝑤 ) )
15 14 imbi1d ⊢ ( 𝑣 = 𝑉 → ( ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈 ) ↔ ( 𝑉 ⊆ 𝑤 → 𝑤 ∈ 𝑈 ) ) )
16 sseq2 ⊢ ( 𝑤 = 𝑊 → ( 𝑉 ⊆ 𝑤 ↔ 𝑉 ⊆ 𝑊 ) )
17 eleq1 ⊢ ( 𝑤 = 𝑊 → ( 𝑤 ∈ 𝑈 ↔ 𝑊 ∈ 𝑈 ) )
18 16 17 imbi12d ⊢ ( 𝑤 = 𝑊 → ( ( 𝑉 ⊆ 𝑤 → 𝑤 ∈ 𝑈 ) ↔ ( 𝑉 ⊆ 𝑊 → 𝑊 ∈ 𝑈 ) ) )
19 15 18 rspc2v ⊢ ( ( 𝑉 ∈ 𝑈 ∧ 𝑊 ∈ 𝒫 ( 𝑋 × 𝑋 ) ) → ( ∀ 𝑣 ∈ 𝑈 ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈 ) → ( 𝑉 ⊆ 𝑊 → 𝑊 ∈ 𝑈 ) ) )
20 10 13 19 syl2anc ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ∧ 𝑊 ⊆ ( 𝑋 × 𝑋 ) ) → ( ∀ 𝑣 ∈ 𝑈 ∀ 𝑤 ∈ 𝒫 ( 𝑋 × 𝑋 ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑈 ) → ( 𝑉 ⊆ 𝑊 → 𝑊 ∈ 𝑈 ) ) )
21 9 20 mpd ⊢ ( ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) ∧ 𝑉 ∈ 𝑈 ∧ 𝑊 ⊆ ( 𝑋 × 𝑋 ) ) → ( 𝑉 ⊆ 𝑊 → 𝑊 ∈ 𝑈 ) )