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 𝐴 ∧ Ord 𝐵 ∧ ( 𝐴𝐵 ) ≠ ∅ ) → 𝐵 = ( 𝐴𝐵 ) )

Proof

Step Hyp Ref Expression
1 ssdif0 ( 𝐴𝐵 ↔ ( 𝐴𝐵 ) = ∅ )
2 1 necon3bbii ( ¬ 𝐴𝐵 ↔ ( 𝐴𝐵 ) ≠ ∅ )
3 dfdif2 ( 𝐴𝐵 ) = { 𝑥𝐴 ∣ ¬ 𝑥𝐵 }
4 3 inteqi ( 𝐴𝐵 ) = { 𝑥𝐴 ∣ ¬ 𝑥𝐵 }
5 ordtri1 ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴𝐵 ↔ ¬ 𝐵𝐴 ) )
6 5 con2bid ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐵𝐴 ↔ ¬ 𝐴𝐵 ) )
7 id ( Ord 𝐵 → Ord 𝐵 )
8 ordelord ( ( Ord 𝐴𝑥𝐴 ) → Ord 𝑥 )
9 ordtri1 ( ( Ord 𝐵 ∧ Ord 𝑥 ) → ( 𝐵𝑥 ↔ ¬ 𝑥𝐵 ) )
10 7 8 9 syl2anr ( ( ( Ord 𝐴𝑥𝐴 ) ∧ Ord 𝐵 ) → ( 𝐵𝑥 ↔ ¬ 𝑥𝐵 ) )
11 10 an32s ( ( ( Ord 𝐴 ∧ Ord 𝐵 ) ∧ 𝑥𝐴 ) → ( 𝐵𝑥 ↔ ¬ 𝑥𝐵 ) )
12 11 rabbidva ( ( Ord 𝐴 ∧ Ord 𝐵 ) → { 𝑥𝐴𝐵𝑥 } = { 𝑥𝐴 ∣ ¬ 𝑥𝐵 } )
13 12 inteqd ( ( Ord 𝐴 ∧ Ord 𝐵 ) → { 𝑥𝐴𝐵𝑥 } = { 𝑥𝐴 ∣ ¬ 𝑥𝐵 } )
14 intmin ( 𝐵𝐴 { 𝑥𝐴𝐵𝑥 } = 𝐵 )
15 13 14 sylan9req ( ( ( Ord 𝐴 ∧ Ord 𝐵 ) ∧ 𝐵𝐴 ) → { 𝑥𝐴 ∣ ¬ 𝑥𝐵 } = 𝐵 )
16 15 ex ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐵𝐴 { 𝑥𝐴 ∣ ¬ 𝑥𝐵 } = 𝐵 ) )
17 6 16 sylbird ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( ¬ 𝐴𝐵 { 𝑥𝐴 ∣ ¬ 𝑥𝐵 } = 𝐵 ) )
18 17 3impia ( ( Ord 𝐴 ∧ Ord 𝐵 ∧ ¬ 𝐴𝐵 ) → { 𝑥𝐴 ∣ ¬ 𝑥𝐵 } = 𝐵 )
19 4 18 eqtr2id ( ( Ord 𝐴 ∧ Ord 𝐵 ∧ ¬ 𝐴𝐵 ) → 𝐵 = ( 𝐴𝐵 ) )
20 2 19 syl3an3br ( ( Ord 𝐴 ∧ Ord 𝐵 ∧ ( 𝐴𝐵 ) ≠ ∅ ) → 𝐵 = ( 𝐴𝐵 ) )