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