Step |
Hyp |
Ref |
Expression |
1 |
|
isros.1 |
|- Q = { s e. ~P ~P O | ( (/) e. s /\ A. x e. s A. y e. s ( ( x u. y ) e. s /\ ( x \ y ) e. s ) ) } |
2 |
|
simp2 |
|- ( ( S e. Q /\ A e. S /\ B e. S ) -> A e. S ) |
3 |
|
simp3 |
|- ( ( S e. Q /\ A e. S /\ B e. S ) -> B e. S ) |
4 |
1
|
isros |
|- ( S e. Q <-> ( S e. ~P ~P O /\ (/) e. S /\ A. u e. S A. v e. S ( ( u u. v ) e. S /\ ( u \ v ) e. S ) ) ) |
5 |
4
|
simp3bi |
|- ( S e. Q -> A. u e. S A. v e. S ( ( u u. v ) e. S /\ ( u \ v ) e. S ) ) |
6 |
5
|
3ad2ant1 |
|- ( ( S e. Q /\ A e. S /\ B e. S ) -> A. u e. S A. v e. S ( ( u u. v ) e. S /\ ( u \ v ) e. S ) ) |
7 |
|
uneq1 |
|- ( u = A -> ( u u. v ) = ( A u. v ) ) |
8 |
7
|
eleq1d |
|- ( u = A -> ( ( u u. v ) e. S <-> ( A u. v ) e. S ) ) |
9 |
|
difeq1 |
|- ( u = A -> ( u \ v ) = ( A \ v ) ) |
10 |
9
|
eleq1d |
|- ( u = A -> ( ( u \ v ) e. S <-> ( A \ v ) e. S ) ) |
11 |
8 10
|
anbi12d |
|- ( u = A -> ( ( ( u u. v ) e. S /\ ( u \ v ) e. S ) <-> ( ( A u. v ) e. S /\ ( A \ v ) e. S ) ) ) |
12 |
|
uneq2 |
|- ( v = B -> ( A u. v ) = ( A u. B ) ) |
13 |
12
|
eleq1d |
|- ( v = B -> ( ( A u. v ) e. S <-> ( A u. B ) e. S ) ) |
14 |
|
difeq2 |
|- ( v = B -> ( A \ v ) = ( A \ B ) ) |
15 |
14
|
eleq1d |
|- ( v = B -> ( ( A \ v ) e. S <-> ( A \ B ) e. S ) ) |
16 |
13 15
|
anbi12d |
|- ( v = B -> ( ( ( A u. v ) e. S /\ ( A \ v ) e. S ) <-> ( ( A u. B ) e. S /\ ( A \ B ) e. S ) ) ) |
17 |
11 16
|
rspc2va |
|- ( ( ( A e. S /\ B e. S ) /\ A. u e. S A. v e. S ( ( u u. v ) e. S /\ ( u \ v ) e. S ) ) -> ( ( A u. B ) e. S /\ ( A \ B ) e. S ) ) |
18 |
2 3 6 17
|
syl21anc |
|- ( ( S e. Q /\ A e. S /\ B e. S ) -> ( ( A u. B ) e. S /\ ( A \ B ) e. S ) ) |
19 |
18
|
simpld |
|- ( ( S e. Q /\ A e. S /\ B e. S ) -> ( A u. B ) e. S ) |