infdif2

Description: Cardinality ordering for an infinite class difference. (Contributed by NM, 24-Mar-2007) (Revised by Mario Carneiro, 29-Apr-2015)

		Ref	Expression
	Assertion	infdif2	$⊢ (A \in dom card \land B \in dom card \land ω ≼ A) \to ((A ∖ B) ≼ B \leftrightarrow A ≼ B)$

Proof

Step	Hyp	Ref	Expression
1		domnsym	$⊢ (A ∖ B) ≼ B \to \neg B ≺ (A ∖ B)$
2		simp3	$⊢ (A \in dom card \land ω ≼ A \land B ≺ A) \to B ≺ A$
3		infdif	$⊢ (A \in dom card \land ω ≼ A \land B ≺ A) \to (A ∖ B) \approx A$
4	3	ensymd	$⊢ (A \in dom card \land ω ≼ A \land B ≺ A) \to A \approx (A ∖ B)$
5		sdomentr	$⊢ (B ≺ A \land A \approx (A ∖ B)) \to B ≺ (A ∖ B)$
6	2 4 5	syl2anc	$⊢ (A \in dom card \land ω ≼ A \land B ≺ A) \to B ≺ (A ∖ B)$
7	1 6	nsyl3	$⊢ (A \in dom card \land ω ≼ A \land B ≺ A) \to \neg (A ∖ B) ≼ B$
8	7	3expia	$⊢ (A \in dom card \land ω ≼ A) \to (B ≺ A \to \neg (A ∖ B) ≼ B)$
9	8	3adant2	$⊢ (A \in dom card \land B \in dom card \land ω ≼ A) \to (B ≺ A \to \neg (A ∖ B) ≼ B)$
10	9	con2d	$⊢ (A \in dom card \land B \in dom card \land ω ≼ A) \to ((A ∖ B) ≼ B \to \neg B ≺ A)$
11		domtri2	$⊢ (A \in dom card \land B \in dom card) \to (A ≼ B \leftrightarrow \neg B ≺ A)$
12	11	3adant3	$⊢ (A \in dom card \land B \in dom card \land ω ≼ A) \to (A ≼ B \leftrightarrow \neg B ≺ A)$
13	10 12	sylibrd	$⊢ (A \in dom card \land B \in dom card \land ω ≼ A) \to ((A ∖ B) ≼ B \to A ≼ B)$
14		simp1	$⊢ (A \in dom card \land B \in dom card \land ω ≼ A) \to A \in dom card$
15		difss	$⊢ A ∖ B \subseteq A$
16		ssdomg	$⊢ A \in dom card \to (A ∖ B \subseteq A \to (A ∖ B) ≼ A)$
17	14 15 16	mpisyl	$⊢ (A \in dom card \land B \in dom card \land ω ≼ A) \to (A ∖ B) ≼ A$
18		domtr	$⊢ ((A ∖ B) ≼ A \land A ≼ B) \to (A ∖ B) ≼ B$
19	18	ex	$⊢ (A ∖ B) ≼ A \to (A ≼ B \to (A ∖ B) ≼ B)$
20	17 19	syl	$⊢ (A \in dom card \land B \in dom card \land ω ≼ A) \to (A ≼ B \to (A ∖ B) ≼ B)$
21	13 20	impbid	$⊢ (A \in dom card \land B \in dom card \land ω ≼ A) \to ((A ∖ B) ≼ B \leftrightarrow A ≼ B)$

Metamath Proof Explorer

Theorem infdif2

Proof