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 e. A -> ( J e. Top <-> ( A. x ( x C_ J -> U. x e. J ) /\ A. x e. J A. y e. J ( x i^i y ) e. J ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pweq | |- ( z = J -> ~P z = ~P J ) |
|
2 | eleq2 | |- ( z = J -> ( U. x e. z <-> U. x e. J ) ) |
|
3 | 1 2 | raleqbidv | |- ( z = J -> ( A. x e. ~P z U. x e. z <-> A. x e. ~P J U. x e. J ) ) |
4 | eleq2 | |- ( z = J -> ( ( x i^i y ) e. z <-> ( x i^i y ) e. J ) ) |
|
5 | 4 | raleqbi1dv | |- ( z = J -> ( A. y e. z ( x i^i y ) e. z <-> A. y e. J ( x i^i y ) e. J ) ) |
6 | 5 | raleqbi1dv | |- ( z = J -> ( A. x e. z A. y e. z ( x i^i y ) e. z <-> A. x e. J A. y e. J ( x i^i y ) e. J ) ) |
7 | 3 6 | anbi12d | |- ( z = J -> ( ( A. x e. ~P z U. x e. z /\ A. x e. z A. y e. z ( x i^i y ) e. z ) <-> ( A. x e. ~P J U. x e. J /\ A. x e. J A. y e. J ( x i^i y ) e. J ) ) ) |
8 | df-top | |- Top = { z | ( A. x e. ~P z U. x e. z /\ A. x e. z A. y e. z ( x i^i y ) e. z ) } |
|
9 | 7 8 | elab2g | |- ( J e. A -> ( J e. Top <-> ( A. x e. ~P J U. x e. J /\ A. x e. J A. y e. J ( x i^i y ) e. J ) ) ) |
10 | df-ral | |- ( A. x e. ~P J U. x e. J <-> A. x ( x e. ~P J -> U. x e. J ) ) |
|
11 | elpw2g | |- ( J e. A -> ( x e. ~P J <-> x C_ J ) ) |
|
12 | 11 | imbi1d | |- ( J e. A -> ( ( x e. ~P J -> U. x e. J ) <-> ( x C_ J -> U. x e. J ) ) ) |
13 | 12 | albidv | |- ( J e. A -> ( A. x ( x e. ~P J -> U. x e. J ) <-> A. x ( x C_ J -> U. x e. J ) ) ) |
14 | 10 13 | syl5bb | |- ( J e. A -> ( A. x e. ~P J U. x e. J <-> A. x ( x C_ J -> U. x e. J ) ) ) |
15 | 14 | anbi1d | |- ( J e. A -> ( ( A. x e. ~P J U. x e. J /\ A. x e. J A. y e. J ( x i^i y ) e. J ) <-> ( A. x ( x C_ J -> U. x e. J ) /\ A. x e. J A. y e. J ( x i^i y ) e. J ) ) ) |
16 | 9 15 | bitrd | |- ( J e. A -> ( J e. Top <-> ( A. x ( x C_ J -> U. x e. J ) /\ A. x e. J A. y e. J ( x i^i y ) e. J ) ) ) |