This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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