Metamath Proof Explorer

Theorem brwdom

Description: Property of weak dominance (definitional form). (Contributed by Stefan O'Rear, 11-Feb-2015)

Ref Expression
Assertion brwdom ⊢ Y ∈ V → X ≼ * Y ↔ X = ∅ ∨ ∃ z z : Y ⟶ onto X

Proof

Step Hyp Ref Expression
1 elex ⊢ Y ∈ V → Y ∈ V
2 relwdom ⊢ Rel ⁡ ≼ *
3 2 brrelex1i ⊢ X ≼ * Y → X ∈ V
4 3 a1i ⊢ Y ∈ V → X ≼ * Y → X ∈ V
5 0ex ⊢ ∅ ∈ V
6 eleq1a ⊢ ∅ ∈ V → X = ∅ → X ∈ V
7 5 6 ax-mp ⊢ X = ∅ → X ∈ V
8 forn ⊢ z : Y ⟶ onto X → ran ⁡ z = X
9 vex ⊢ z ∈ V
10 9 rnex ⊢ ran ⁡ z ∈ V
11 8 10 eqeltrrdi ⊢ z : Y ⟶ onto X → X ∈ V
12 11 exlimiv ⊢ ∃ z z : Y ⟶ onto X → X ∈ V
13 7 12 jaoi ⊢ X = ∅ ∨ ∃ z z : Y ⟶ onto X → X ∈ V
14 13 a1i ⊢ Y ∈ V → X = ∅ ∨ ∃ z z : Y ⟶ onto X → X ∈ V
15 eqeq1 ⊢ x = X → x = ∅ ↔ X = ∅
16 foeq3 ⊢ x = X → z : y ⟶ onto x ↔ z : y ⟶ onto X
17 16 exbidv ⊢ x = X → ∃ z z : y ⟶ onto x ↔ ∃ z z : y ⟶ onto X
18 15 17 orbi12d ⊢ x = X → x = ∅ ∨ ∃ z z : y ⟶ onto x ↔ X = ∅ ∨ ∃ z z : y ⟶ onto X
19 foeq2 ⊢ y = Y → z : y ⟶ onto X ↔ z : Y ⟶ onto X
20 19 exbidv ⊢ y = Y → ∃ z z : y ⟶ onto X ↔ ∃ z z : Y ⟶ onto X
21 20 orbi2d ⊢ y = Y → X = ∅ ∨ ∃ z z : y ⟶ onto X ↔ X = ∅ ∨ ∃ z z : Y ⟶ onto X
22 df-wdom ⊢ ≼ * = x y | x = ∅ ∨ ∃ z z : y ⟶ onto x
23 18 21 22 brabg ⊢ X ∈ V ∧ Y ∈ V → X ≼ * Y ↔ X = ∅ ∨ ∃ z z : Y ⟶ onto X
24 23 expcom ⊢ Y ∈ V → X ∈ V → X ≼ * Y ↔ X = ∅ ∨ ∃ z z : Y ⟶ onto X
25 4 14 24 pm5.21ndd ⊢ Y ∈ V → X ≼ * Y ↔ X = ∅ ∨ ∃ z z : Y ⟶ onto X
26 1 25 syl ⊢ Y ∈ V → X ≼ * Y ↔ X = ∅ ∨ ∃ z z : Y ⟶ onto X