Theorem domsdomtrfi

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

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

Proof

Step	Hyp	Ref	Expression
1		sdomdom	|- ( B ~< C -> B ~<_ C )
2		domtrfil	|- ( ( A e. Fin /\ A ~<_ B /\ B ~<_ C ) -> A ~<_ C )
3	1 2	syl3an3	|- ( ( A e. Fin /\ A ~<_ B /\ B ~< C ) -> A ~<_ C )
4		ensymfib	|- ( A e. Fin -> ( A ~~ C <-> C ~~ A ) )
5	4	biimpa	|- ( ( A e. Fin /\ A ~~ C ) -> C ~~ A )
6	5	3adant3	|- ( ( A e. Fin /\ A ~~ C /\ A ~<_ B ) -> C ~~ A )
7		enfii	|- ( ( A e. Fin /\ C ~~ A ) -> C e. Fin )
8	7	3adant3	|- ( ( A e. Fin /\ C ~~ A /\ A ~<_ B ) -> C e. Fin )
9		endom	|- ( C ~~ A -> C ~<_ A )
10		domtrfi	|- ( ( A e. Fin /\ C ~<_ A /\ A ~<_ B ) -> C ~<_ B )
11	9 10	syl3an2	|- ( ( A e. Fin /\ C ~~ A /\ A ~<_ B ) -> C ~<_ B )
12	8 11	jca	|- ( ( A e. Fin /\ C ~~ A /\ A ~<_ B ) -> ( C e. Fin /\ C ~<_ B ) )
13	6 12	syld3an2	|- ( ( A e. Fin /\ A ~~ C /\ A ~<_ B ) -> ( C e. Fin /\ C ~<_ B ) )
14		domnsymfi	|- ( ( C e. Fin /\ C ~<_ B ) -> -. B ~< C )
15	13 14	syl	|- ( ( A e. Fin /\ A ~~ C /\ A ~<_ B ) -> -. B ~< C )
16	15	3com23	|- ( ( A e. Fin /\ A ~<_ B /\ A ~~ C ) -> -. B ~< C )
17	16	3expia	|- ( ( A e. Fin /\ A ~<_ B ) -> ( A ~~ C -> -. B ~< C ) )
18	17	con2d	|- ( ( A e. Fin /\ A ~<_ B ) -> ( B ~< C -> -. A ~~ C ) )
19	18	3impia	|- ( ( 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 )