Theorem fidomtri

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

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

Proof

Step	Hyp	Ref	Expression
1		domnsym	⊢ ( 𝐴 ≼ 𝐵 → ¬ 𝐵 ≺ 𝐴 )
2		finnum	⊢ ( 𝐴 ∈ Fin → 𝐴 ∈ dom card )
3	2	adantr	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ) → 𝐴 ∈ dom card )
4		finnum	⊢ ( 𝐵 ∈ Fin → 𝐵 ∈ dom card )
5		domtri2	⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( 𝐴 ≼ 𝐵 ↔ ¬ 𝐵 ≺ 𝐴 ) )
6	3 4 5	syl2an	⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐵 ∈ Fin ) → ( 𝐴 ≼ 𝐵 ↔ ¬ 𝐵 ≺ 𝐴 ) )
7	6	biimprd	⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ) ∧ 𝐵 ∈ Fin ) → ( ¬ 𝐵 ≺ 𝐴 → 𝐴 ≼ 𝐵 ) )
8		isinffi	⊢ ( ( ¬ 𝐵 ∈ Fin ∧ 𝐴 ∈ Fin ) → ∃ 𝑎 𝑎 : 𝐴 –1-1→ 𝐵 )
9	8	ancoms	⊢ ( ( 𝐴 ∈ Fin ∧ ¬ 𝐵 ∈ Fin ) → ∃ 𝑎 𝑎 : 𝐴 –1-1→ 𝐵 )
10	9	adantlr	⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ) ∧ ¬ 𝐵 ∈ Fin ) → ∃ 𝑎 𝑎 : 𝐴 –1-1→ 𝐵 )
11		brdomg	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 ≼ 𝐵 ↔ ∃ 𝑎 𝑎 : 𝐴 –1-1→ 𝐵 ) )
12	11	ad2antlr	⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ) ∧ ¬ 𝐵 ∈ Fin ) → ( 𝐴 ≼ 𝐵 ↔ ∃ 𝑎 𝑎 : 𝐴 –1-1→ 𝐵 ) )
13	10 12	mpbird	⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ) ∧ ¬ 𝐵 ∈ Fin ) → 𝐴 ≼ 𝐵 )
14	13	a1d	⊢ ( ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ) ∧ ¬ 𝐵 ∈ Fin ) → ( ¬ 𝐵 ≺ 𝐴 → 𝐴 ≼ 𝐵 ) )
15	7 14	pm2.61dan	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ) → ( ¬ 𝐵 ≺ 𝐴 → 𝐴 ≼ 𝐵 ) )
16	1 15	impbid2	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 ≼ 𝐵 ↔ ¬ 𝐵 ≺ 𝐴 ) )