Metamath Proof Explorer

Theorem wlogle

Description: If the predicate ch ( x , y ) is symmetric under interchange of x , y , then "without loss of generality" we can assume that x <_ y . (Contributed by Mario Carneiro, 18-Aug-2014) (Revised by Mario Carneiro, 11-Sep-2014)

		Ref	Expression
	Hypotheses	wlogle.1	$⊢ (z = x \land w = y) \to (ψ \leftrightarrow χ)$
		wlogle.2	$⊢ (z = y \land w = x) \to (ψ \leftrightarrow θ)$
		wlogle.3	$⊢ φ \to S \subseteq ℝ$
		wlogle.4	$⊢ (φ \land (x \in S \land y \in S)) \to (χ \leftrightarrow θ)$
		wlogle.5	$⊢ (φ \land (x \in S \land y \in S \land x \leq y)) \to χ$
	Assertion	wlogle	$⊢ (φ \land (x \in S \land y \in S)) \to χ$

Proof

Step	Hyp	Ref	Expression
1		wlogle.1	$⊢ (z = x \land w = y) \to (ψ \leftrightarrow χ)$
2		wlogle.2	$⊢ (z = y \land w = x) \to (ψ \leftrightarrow θ)$
3		wlogle.3	$⊢ φ \to S \subseteq ℝ$
4		wlogle.4	$⊢ (φ \land (x \in S \land y \in S)) \to (χ \leftrightarrow θ)$
5		wlogle.5	$⊢ (φ \land (x \in S \land y \in S \land x \leq y)) \to χ$
6	4	3adantr3	$⊢ (φ \land (x \in S \land y \in S \land x \leq y)) \to (χ \leftrightarrow θ)$
7	5 6	mpbid	$⊢ (φ \land (x \in S \land y \in S \land x \leq y)) \to θ$
8	1 2 3 7 5	wloglei	$⊢ (φ \land (x \in S \land y \in S)) \to χ$