This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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 )