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 e. Fin /\ A ~<_ B ) -> -. B ~< A )

Proof

Step	Hyp	Ref	Expression
1		brdom2	|- ( A ~<_ B <-> ( A ~< B \/ A ~~ B ) )
2		sdomnen	|- ( A ~< B -> -. A ~~ B )
3	2	adantl	|- ( ( A e. Fin /\ A ~< B ) -> -. A ~~ B )
4		sdomdom	|- ( A ~< B -> A ~<_ B )
5		sdomdom	|- ( B ~< A -> B ~<_ A )
6		sbthfi	|- ( ( A e. Fin /\ B ~<_ A /\ A ~<_ B ) -> B ~~ A )
7		ensymfib	|- ( A e. Fin -> ( A ~~ B <-> B ~~ A ) )
8	7	3ad2ant1	|- ( ( A e. Fin /\ B ~<_ A /\ A ~<_ B ) -> ( A ~~ B <-> B ~~ A ) )
9	6 8	mpbird	|- ( ( A e. Fin /\ B ~<_ A /\ A ~<_ B ) -> A ~~ B )
10	5 9	syl3an2	|- ( ( A e. Fin /\ B ~< A /\ A ~<_ B ) -> A ~~ B )
11	4 10	syl3an3	|- ( ( A e. Fin /\ B ~< A /\ A ~< B ) -> A ~~ B )
12	11	3com23	|- ( ( A e. Fin /\ A ~< B /\ B ~< A ) -> A ~~ B )
13	12	3expa	|- ( ( ( A e. Fin /\ A ~< B ) /\ B ~< A ) -> A ~~ B )
14	3 13	mtand	|- ( ( A e. Fin /\ A ~< B ) -> -. B ~< A )
15		sdomnen	|- ( B ~< A -> -. B ~~ A )
16	7	biimpa	|- ( ( A e. Fin /\ A ~~ B ) -> B ~~ A )
17	15 16	nsyl3	|- ( ( A e. Fin /\ A ~~ B ) -> -. B ~< A )
18	14 17	jaodan	|- ( ( A e. Fin /\ ( A ~< B \/ A ~~ B ) ) -> -. B ~< A )
19	1 18	sylan2b	|- ( ( A e. Fin /\ A ~<_ B ) -> -. B ~< A )