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
|
syl5bb |
⊢ ( 𝑌 ⊆ ∪ 𝐽 → ( ( 𝑋 ∩ 𝑌 ) = ∅ ↔ 𝑌 ⊆ ( ∪ 𝐽 ∖ 𝑋 ) ) ) |
11 |
6 10
|
syl |
⊢ ( 𝑌 ∈ 𝐽 → ( ( 𝑋 ∩ 𝑌 ) = ∅ ↔ 𝑌 ⊆ ( ∪ 𝐽 ∖ 𝑋 ) ) ) |
12 |
11
|
pm5.32i |
⊢ ( ( 𝑌 ∈ 𝐽 ∧ ( 𝑋 ∩ 𝑌 ) = ∅ ) ↔ ( 𝑌 ∈ 𝐽 ∧ 𝑌 ⊆ ( ∪ 𝐽 ∖ 𝑋 ) ) ) |
13 |
4 5 12
|
3bitr4g |
⊢ ( 𝑍 = ( ∪ 𝐽 ∖ 𝑋 ) → ( 𝑌 ∈ ( 𝐽 ∩ 𝒫 𝑍 ) ↔ ( 𝑌 ∈ 𝐽 ∧ ( 𝑋 ∩ 𝑌 ) = ∅ ) ) ) |