Metamath Proof Explorer

Theorem istopg

Description: Express the predicate " J is a topology". See istop2g for another characterization using nonempty finite intersections instead of binary intersections.

Note: In the literature, a topology is often represented by a calligraphic letter T, which resembles the letter J. This confusion may have led to J being used by some authors (e.g., K. D. Joshi, Introduction to General Topology (1983), p. 114) and it is convenient for us since we later use T to represent linear transformations (operators). (Contributed by Stefan Allan, 3-Mar-2006) (Revised by Mario Carneiro, 11-Nov-2013)

Ref Expression
Assertion istopg ⊢ J ∈ A → J ∈ Top ↔ ∀ x x ⊆ J → ⋃ x ∈ J ∧ ∀ x ∈ J ∀ y ∈ J x ∩ y ∈ J

Proof

Step Hyp Ref Expression
1 pweq ⊢ z = J → 𝒫 z = 𝒫 J
2 eleq2 ⊢ z = J → ⋃ x ∈ z ↔ ⋃ x ∈ J
3 1 2 raleqbidv ⊢ z = J → ∀ x ∈ 𝒫 z ⋃ x ∈ z ↔ ∀ x ∈ 𝒫 J ⋃ x ∈ J
4 eleq2 ⊢ z = J → x ∩ y ∈ z ↔ x ∩ y ∈ J
5 4 raleqbi1dv ⊢ z = J → ∀ y ∈ z x ∩ y ∈ z ↔ ∀ y ∈ J x ∩ y ∈ J
6 5 raleqbi1dv ⊢ z = J → ∀ x ∈ z ∀ y ∈ z x ∩ y ∈ z ↔ ∀ x ∈ J ∀ y ∈ J x ∩ y ∈ J
7 3 6 anbi12d ⊢ z = J → ∀ x ∈ 𝒫 z ⋃ x ∈ z ∧ ∀ x ∈ z ∀ y ∈ z x ∩ y ∈ z ↔ ∀ x ∈ 𝒫 J ⋃ x ∈ J ∧ ∀ x ∈ J ∀ y ∈ J x ∩ y ∈ J
8 df-top ⊢ Top = z | ∀ x ∈ 𝒫 z ⋃ x ∈ z ∧ ∀ x ∈ z ∀ y ∈ z x ∩ y ∈ z
9 7 8 elab2g ⊢ J ∈ A → J ∈ Top ↔ ∀ x ∈ 𝒫 J ⋃ x ∈ J ∧ ∀ x ∈ J ∀ y ∈ J x ∩ y ∈ J
10 df-ral ⊢ ∀ x ∈ 𝒫 J ⋃ x ∈ J ↔ ∀ x x ∈ 𝒫 J → ⋃ x ∈ J
11 elpw2g ⊢ J ∈ A → x ∈ 𝒫 J ↔ x ⊆ J
12 11 imbi1d ⊢ J ∈ A → x ∈ 𝒫 J → ⋃ x ∈ J ↔ x ⊆ J → ⋃ x ∈ J
13 12 albidv ⊢ J ∈ A → ∀ x x ∈ 𝒫 J → ⋃ x ∈ J ↔ ∀ x x ⊆ J → ⋃ x ∈ J
14 10 13 syl5bb ⊢ J ∈ A → ∀ x ∈ 𝒫 J ⋃ x ∈ J ↔ ∀ x x ⊆ J → ⋃ x ∈ J
15 14 anbi1d ⊢ J ∈ A → ∀ x ∈ 𝒫 J ⋃ x ∈ J ∧ ∀ x ∈ J ∀ y ∈ J x ∩ y ∈ J ↔ ∀ x x ⊆ J → ⋃ x ∈ J ∧ ∀ x ∈ J ∀ y ∈ J x ∩ y ∈ J
16 9 15 bitrd ⊢ J ∈ A → J ∈ Top ↔ ∀ x x ⊆ J → ⋃ x ∈ J ∧ ∀ x ∈ J ∀ y ∈ J x ∩ y ∈ J