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	⊢ ( 𝑍 = ( ∪ 𝐽 ∖ 𝑋 ) → ( 𝑌 ∈ ( 𝐽 ∩ 𝒫 𝑍 ) ↔ ( 𝑌 ∈ 𝐽 ∧ ( 𝑋 ∩ 𝑌 ) = ∅ ) ) )

Proof

Step	Hyp	Ref	Expression
1		elpwg	⊢ ( 𝑌 ∈ 𝐽 → ( 𝑌 ∈ 𝒫 𝑍 ↔ 𝑌 ⊆ 𝑍 ) )
2		sseq2	⊢ ( 𝑍 = ( ∪ 𝐽 ∖ 𝑋 ) → ( 𝑌 ⊆ 𝑍 ↔ 𝑌 ⊆ ( ∪ 𝐽 ∖ 𝑋 ) ) )
3	1 2	sylan9bbr	⊢ ( ( 𝑍 = ( ∪ 𝐽 ∖ 𝑋 ) ∧ 𝑌 ∈ 𝐽 ) → ( 𝑌 ∈ 𝒫 𝑍 ↔ 𝑌 ⊆ ( ∪ 𝐽 ∖ 𝑋 ) ) )
4	3	pm5.32da	⊢ ( 𝑍 = ( ∪ 𝐽 ∖ 𝑋 ) → ( ( 𝑌 ∈ 𝐽 ∧ 𝑌 ∈ 𝒫 𝑍 ) ↔ ( 𝑌 ∈ 𝐽 ∧ 𝑌 ⊆ ( ∪ 𝐽 ∖ 𝑋 ) ) ) )
5		elin	⊢ ( 𝑌 ∈ ( 𝐽 ∩ 𝒫 𝑍 ) ↔ ( 𝑌 ∈ 𝐽 ∧ 𝑌 ∈ 𝒫 𝑍 ) )
6		elssuni	⊢ ( 𝑌 ∈ 𝐽 → 𝑌 ⊆ ∪ 𝐽 )
7		incom	⊢ ( 𝑋 ∩ 𝑌 ) = ( 𝑌 ∩ 𝑋 )
8	7	eqeq1i	⊢ ( ( 𝑋 ∩ 𝑌 ) = ∅ ↔ ( 𝑌 ∩ 𝑋 ) = ∅ )
9		reldisj	⊢ ( 𝑌 ⊆ ∪ 𝐽 → ( ( 𝑌 ∩ 𝑋 ) = ∅ ↔ 𝑌 ⊆ ( ∪ 𝐽 ∖ 𝑋 ) ) )
10	8 9	bitrid	⊢ ( 𝑌 ⊆ ∪ 𝐽 → ( ( 𝑋 ∩ 𝑌 ) = ∅ ↔ 𝑌 ⊆ ( ∪ 𝐽 ∖ 𝑋 ) ) )
11	6 10	syl	⊢ ( 𝑌 ∈ 𝐽 → ( ( 𝑋 ∩ 𝑌 ) = ∅ ↔ 𝑌 ⊆ ( ∪ 𝐽 ∖ 𝑋 ) ) )
12	11	pm5.32i	⊢ ( ( 𝑌 ∈ 𝐽 ∧ ( 𝑋 ∩ 𝑌 ) = ∅ ) ↔ ( 𝑌 ∈ 𝐽 ∧ 𝑌 ⊆ ( ∪ 𝐽 ∖ 𝑋 ) ) )
13	4 5 12	3bitr4g	⊢ ( 𝑍 = ( ∪ 𝐽 ∖ 𝑋 ) → ( 𝑌 ∈ ( 𝐽 ∩ 𝒫 𝑍 ) ↔ ( 𝑌 ∈ 𝐽 ∧ ( 𝑋 ∩ 𝑌 ) = ∅ ) ) )