This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem brdomg

Description: Dominance relation. (Contributed by NM, 15-Jun-1998) Extract brdom2g as an intermediate result. (Revised 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→ 𝐵 ) )