Theorem brsdom2

Description: Alternate definition of strict dominance. Definition 3 of Suppes p. 97. (Contributed by NM, 27-Jul-2004)

	Ref	Expression
Hypotheses	brsdom2.1	⊢ 𝐴 ∈ V
	brsdom2.2	⊢ 𝐵 ∈ V
Assertion	brsdom2	⊢ ( 𝐴 ≺ 𝐵 ↔ ( 𝐴 ≼ 𝐵 ∧ ¬ 𝐵 ≼ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		brsdom2.1	⊢ 𝐴 ∈ V
2		brsdom2.2	⊢ 𝐵 ∈ V
3		dfsdom2	⊢ ≺ = ( ≼ ∖ ◡ ≼ )
4	3	eleq2i	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ≺ ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ≼ ∖ ◡ ≼ ) )
5		df-br	⊢ ( 𝐴 ≺ 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ≺ )
6		df-br	⊢ ( 𝐴 ≼ 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ≼ )
7		df-br	⊢ ( 𝐵 ≼ 𝐴 ↔ ⟨ 𝐵 , 𝐴 ⟩ ∈ ≼ )
8	1 2	opelcnv	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ◡ ≼ ↔ ⟨ 𝐵 , 𝐴 ⟩ ∈ ≼ )
9	7 8	bitr4i	⊢ ( 𝐵 ≼ 𝐴 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ◡ ≼ )
10	9	notbii	⊢ ( ¬ 𝐵 ≼ 𝐴 ↔ ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ ◡ ≼ )
11	6 10	anbi12i	⊢ ( ( 𝐴 ≼ 𝐵 ∧ ¬ 𝐵 ≼ 𝐴 ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ≼ ∧ ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ ◡ ≼ ) )
12		eldif	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ≼ ∖ ◡ ≼ ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ≼ ∧ ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ ◡ ≼ ) )
13	11 12	bitr4i	⊢ ( ( 𝐴 ≼ 𝐵 ∧ ¬ 𝐵 ≼ 𝐴 ) ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ≼ ∖ ◡ ≼ ) )
14	4 5 13	3bitr4i	⊢ ( 𝐴 ≺ 𝐵 ↔ ( 𝐴 ≼ 𝐵 ∧ ¬ 𝐵 ≼ 𝐴 ) )