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 \land Ord B \land A ∖ B \neq \emptyset) \to B = ⋂ (A ∖ B)$

Proof

Step	Hyp	Ref	Expression
1		ssdif0	$⊢ A \subseteq B \leftrightarrow A ∖ B = \emptyset$
2	1	necon3bbii	$⊢ \neg A \subseteq B \leftrightarrow A ∖ B \neq \emptyset$
3		dfdif2	$⊢ A ∖ B = \{x \in A \| \neg x \in B\}$
4	3	inteqi	$⊢ ⋂ (A ∖ B) = ⋂ \{x \in A \| \neg x \in B\}$
5		ordtri1	$⊢ (Ord A \land Ord B) \to (A \subseteq B \leftrightarrow \neg B \in A)$
6	5	con2bid	$⊢ (Ord A \land Ord B) \to (B \in A \leftrightarrow \neg A \subseteq B)$
7		id	$⊢ Ord B \to Ord B$
8		ordelord	$⊢ (Ord A \land x \in A) \to Ord x$
9		ordtri1	$⊢ (Ord B \land Ord x) \to (B \subseteq x \leftrightarrow \neg x \in B)$
10	7 8 9	syl2anr	$⊢ ((Ord A \land x \in A) \land Ord B) \to (B \subseteq x \leftrightarrow \neg x \in B)$
11	10	an32s	$⊢ ((Ord A \land Ord B) \land x \in A) \to (B \subseteq x \leftrightarrow \neg x \in B)$
12	11	rabbidva	$⊢ (Ord A \land Ord B) \to \{x \in A \| B \subseteq x\} = \{x \in A \| \neg x \in B\}$
13	12	inteqd	$⊢ (Ord A \land Ord B) \to ⋂ \{x \in A \| B \subseteq x\} = ⋂ \{x \in A \| \neg x \in B\}$
14		intmin	$⊢ B \in A \to ⋂ \{x \in A \| B \subseteq x\} = B$
15	13 14	sylan9req	$⊢ ((Ord A \land Ord B) \land B \in A) \to ⋂ \{x \in A \| \neg x \in B\} = B$
16	15	ex	$⊢ (Ord A \land Ord B) \to (B \in A \to ⋂ \{x \in A \| \neg x \in B\} = B)$
17	6 16	sylbird	$⊢ (Ord A \land Ord B) \to (\neg A \subseteq B \to ⋂ \{x \in A \| \neg x \in B\} = B)$
18	17	3impia	$⊢ (Ord A \land Ord B \land \neg A \subseteq B) \to ⋂ \{x \in A \| \neg x \in B\} = B$
19	4 18	syl5req	$⊢ (Ord A \land Ord B \land \neg A \subseteq B) \to B = ⋂ (A ∖ B)$
20	2 19	syl3an3br	$⊢ (Ord A \land Ord B \land A ∖ B \neq \emptyset) \to B = ⋂ (A ∖ B)$

Metamath Proof Explorer

Theorem ordintdif

Proof