Metamath Proof Explorer

Theorem clddisj

Description: Two ways of saying that two closed sets are disjoint, if J is a topology and X is a closed set. An alternative proof is similar to that of opndisj with elssuni replaced by the combination of cldss and eqid . (Contributed by Zhi Wang, 6-Sep-2024)

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

Proof

Step Hyp Ref Expression
1 elin 
 |-  ( Y e. ( ( Clsd ` J ) i^i ~P Z ) <-> ( Y e. ( Clsd ` J ) /\ Y e. ~P Z ) )
2 simpl 
 |-  ( ( Z = ( U. J \ X ) /\ Y e. ( Clsd ` J ) ) -> Z = ( U. J \ X ) )
3 cldrcl 
 |-  ( Y e. ( Clsd ` J ) -> J e. Top )
4 clduni 
 |-  ( J e. Top -> U. ( Clsd ` J ) = U. J )
5 4 difeq1d 
 |-  ( J e. Top -> ( U. ( Clsd ` J ) \ X ) = ( U. J \ X ) )
6 3 5 syl 
 |-  ( Y e. ( Clsd ` J ) -> ( U. ( Clsd ` J ) \ X ) = ( U. J \ X ) )
7 6 adantl 
 |-  ( ( Z = ( U. J \ X ) /\ Y e. ( Clsd ` J ) ) -> ( U. ( Clsd ` J ) \ X ) = ( U. J \ X ) )
8 2 7 eqtr4d 
 |-  ( ( Z = ( U. J \ X ) /\ Y e. ( Clsd ` J ) ) -> Z = ( U. ( Clsd ` J ) \ X ) )
9 opndisj 
 |-  ( Z = ( U. ( Clsd ` J ) \ X ) -> ( Y e. ( ( Clsd ` J ) i^i ~P Z ) <-> ( Y e. ( Clsd ` J ) /\ ( X i^i Y ) = (/) ) ) )
10 1 9 bitr3id 
 |-  ( Z = ( U. ( Clsd ` J ) \ X ) -> ( ( Y e. ( Clsd ` J ) /\ Y e. ~P Z ) <-> ( Y e. ( Clsd ` J ) /\ ( X i^i Y ) = (/) ) ) )
11 10 pm5.32dra 
 |-  ( ( Z = ( U. ( Clsd ` J ) \ X ) /\ Y e. ( Clsd ` J ) ) -> ( Y e. ~P Z <-> ( X i^i Y ) = (/) ) )
12 8 11 sylancom 
 |-  ( ( Z = ( U. J \ X ) /\ Y e. ( Clsd ` J ) ) -> ( Y e. ~P Z <-> ( X i^i Y ) = (/) ) )
13 12 pm5.32da 
 |-  ( Z = ( U. J \ X ) -> ( ( Y e. ( Clsd ` J ) /\ Y e. ~P Z ) <-> ( Y e. ( Clsd ` J ) /\ ( X i^i Y ) = (/) ) ) )
14 1 13 bitrid 
 |-  ( Z = ( U. J \ X ) -> ( Y e. ( ( Clsd ` J ) i^i ~P Z ) <-> ( Y e. ( Clsd ` J ) /\ ( X i^i Y ) = (/) ) ) )