Theorem brdomg

Description: Dominance relation. (Contributed by NM, 15-Jun-1998) (Proof shortened by BTernaryTau, 29-Nov-2024)

	Ref	Expression
Assertion	brdomg	⊢ ( 𝐵 ∈ 𝐶 → ( 𝐴 ≼ 𝐵 ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		brdom2g	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ 𝐶 ) → ( 𝐴 ≼ 𝐵 ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝐵 ) )
2	1	ex	⊢ ( 𝐴 ∈ V → ( 𝐵 ∈ 𝐶 → ( 𝐴 ≼ 𝐵 ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝐵 ) ) )
3		reldom	⊢ Rel ≼
4	3	brrelex1i	⊢ ( 𝐴 ≼ 𝐵 → 𝐴 ∈ V )
5		f1f	⊢ ( 𝑓 : 𝐴 –1-1→ 𝐵 → 𝑓 : 𝐴 ⟶ 𝐵 )
6		fdm	⊢ ( 𝑓 : 𝐴 ⟶ 𝐵 → dom 𝑓 = 𝐴 )
7		vex	⊢ 𝑓 ∈ V
8	7	dmex	⊢ dom 𝑓 ∈ V
9	6 8	eqeltrrdi	⊢ ( 𝑓 : 𝐴 ⟶ 𝐵 → 𝐴 ∈ V )
10	5 9	syl	⊢ ( 𝑓 : 𝐴 –1-1→ 𝐵 → 𝐴 ∈ V )
11	10	exlimiv	⊢ ( ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝐵 → 𝐴 ∈ V )
12	4 11	pm5.21ni	⊢ ( ¬ 𝐴 ∈ V → ( 𝐴 ≼ 𝐵 ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝐵 ) )
13	12	a1d	⊢ ( ¬ 𝐴 ∈ V → ( 𝐵 ∈ 𝐶 → ( 𝐴 ≼ 𝐵 ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝐵 ) ) )
14	2 13	pm2.61i	⊢ ( 𝐵 ∈ 𝐶 → ( 𝐴 ≼ 𝐵 ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝐵 ) )