Theorem fidomtri2

Description: Trichotomy of dominance without AC when one set is finite. (Contributed by Stefan O'Rear, 30-Oct-2014) (Revised by Mario Carneiro, 7-May-2015)

	Ref	Expression
Assertion	fidomtri2	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ) → ( 𝐴 ≼ 𝐵 ↔ ¬ 𝐵 ≺ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		domnsym	⊢ ( 𝐴 ≼ 𝐵 → ¬ 𝐵 ≺ 𝐴 )
2		sdomdom	⊢ ( 𝐴 ≺ 𝐵 → 𝐴 ≼ 𝐵 )
3	2	con3i	⊢ ( ¬ 𝐴 ≼ 𝐵 → ¬ 𝐴 ≺ 𝐵 )
4		fidomtri	⊢ ( ( 𝐵 ∈ Fin ∧ 𝐴 ∈ 𝑉 ) → ( 𝐵 ≼ 𝐴 ↔ ¬ 𝐴 ≺ 𝐵 ) )
5	4	ancoms	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ) → ( 𝐵 ≼ 𝐴 ↔ ¬ 𝐴 ≺ 𝐵 ) )
6	3 5	syl5ibr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ) → ( ¬ 𝐴 ≼ 𝐵 → 𝐵 ≼ 𝐴 ) )
7		ensym	⊢ ( 𝐵 ≈ 𝐴 → 𝐴 ≈ 𝐵 )
8		endom	⊢ ( 𝐴 ≈ 𝐵 → 𝐴 ≼ 𝐵 )
9	7 8	syl	⊢ ( 𝐵 ≈ 𝐴 → 𝐴 ≼ 𝐵 )
10	9	con3i	⊢ ( ¬ 𝐴 ≼ 𝐵 → ¬ 𝐵 ≈ 𝐴 )
11	6 10	jca2	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ) → ( ¬ 𝐴 ≼ 𝐵 → ( 𝐵 ≼ 𝐴 ∧ ¬ 𝐵 ≈ 𝐴 ) ) )
12		brsdom	⊢ ( 𝐵 ≺ 𝐴 ↔ ( 𝐵 ≼ 𝐴 ∧ ¬ 𝐵 ≈ 𝐴 ) )
13	11 12	syl6ibr	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ) → ( ¬ 𝐴 ≼ 𝐵 → 𝐵 ≺ 𝐴 ) )
14	13	con1d	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ) → ( ¬ 𝐵 ≺ 𝐴 → 𝐴 ≼ 𝐵 ) )
15	1 14	impbid2	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ Fin ) → ( 𝐴 ≼ 𝐵 ↔ ¬ 𝐵 ≺ 𝐴 ) )