Metamath Proof Explorer


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 ) → ( 𝐴𝐵 ↔ ¬ 𝐵𝐴 ) )