Metamath Proof Explorer

Theorem brwdomn0

Description: Weak dominance over nonempty sets. (Contributed by Stefan O'Rear, 11-Feb-2015) (Revised by Mario Carneiro, 5-May-2015)

Ref Expression
Assertion brwdomn0 ⊢ X ≠ ∅ → X ≼ * Y ↔ ∃ z z : Y ⟶ onto X

Proof

Step Hyp Ref Expression
1 relwdom ⊢ Rel ⁡ ≼ *
2 1 brrelex2i ⊢ X ≼ * Y → Y ∈ V
3 2 a1i ⊢ X ≠ ∅ → X ≼ * Y → Y ∈ V
4 fof ⊢ z : Y ⟶ onto X → z : Y ⟶ X
5 4 fdmd ⊢ z : Y ⟶ onto X → dom ⁡ z = Y
6 vex ⊢ z ∈ V
7 6 dmex ⊢ dom ⁡ z ∈ V
8 5 7 eqeltrrdi ⊢ z : Y ⟶ onto X → Y ∈ V
9 8 exlimiv ⊢ ∃ z z : Y ⟶ onto X → Y ∈ V
10 9 a1i ⊢ X ≠ ∅ → ∃ z z : Y ⟶ onto X → Y ∈ V
11 brwdom ⊢ Y ∈ V → X ≼ * Y ↔ X = ∅ ∨ ∃ z z : Y ⟶ onto X
12 df-ne ⊢ X ≠ ∅ ↔ ¬ X = ∅
13 biorf ⊢ ¬ X = ∅ → ∃ z z : Y ⟶ onto X ↔ X = ∅ ∨ ∃ z z : Y ⟶ onto X
14 12 13 sylbi ⊢ X ≠ ∅ → ∃ z z : Y ⟶ onto X ↔ X = ∅ ∨ ∃ z z : Y ⟶ onto X
15 14 bicomd ⊢ X ≠ ∅ → X = ∅ ∨ ∃ z z : Y ⟶ onto X ↔ ∃ z z : Y ⟶ onto X
16 11 15 sylan9bbr ⊢ X ≠ ∅ ∧ Y ∈ V → X ≼ * Y ↔ ∃ z z : Y ⟶ onto X
17 16 ex ⊢ X ≠ ∅ → Y ∈ V → X ≼ * Y ↔ ∃ z z : Y ⟶ onto X
18 3 10 17 pm5.21ndd ⊢ X ≠ ∅ → X ≼ * Y ↔ ∃ z z : Y ⟶ onto X