Theorem brdomg

Description: Dominance relation. (Contributed by NM, 15-Jun-1998)

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

Proof

Step	Hyp	Ref	Expression
1		f1eq2	⊢ ( 𝑥 = 𝐴 → ( 𝑓 : 𝑥 –1-1→ 𝑦 ↔ 𝑓 : 𝐴 –1-1→ 𝑦 ) )
2	1	exbidv	⊢ ( 𝑥 = 𝐴 → ( ∃ 𝑓 𝑓 : 𝑥 –1-1→ 𝑦 ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝑦 ) )
3		f1eq3	⊢ ( 𝑦 = 𝐵 → ( 𝑓 : 𝐴 –1-1→ 𝑦 ↔ 𝑓 : 𝐴 –1-1→ 𝐵 ) )
4	3	exbidv	⊢ ( 𝑦 = 𝐵 → ( ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝑦 ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝐵 ) )
5		df-dom	⊢ ≼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑓 𝑓 : 𝑥 –1-1→ 𝑦 }
6	2 4 5	brabg	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ 𝐶 ) → ( 𝐴 ≼ 𝐵 ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝐵 ) )
7	6	ex	⊢ ( 𝐴 ∈ V → ( 𝐵 ∈ 𝐶 → ( 𝐴 ≼ 𝐵 ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝐵 ) ) )
8		reldom	⊢ Rel ≼
9	8	brrelex1i	⊢ ( 𝐴 ≼ 𝐵 → 𝐴 ∈ V )
10		f1f	⊢ ( 𝑓 : 𝐴 –1-1→ 𝐵 → 𝑓 : 𝐴 ⟶ 𝐵 )
11		fdm	⊢ ( 𝑓 : 𝐴 ⟶ 𝐵 → dom 𝑓 = 𝐴 )
12		vex	⊢ 𝑓 ∈ V
13	12	dmex	⊢ dom 𝑓 ∈ V
14	11 13	eqeltrrdi	⊢ ( 𝑓 : 𝐴 ⟶ 𝐵 → 𝐴 ∈ V )
15	10 14	syl	⊢ ( 𝑓 : 𝐴 –1-1→ 𝐵 → 𝐴 ∈ V )
16	15	exlimiv	⊢ ( ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝐵 → 𝐴 ∈ V )
17	9 16	pm5.21ni	⊢ ( ¬ 𝐴 ∈ V → ( 𝐴 ≼ 𝐵 ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝐵 ) )
18	17	a1d	⊢ ( ¬ 𝐴 ∈ V → ( 𝐵 ∈ 𝐶 → ( 𝐴 ≼ 𝐵 ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝐵 ) ) )
19	7 18	pm2.61i	⊢ ( 𝐵 ∈ 𝐶 → ( 𝐴 ≼ 𝐵 ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝐵 ) )