This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem brsdom

Description: Strict dominance relation, meaning " B is strictly greater in size than A ". Definition of Mendelson p. 255. (Contributed by NM, 25-Jun-1998)

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

Proof

Step	Hyp	Ref	Expression
1		df-sdom	⊢ ≺ = ( ≼ ∖ ≈ )
2	1	eleq2i	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ≺ ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ≼ ∖ ≈ ) )
3		df-br	⊢ ( 𝐴 ≺ 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ≺ )
4		df-br	⊢ ( 𝐴 ≼ 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ≼ )
5		df-br	⊢ ( 𝐴 ≈ 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ≈ )
6	5	notbii	⊢ ( ¬ 𝐴 ≈ 𝐵 ↔ ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ ≈ )
7	4 6	anbi12i	⊢ ( ( 𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≈ 𝐵 ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ≼ ∧ ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ ≈ ) )
8		eldif	⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ≼ ∖ ≈ ) ↔ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ ≼ ∧ ¬ ⟨ 𝐴 , 𝐵 ⟩ ∈ ≈ ) )
9	7 8	bitr4i	⊢ ( ( 𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≈ 𝐵 ) ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( ≼ ∖ ≈ ) )
10	2 3 9	3bitr4i	⊢ ( 𝐴 ≺ 𝐵 ↔ ( 𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≈ 𝐵 ) )