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 JAJTopxxJxJxxJxxFinxJ

Proof

Step Hyp Ref Expression
1 istopg JAJTopxxJxJxJyJxyJ
2 fiint xJyJxyJxxJxxFinxJ
3 2 anbi2i xxJxJxJyJxyJxxJxJxxJxxFinxJ
4 1 3 bitrdi JAJTopxxJxJxxJxxFinxJ