Metamath Proof Explorer

Theorem domnsymfi

Description: If a set dominates a finite set, it cannot also be strictly dominated by the finite set. This theorem is proved without using the Axiom of Power Sets (unlike domnsym ). (Contributed by BTernaryTau, 22-Nov-2024)

		Ref	Expression
	Assertion	domnsymfi	$⊢ (A \in Fin \land A ≼ B) \to \neg B ≺ A$

Proof

Step	Hyp	Ref	Expression
1		brdom2	$⊢ A ≼ B \leftrightarrow (A ≺ B \lor A \approx B)$
2		sdomnen	$⊢ A ≺ B \to \neg A \approx B$
3	2	adantl	$⊢ (A \in Fin \land A ≺ B) \to \neg A \approx B$
4		sdomdom	$⊢ A ≺ B \to A ≼ B$
5		sdomdom	$⊢ B ≺ A \to B ≼ A$
6		sbthfi	$⊢ (A \in Fin \land B ≼ A \land A ≼ B) \to B \approx A$
7		ensymfib	$⊢ A \in Fin \to (A \approx B \leftrightarrow B \approx A)$
8	7	3ad2ant1	$⊢ (A \in Fin \land B ≼ A \land A ≼ B) \to (A \approx B \leftrightarrow B \approx A)$
9	6 8	mpbird	$⊢ (A \in Fin \land B ≼ A \land A ≼ B) \to A \approx B$
10	5 9	syl3an2	$⊢ (A \in Fin \land B ≺ A \land A ≼ B) \to A \approx B$
11	4 10	syl3an3	$⊢ (A \in Fin \land B ≺ A \land A ≺ B) \to A \approx B$
12	11	3com23	$⊢ (A \in Fin \land A ≺ B \land B ≺ A) \to A \approx B$
13	12	3expa	$⊢ ((A \in Fin \land A ≺ B) \land B ≺ A) \to A \approx B$
14	3 13	mtand	$⊢ (A \in Fin \land A ≺ B) \to \neg B ≺ A$
15		sdomnen	$⊢ B ≺ A \to \neg B \approx A$
16	7	biimpa	$⊢ (A \in Fin \land A \approx B) \to B \approx A$
17	15 16	nsyl3	$⊢ (A \in Fin \land A \approx B) \to \neg B ≺ A$
18	14 17	jaodan	$⊢ (A \in Fin \land (A ≺ B \lor A \approx B)) \to \neg B ≺ A$
19	1 18	sylan2b	$⊢ (A \in Fin \land A ≼ B) \to \neg B ≺ A$