# Metamath Proof Explorer

## Theorem domwdom

Description: Weak dominance is implied by dominance in the usual sense. (Contributed by Stefan O'Rear, 11-Feb-2015)

Ref Expression
Assertion domwdom ${⊢}{X}\preccurlyeq {Y}\to {X}{\preccurlyeq }^{*}{Y}$

### Proof

Step Hyp Ref Expression
1 neqne ${⊢}¬{X}=\varnothing \to {X}\ne \varnothing$
2 1 adantl ${⊢}\left({X}\preccurlyeq {Y}\wedge ¬{X}=\varnothing \right)\to {X}\ne \varnothing$
3 reldom ${⊢}\mathrm{Rel}\preccurlyeq$
4 3 brrelex1i ${⊢}{X}\preccurlyeq {Y}\to {X}\in \mathrm{V}$
5 0sdomg ${⊢}{X}\in \mathrm{V}\to \left(\varnothing \prec {X}↔{X}\ne \varnothing \right)$
6 4 5 syl ${⊢}{X}\preccurlyeq {Y}\to \left(\varnothing \prec {X}↔{X}\ne \varnothing \right)$
7 6 adantr ${⊢}\left({X}\preccurlyeq {Y}\wedge ¬{X}=\varnothing \right)\to \left(\varnothing \prec {X}↔{X}\ne \varnothing \right)$
8 2 7 mpbird ${⊢}\left({X}\preccurlyeq {Y}\wedge ¬{X}=\varnothing \right)\to \varnothing \prec {X}$
9 simpl ${⊢}\left({X}\preccurlyeq {Y}\wedge ¬{X}=\varnothing \right)\to {X}\preccurlyeq {Y}$
10 fodomr ${⊢}\left(\varnothing \prec {X}\wedge {X}\preccurlyeq {Y}\right)\to \exists {y}\phantom{\rule{.4em}{0ex}}{y}:{Y}\underset{onto}{⟶}{X}$
11 8 9 10 syl2anc ${⊢}\left({X}\preccurlyeq {Y}\wedge ¬{X}=\varnothing \right)\to \exists {y}\phantom{\rule{.4em}{0ex}}{y}:{Y}\underset{onto}{⟶}{X}$
12 11 ex ${⊢}{X}\preccurlyeq {Y}\to \left(¬{X}=\varnothing \to \exists {y}\phantom{\rule{.4em}{0ex}}{y}:{Y}\underset{onto}{⟶}{X}\right)$
13 12 orrd ${⊢}{X}\preccurlyeq {Y}\to \left({X}=\varnothing \vee \exists {y}\phantom{\rule{.4em}{0ex}}{y}:{Y}\underset{onto}{⟶}{X}\right)$
14 3 brrelex2i ${⊢}{X}\preccurlyeq {Y}\to {Y}\in \mathrm{V}$
15 brwdom ${⊢}{Y}\in \mathrm{V}\to \left({X}{\preccurlyeq }^{*}{Y}↔\left({X}=\varnothing \vee \exists {y}\phantom{\rule{.4em}{0ex}}{y}:{Y}\underset{onto}{⟶}{X}\right)\right)$
16 14 15 syl ${⊢}{X}\preccurlyeq {Y}\to \left({X}{\preccurlyeq }^{*}{Y}↔\left({X}=\varnothing \vee \exists {y}\phantom{\rule{.4em}{0ex}}{y}:{Y}\underset{onto}{⟶}{X}\right)\right)$
17 13 16 mpbird ${⊢}{X}\preccurlyeq {Y}\to {X}{\preccurlyeq }^{*}{Y}$