Metamath Proof Explorer


Theorem ordintdif

Description: If B is smaller than A , then it equals the intersection of the difference. Exercise 11 in TakeutiZaring p. 44. (Contributed by Andrew Salmon, 14-Nov-2011)

Ref Expression
Assertion ordintdif
|- ( ( Ord A /\ Ord B /\ ( A \ B ) =/= (/) ) -> B = |^| ( A \ B ) )

Proof

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 ) )