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

Metamath Proof Explorer

Theorem istop2g

Description: Express the predicate " J is a topology" using nonempty finite intersections instead of binary intersections as in istopg . (Contributed by NM, 19-Jul-2006)

Ref Expression
Assertion istop2g ⊢ J ∈ A → J ∈ Top ↔ ∀ x x ⊆ J → ⋃ x ∈ J ∧ ∀ x x ⊆ J ∧ x ≠ ∅ ∧ x ∈ Fin → ⋂ x ∈ J

Proof

Step Hyp Ref Expression
1 istopg ⊢ J ∈ A → J ∈ Top ↔ ∀ x x ⊆ J → ⋃ x ∈ J ∧ ∀ x ∈ J ∀ y ∈ J x ∩ y ∈ J
2 fiint ⊢ ∀ x ∈ J ∀ y ∈ J x ∩ y ∈ J ↔ ∀ x x ⊆ J ∧ x ≠ ∅ ∧ x ∈ Fin → ⋂ x ∈ J
3 2 anbi2i ⊢ ∀ x x ⊆ J → ⋃ x ∈ J ∧ ∀ x ∈ J ∀ y ∈ J x ∩ y ∈ J ↔ ∀ x x ⊆ J → ⋃ x ∈ J ∧ ∀ x x ⊆ J ∧ x ≠ ∅ ∧ x ∈ Fin → ⋂ x ∈ J
4 1 3 bitrdi ⊢ J ∈ A → J ∈ Top ↔ ∀ x x ⊆ J → ⋃ x ∈ J ∧ ∀ x x ⊆ J ∧ x ≠ ∅ ∧ x ∈ Fin → ⋂ x ∈ J