Metamath Proof Explorer


Theorem opndisj

Description: Two ways of saying that two open sets are disjoint, if J is a topology and X is an open set. (Contributed by Zhi Wang, 6-Sep-2024)

Ref Expression
Assertion opndisj
|- ( Z = ( U. J \ X ) -> ( Y e. ( J i^i ~P Z ) <-> ( Y e. J /\ ( X i^i Y ) = (/) ) ) )

Proof

Step Hyp Ref Expression
1 elpwg
 |-  ( Y e. J -> ( Y e. ~P Z <-> Y C_ Z ) )
2 sseq2
 |-  ( Z = ( U. J \ X ) -> ( Y C_ Z <-> Y C_ ( U. J \ X ) ) )
3 1 2 sylan9bbr
 |-  ( ( Z = ( U. J \ X ) /\ Y e. J ) -> ( Y e. ~P Z <-> Y C_ ( U. J \ X ) ) )
4 3 pm5.32da
 |-  ( Z = ( U. J \ X ) -> ( ( Y e. J /\ Y e. ~P Z ) <-> ( Y e. J /\ Y C_ ( U. J \ X ) ) ) )
5 elin
 |-  ( Y e. ( J i^i ~P Z ) <-> ( Y e. J /\ Y e. ~P Z ) )
6 elssuni
 |-  ( Y e. J -> Y C_ U. J )
7 incom
 |-  ( X i^i Y ) = ( Y i^i X )
8 7 eqeq1i
 |-  ( ( X i^i Y ) = (/) <-> ( Y i^i X ) = (/) )
9 reldisj
 |-  ( Y C_ U. J -> ( ( Y i^i X ) = (/) <-> Y C_ ( U. J \ X ) ) )
10 8 9 syl5bb
 |-  ( Y C_ U. J -> ( ( X i^i Y ) = (/) <-> Y C_ ( U. J \ X ) ) )
11 6 10 syl
 |-  ( Y e. J -> ( ( X i^i Y ) = (/) <-> Y C_ ( U. J \ X ) ) )
12 11 pm5.32i
 |-  ( ( Y e. J /\ ( X i^i Y ) = (/) ) <-> ( Y e. J /\ Y C_ ( U. J \ X ) ) )
13 4 5 12 3bitr4g
 |-  ( Z = ( U. J \ X ) -> ( Y e. ( J i^i ~P Z ) <-> ( Y e. J /\ ( X i^i Y ) = (/) ) ) )