Theorem wdomnumr

Description: Weak dominance agrees with normal for numerable right sets. (Contributed by Stefan O'Rear, 28-Feb-2015) (Revised by Mario Carneiro, 5-May-2015)

	Ref	Expression
Assertion	wdomnumr	⊢ ( 𝐵 ∈ dom card → ( 𝐴 ≼* 𝐵 ↔ 𝐴 ≼ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		brwdom	⊢ ( 𝐵 ∈ dom card → ( 𝐴 ≼* 𝐵 ↔ ( 𝐴 = ∅ ∨ ∃ 𝑥 𝑥 : 𝐵 –onto→ 𝐴 ) ) )
2		0domg	⊢ ( 𝐵 ∈ dom card → ∅ ≼ 𝐵 )
3		breq1	⊢ ( 𝐴 = ∅ → ( 𝐴 ≼ 𝐵 ↔ ∅ ≼ 𝐵 ) )
4	2 3	syl5ibrcom	⊢ ( 𝐵 ∈ dom card → ( 𝐴 = ∅ → 𝐴 ≼ 𝐵 ) )
5		fodomnum	⊢ ( 𝐵 ∈ dom card → ( 𝑥 : 𝐵 –onto→ 𝐴 → 𝐴 ≼ 𝐵 ) )
6	5	exlimdv	⊢ ( 𝐵 ∈ dom card → ( ∃ 𝑥 𝑥 : 𝐵 –onto→ 𝐴 → 𝐴 ≼ 𝐵 ) )
7	4 6	jaod	⊢ ( 𝐵 ∈ dom card → ( ( 𝐴 = ∅ ∨ ∃ 𝑥 𝑥 : 𝐵 –onto→ 𝐴 ) → 𝐴 ≼ 𝐵 ) )
8	1 7	sylbid	⊢ ( 𝐵 ∈ dom card → ( 𝐴 ≼* 𝐵 → 𝐴 ≼ 𝐵 ) )
9		domwdom	⊢ ( 𝐴 ≼ 𝐵 → 𝐴 ≼* 𝐵 )
10	8 9	impbid1	⊢ ( 𝐵 ∈ dom card → ( 𝐴 ≼* 𝐵 ↔ 𝐴 ≼ 𝐵 ) )