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	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≼ 𝐵 ) → ¬ 𝐵 ≺ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		brdom2	⊢ ( 𝐴 ≼ 𝐵 ↔ ( 𝐴 ≺ 𝐵 ∨ 𝐴 ≈ 𝐵 ) )
2		sdomnen	⊢ ( 𝐴 ≺ 𝐵 → ¬ 𝐴 ≈ 𝐵 )
3	2	adantl	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≺ 𝐵 ) → ¬ 𝐴 ≈ 𝐵 )
4		sdomdom	⊢ ( 𝐴 ≺ 𝐵 → 𝐴 ≼ 𝐵 )
5		sdomdom	⊢ ( 𝐵 ≺ 𝐴 → 𝐵 ≼ 𝐴 )
6		sbthfi	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ≼ 𝐴 ∧ 𝐴 ≼ 𝐵 ) → 𝐵 ≈ 𝐴 )
7		ensymfib	⊢ ( 𝐴 ∈ Fin → ( 𝐴 ≈ 𝐵 ↔ 𝐵 ≈ 𝐴 ) )
8	7	3ad2ant1	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ≼ 𝐴 ∧ 𝐴 ≼ 𝐵 ) → ( 𝐴 ≈ 𝐵 ↔ 𝐵 ≈ 𝐴 ) )
9	6 8	mpbird	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ≼ 𝐴 ∧ 𝐴 ≼ 𝐵 ) → 𝐴 ≈ 𝐵 )
10	5 9	syl3an2	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ≺ 𝐴 ∧ 𝐴 ≼ 𝐵 ) → 𝐴 ≈ 𝐵 )
11	4 10	syl3an3	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ≺ 𝐴 ∧ 𝐴 ≺ 𝐵 ) → 𝐴 ≈ 𝐵 )
12	11	3com23	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≺ 𝐵 ∧ 𝐵 ≺ 𝐴 ) → 𝐴 ≈ 𝐵 )
13	12	3expa	⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐴 ≺ 𝐵 ) ∧ 𝐵 ≺ 𝐴 ) → 𝐴 ≈ 𝐵 )
14	3 13	mtand	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≺ 𝐵 ) → ¬ 𝐵 ≺ 𝐴 )
15		sdomnen	⊢ ( 𝐵 ≺ 𝐴 → ¬ 𝐵 ≈ 𝐴 )
16	7	biimpa	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵 ) → 𝐵 ≈ 𝐴 )
17	15 16	nsyl3	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≈ 𝐵 ) → ¬ 𝐵 ≺ 𝐴 )
18	14 17	jaodan	⊢ ( ( 𝐴 ∈ Fin ∧ ( 𝐴 ≺ 𝐵 ∨ 𝐴 ≈ 𝐵 ) ) → ¬ 𝐵 ≺ 𝐴 )
19	1 18	sylan2b	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ≼ 𝐵 ) → ¬ 𝐵 ≺ 𝐴 )