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	⊢ ( 𝑋 ≠ ∅ → ( 𝑋 ≼* 𝑌 ↔ ∃ 𝑧 𝑧 : 𝑌 –onto→ 𝑋 ) )

Proof

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