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	syl5req	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ∧ ¬ 𝐴 ⊆ 𝐵 ) → 𝐵 = ∩ ( 𝐴 ∖ 𝐵 ) )
20	2 19	syl3an3br	⊢ ( ( Ord 𝐴 ∧ Ord 𝐵 ∧ ( 𝐴 ∖ 𝐵 ) ≠ ∅ ) → 𝐵 = ∩ ( 𝐴 ∖ 𝐵 ) )