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	⊢ ( 𝑋 ≼ 𝑌 → 𝑋 ≼* 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		neqne	⊢ ( ¬ 𝑋 = ∅ → 𝑋 ≠ ∅ )
2	1	adantl	⊢ ( ( 𝑋 ≼ 𝑌 ∧ ¬ 𝑋 = ∅ ) → 𝑋 ≠ ∅ )
3		reldom	⊢ Rel ≼
4	3	brrelex1i	⊢ ( 𝑋 ≼ 𝑌 → 𝑋 ∈ V )
5		0sdomg	⊢ ( 𝑋 ∈ V → ( ∅ ≺ 𝑋 ↔ 𝑋 ≠ ∅ ) )
6	4 5	syl	⊢ ( 𝑋 ≼ 𝑌 → ( ∅ ≺ 𝑋 ↔ 𝑋 ≠ ∅ ) )
7	6	adantr	⊢ ( ( 𝑋 ≼ 𝑌 ∧ ¬ 𝑋 = ∅ ) → ( ∅ ≺ 𝑋 ↔ 𝑋 ≠ ∅ ) )
8	2 7	mpbird	⊢ ( ( 𝑋 ≼ 𝑌 ∧ ¬ 𝑋 = ∅ ) → ∅ ≺ 𝑋 )
9		simpl	⊢ ( ( 𝑋 ≼ 𝑌 ∧ ¬ 𝑋 = ∅ ) → 𝑋 ≼ 𝑌 )
10		fodomr	⊢ ( ( ∅ ≺ 𝑋 ∧ 𝑋 ≼ 𝑌 ) → ∃ 𝑦 𝑦 : 𝑌 –onto→ 𝑋 )
11	8 9 10	syl2anc	⊢ ( ( 𝑋 ≼ 𝑌 ∧ ¬ 𝑋 = ∅ ) → ∃ 𝑦 𝑦 : 𝑌 –onto→ 𝑋 )
12	11	ex	⊢ ( 𝑋 ≼ 𝑌 → ( ¬ 𝑋 = ∅ → ∃ 𝑦 𝑦 : 𝑌 –onto→ 𝑋 ) )
13	12	orrd	⊢ ( 𝑋 ≼ 𝑌 → ( 𝑋 = ∅ ∨ ∃ 𝑦 𝑦 : 𝑌 –onto→ 𝑋 ) )
14	3	brrelex2i	⊢ ( 𝑋 ≼ 𝑌 → 𝑌 ∈ V )
15		brwdom	⊢ ( 𝑌 ∈ V → ( 𝑋 ≼* 𝑌 ↔ ( 𝑋 = ∅ ∨ ∃ 𝑦 𝑦 : 𝑌 –onto→ 𝑋 ) ) )
16	14 15	syl	⊢ ( 𝑋 ≼ 𝑌 → ( 𝑋 ≼* 𝑌 ↔ ( 𝑋 = ∅ ∨ ∃ 𝑦 𝑦 : 𝑌 –onto→ 𝑋 ) ) )
17	13 16	mpbird	⊢ ( 𝑋 ≼ 𝑌 → 𝑋 ≼* 𝑌 )