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 syl5req 
 |-  ( ( Ord A /\ Ord B /\ -. A C_ B ) -> B = |^| ( A \ B ) )
20 2 19 syl3an3br 
 |-  ( ( Ord A /\ Ord B /\ ( A \ B ) =/= (/) ) -> B = |^| ( A \ B ) )