Theorem brwdom

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

	Ref	Expression
Assertion	brwdom	⊢ ( 𝑌 ∈ 𝑉 → ( 𝑋 ≼* 𝑌 ↔ ( 𝑋 = ∅ ∨ ∃ 𝑧 𝑧 : 𝑌 –onto→ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elex	⊢ ( 𝑌 ∈ 𝑉 → 𝑌 ∈ V )
2		relwdom	⊢ Rel ≼*
3	2	brrelex1i	⊢ ( 𝑋 ≼* 𝑌 → 𝑋 ∈ V )
4	3	a1i	⊢ ( 𝑌 ∈ V → ( 𝑋 ≼* 𝑌 → 𝑋 ∈ V ) )
5		0ex	⊢ ∅ ∈ V
6		eleq1a	⊢ ( ∅ ∈ V → ( 𝑋 = ∅ → 𝑋 ∈ V ) )
7	5 6	ax-mp	⊢ ( 𝑋 = ∅ → 𝑋 ∈ V )
8		forn	⊢ ( 𝑧 : 𝑌 –onto→ 𝑋 → ran 𝑧 = 𝑋 )
9		vex	⊢ 𝑧 ∈ V
10	9	rnex	⊢ ran 𝑧 ∈ V
11	8 10	eqeltrrdi	⊢ ( 𝑧 : 𝑌 –onto→ 𝑋 → 𝑋 ∈ V )
12	11	exlimiv	⊢ ( ∃ 𝑧 𝑧 : 𝑌 –onto→ 𝑋 → 𝑋 ∈ V )
13	7 12	jaoi	⊢ ( ( 𝑋 = ∅ ∨ ∃ 𝑧 𝑧 : 𝑌 –onto→ 𝑋 ) → 𝑋 ∈ V )
14	13	a1i	⊢ ( 𝑌 ∈ V → ( ( 𝑋 = ∅ ∨ ∃ 𝑧 𝑧 : 𝑌 –onto→ 𝑋 ) → 𝑋 ∈ V ) )
15		eqeq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 = ∅ ↔ 𝑋 = ∅ ) )
16		foeq3	⊢ ( 𝑥 = 𝑋 → ( 𝑧 : 𝑦 –onto→ 𝑥 ↔ 𝑧 : 𝑦 –onto→ 𝑋 ) )
17	16	exbidv	⊢ ( 𝑥 = 𝑋 → ( ∃ 𝑧 𝑧 : 𝑦 –onto→ 𝑥 ↔ ∃ 𝑧 𝑧 : 𝑦 –onto→ 𝑋 ) )
18	15 17	orbi12d	⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 = ∅ ∨ ∃ 𝑧 𝑧 : 𝑦 –onto→ 𝑥 ) ↔ ( 𝑋 = ∅ ∨ ∃ 𝑧 𝑧 : 𝑦 –onto→ 𝑋 ) ) )
19		foeq2	⊢ ( 𝑦 = 𝑌 → ( 𝑧 : 𝑦 –onto→ 𝑋 ↔ 𝑧 : 𝑌 –onto→ 𝑋 ) )
20	19	exbidv	⊢ ( 𝑦 = 𝑌 → ( ∃ 𝑧 𝑧 : 𝑦 –onto→ 𝑋 ↔ ∃ 𝑧 𝑧 : 𝑌 –onto→ 𝑋 ) )
21	20	orbi2d	⊢ ( 𝑦 = 𝑌 → ( ( 𝑋 = ∅ ∨ ∃ 𝑧 𝑧 : 𝑦 –onto→ 𝑋 ) ↔ ( 𝑋 = ∅ ∨ ∃ 𝑧 𝑧 : 𝑌 –onto→ 𝑋 ) ) )
22		df-wdom	⊢ ≼* = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 = ∅ ∨ ∃ 𝑧 𝑧 : 𝑦 –onto→ 𝑥 ) }
23	18 21 22	brabg	⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → ( 𝑋 ≼* 𝑌 ↔ ( 𝑋 = ∅ ∨ ∃ 𝑧 𝑧 : 𝑌 –onto→ 𝑋 ) ) )
24	23	expcom	⊢ ( 𝑌 ∈ V → ( 𝑋 ∈ V → ( 𝑋 ≼* 𝑌 ↔ ( 𝑋 = ∅ ∨ ∃ 𝑧 𝑧 : 𝑌 –onto→ 𝑋 ) ) ) )
25	4 14 24	pm5.21ndd	⊢ ( 𝑌 ∈ V → ( 𝑋 ≼* 𝑌 ↔ ( 𝑋 = ∅ ∨ ∃ 𝑧 𝑧 : 𝑌 –onto→ 𝑋 ) ) )
26	1 25	syl	⊢ ( 𝑌 ∈ 𝑉 → ( 𝑋 ≼* 𝑌 ↔ ( 𝑋 = ∅ ∨ ∃ 𝑧 𝑧 : 𝑌 –onto→ 𝑋 ) ) )