Theorem bren2

Description: Equinumerosity expressed in terms of dominance and strict dominance. (Contributed by NM, 23-Oct-2004)

	Ref	Expression
Assertion	bren2	⊢ ( 𝐴 ≈ 𝐵 ↔ ( 𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≺ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		endom	⊢ ( 𝐴 ≈ 𝐵 → 𝐴 ≼ 𝐵 )
2		sdomnen	⊢ ( 𝐴 ≺ 𝐵 → ¬ 𝐴 ≈ 𝐵 )
3	2	con2i	⊢ ( 𝐴 ≈ 𝐵 → ¬ 𝐴 ≺ 𝐵 )
4	1 3	jca	⊢ ( 𝐴 ≈ 𝐵 → ( 𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≺ 𝐵 ) )
5		brdom2	⊢ ( 𝐴 ≼ 𝐵 ↔ ( 𝐴 ≺ 𝐵 ∨ 𝐴 ≈ 𝐵 ) )
6	5	biimpi	⊢ ( 𝐴 ≼ 𝐵 → ( 𝐴 ≺ 𝐵 ∨ 𝐴 ≈ 𝐵 ) )
7	6	orcanai	⊢ ( ( 𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≺ 𝐵 ) → 𝐴 ≈ 𝐵 )
8	4 7	impbii	⊢ ( 𝐴 ≈ 𝐵 ↔ ( 𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≺ 𝐵 ) )