Theorem sdomdomtrfi

Description: Transitivity of strict dominance and dominance when A is finite, proved without using the Axiom of Power Sets (unlike sdomdomtr ). (Contributed by BTernaryTau, 25-Nov-2024)

	Ref	Expression
Assertion	sdomdomtrfi	|- ( ( A e. Fin /\ A ~< B /\ B ~<_ C ) -> A ~< C )

Proof

Step	Hyp	Ref	Expression
1		sdomdom	|- ( A ~< B -> A ~<_ B )
2		domtrfil	|- ( ( A e. Fin /\ A ~<_ B /\ B ~<_ C ) -> A ~<_ C )
3	1 2	syl3an2	|- ( ( A e. Fin /\ A ~< B /\ B ~<_ C ) -> A ~<_ C )
4		simp1	|- ( ( A e. Fin /\ B ~<_ C /\ A ~~ C ) -> A e. Fin )
5		ensymfib	|- ( A e. Fin -> ( A ~~ C <-> C ~~ A ) )
6	5	biimpa	|- ( ( A e. Fin /\ A ~~ C ) -> C ~~ A )
7	6	3adant2	|- ( ( A e. Fin /\ B ~<_ C /\ A ~~ C ) -> C ~~ A )
8		endom	|- ( C ~~ A -> C ~<_ A )
9		domtrfir	|- ( ( A e. Fin /\ B ~<_ C /\ C ~<_ A ) -> B ~<_ A )
10	8 9	syl3an3	|- ( ( A e. Fin /\ B ~<_ C /\ C ~~ A ) -> B ~<_ A )
11	7 10	syld3an3	|- ( ( A e. Fin /\ B ~<_ C /\ A ~~ C ) -> B ~<_ A )
12		domfi	|- ( ( A e. Fin /\ B ~<_ A ) -> B e. Fin )
13		domnsymfi	|- ( ( B e. Fin /\ B ~<_ A ) -> -. A ~< B )
14	12 13	sylancom	|- ( ( A e. Fin /\ B ~<_ A ) -> -. A ~< B )
15	4 11 14	syl2anc	|- ( ( A e. Fin /\ B ~<_ C /\ A ~~ C ) -> -. A ~< B )
16	15	3expia	|- ( ( A e. Fin /\ B ~<_ C ) -> ( A ~~ C -> -. A ~< B ) )
17	16	con2d	|- ( ( A e. Fin /\ B ~<_ C ) -> ( A ~< B -> -. A ~~ C ) )
18	17	3impia	|- ( ( A e. Fin /\ B ~<_ C /\ A ~< B ) -> -. A ~~ C )
19	18	3com23	|- ( ( A e. Fin /\ A ~< B /\ B ~<_ C ) -> -. A ~~ C )
20		brsdom	|- ( A ~< C <-> ( A ~<_ C /\ -. A ~~ C ) )
21	3 19 20	sylanbrc	|- ( ( A e. Fin /\ A ~< B /\ B ~<_ C ) -> A ~< C )