Description: The topology generation function is one-to-one when applied to completed topologies. (Contributed by NM, 18-Jul-2006)
Ref | Expression | ||
---|---|---|---|
Assertion | tgtop11 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tgtop | |
|
2 | tgtop | |
|
3 | 1 2 | eqeqan12d | |
4 | 3 | biimp3a | |