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 ( 𝐽𝐴 → ( 𝐽 ∈ Top ↔ ( ∀ 𝑥 ( 𝑥𝐽 𝑥𝐽 ) ∧ ∀ 𝑥 ( ( 𝑥𝐽𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin ) → 𝑥𝐽 ) ) ) )

Proof

Step Hyp Ref Expression
1 istopg ( 𝐽𝐴 → ( 𝐽 ∈ Top ↔ ( ∀ 𝑥 ( 𝑥𝐽 𝑥𝐽 ) ∧ ∀ 𝑥𝐽𝑦𝐽 ( 𝑥𝑦 ) ∈ 𝐽 ) ) )
2 fiint ( ∀ 𝑥𝐽𝑦𝐽 ( 𝑥𝑦 ) ∈ 𝐽 ↔ ∀ 𝑥 ( ( 𝑥𝐽𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin ) → 𝑥𝐽 ) )
3 2 anbi2i ( ( ∀ 𝑥 ( 𝑥𝐽 𝑥𝐽 ) ∧ ∀ 𝑥𝐽𝑦𝐽 ( 𝑥𝑦 ) ∈ 𝐽 ) ↔ ( ∀ 𝑥 ( 𝑥𝐽 𝑥𝐽 ) ∧ ∀ 𝑥 ( ( 𝑥𝐽𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin ) → 𝑥𝐽 ) ) )
4 1 3 bitrdi ( 𝐽𝐴 → ( 𝐽 ∈ Top ↔ ( ∀ 𝑥 ( 𝑥𝐽 𝑥𝐽 ) ∧ ∀ 𝑥 ( ( 𝑥𝐽𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin ) → 𝑥𝐽 ) ) ) )