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 ⊢ B ∈ C → A ≼ B ↔ ∃ f f : A ⟶ 1-1 B

Proof

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