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 ) = (/) ) ) )