Step |
Hyp |
Ref |
Expression |
1 |
|
ssdif0 |
|- ( A C_ B <-> ( A \ B ) = (/) ) |
2 |
1
|
necon3bbii |
|- ( -. A C_ B <-> ( A \ B ) =/= (/) ) |
3 |
|
dfdif2 |
|- ( A \ B ) = { x e. A | -. x e. B } |
4 |
3
|
inteqi |
|- |^| ( A \ B ) = |^| { x e. A | -. x e. B } |
5 |
|
ordtri1 |
|- ( ( Ord A /\ Ord B ) -> ( A C_ B <-> -. B e. A ) ) |
6 |
5
|
con2bid |
|- ( ( Ord A /\ Ord B ) -> ( B e. A <-> -. A C_ B ) ) |
7 |
|
id |
|- ( Ord B -> Ord B ) |
8 |
|
ordelord |
|- ( ( Ord A /\ x e. A ) -> Ord x ) |
9 |
|
ordtri1 |
|- ( ( Ord B /\ Ord x ) -> ( B C_ x <-> -. x e. B ) ) |
10 |
7 8 9
|
syl2anr |
|- ( ( ( Ord A /\ x e. A ) /\ Ord B ) -> ( B C_ x <-> -. x e. B ) ) |
11 |
10
|
an32s |
|- ( ( ( Ord A /\ Ord B ) /\ x e. A ) -> ( B C_ x <-> -. x e. B ) ) |
12 |
11
|
rabbidva |
|- ( ( Ord A /\ Ord B ) -> { x e. A | B C_ x } = { x e. A | -. x e. B } ) |
13 |
12
|
inteqd |
|- ( ( Ord A /\ Ord B ) -> |^| { x e. A | B C_ x } = |^| { x e. A | -. x e. B } ) |
14 |
|
intmin |
|- ( B e. A -> |^| { x e. A | B C_ x } = B ) |
15 |
13 14
|
sylan9req |
|- ( ( ( Ord A /\ Ord B ) /\ B e. A ) -> |^| { x e. A | -. x e. B } = B ) |
16 |
15
|
ex |
|- ( ( Ord A /\ Ord B ) -> ( B e. A -> |^| { x e. A | -. x e. B } = B ) ) |
17 |
6 16
|
sylbird |
|- ( ( Ord A /\ Ord B ) -> ( -. A C_ B -> |^| { x e. A | -. x e. B } = B ) ) |
18 |
17
|
3impia |
|- ( ( Ord A /\ Ord B /\ -. A C_ B ) -> |^| { x e. A | -. x e. B } = B ) |
19 |
4 18
|
eqtr2id |
|- ( ( Ord A /\ Ord B /\ -. A C_ B ) -> B = |^| ( A \ B ) ) |
20 |
2 19
|
syl3an3br |
|- ( ( Ord A /\ Ord B /\ ( A \ B ) =/= (/) ) -> B = |^| ( A \ B ) ) |