Theorem wdomac

Description: When assuming AC, weak and usual dominance coincide. It is not known if this is an AC equivalent. (Contributed by Stefan O'Rear, 11-Feb-2015) (Revised by Mario Carneiro, 5-May-2015)

	Ref	Expression
Assertion	wdomac	⊢ ( 𝑋 ≼* 𝑌 ↔ 𝑋 ≼ 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		relwdom	⊢ Rel ≼*
2	1	brrelex2i	⊢ ( 𝑋 ≼* 𝑌 → 𝑌 ∈ V )
3		reldom	⊢ Rel ≼
4	3	brrelex2i	⊢ ( 𝑋 ≼ 𝑌 → 𝑌 ∈ V )
5		numth3	⊢ ( 𝑌 ∈ V → 𝑌 ∈ dom card )
6		wdomnumr	⊢ ( 𝑌 ∈ dom card → ( 𝑋 ≼* 𝑌 ↔ 𝑋 ≼ 𝑌 ) )
7	5 6	syl	⊢ ( 𝑌 ∈ V → ( 𝑋 ≼* 𝑌 ↔ 𝑋 ≼ 𝑌 ) )
8	2 4 7	pm5.21nii	⊢ ( 𝑋 ≼* 𝑌 ↔ 𝑋 ≼ 𝑌 )