wloglei

Description: Form of wlogle where both sides of the equivalence are proven rather than showing that they are equivalent to each other. (Contributed by Mario Carneiro, 9-Mar-2015)

	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 ℝ$
	wloglei.4	$⊢ (φ \land (x \in S \land y \in S \land x \leq y)) \to θ$
	wloglei.5	$⊢ (φ \land (x \in S \land y \in S \land x \leq y)) \to χ$
Assertion	wloglei	$⊢ (φ \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		wloglei.4	$⊢ (φ \land (x \in S \land y \in S \land x \leq y)) \to θ$
5		wloglei.5	$⊢ (φ \land (x \in S \land y \in S \land x \leq y)) \to χ$
6	3	adantr	$⊢ (φ \land (x \in S \land y \in S)) \to S \subseteq ℝ$
7		simprr	$⊢ (φ \land (x \in S \land y \in S)) \to y \in S$
8	6 7	sseldd	$⊢ (φ \land (x \in S \land y \in S)) \to y \in ℝ$
9		simprl	$⊢ (φ \land (x \in S \land y \in S)) \to x \in S$
10	6 9	sseldd	$⊢ (φ \land (x \in S \land y \in S)) \to x \in ℝ$
11		vex	$⊢ x \in V$
12		vex	$⊢ y \in V$
13		eleq1w	$⊢ z = x \to (z \in S \leftrightarrow x \in S)$
14		eleq1w	$⊢ w = y \to (w \in S \leftrightarrow y \in S)$
15	13 14	bi2anan9	$⊢ (z = x \land w = y) \to ((z \in S \land w \in S) \leftrightarrow (x \in S \land y \in S))$
16	15	anbi2d	$⊢ (z = x \land w = y) \to ((φ \land (z \in S \land w \in S)) \leftrightarrow (φ \land (x \in S \land y \in S)))$
17		breq12	$⊢ (w = y \land z = x) \to (w \leq z \leftrightarrow y \leq x)$
18	17	ancoms	$⊢ (z = x \land w = y) \to (w \leq z \leftrightarrow y \leq x)$
19	16 18	anbi12d	$⊢ (z = x \land w = y) \to (((φ \land (z \in S \land w \in S)) \land w \leq z) \leftrightarrow ((φ \land (x \in S \land y \in S)) \land y \leq x))$
20	19 1	imbi12d	$⊢ (z = x \land w = y) \to ((((φ \land (z \in S \land w \in S)) \land w \leq z) \to ψ) \leftrightarrow (((φ \land (x \in S \land y \in S)) \land y \leq x) \to χ))$
21		vex	$⊢ z \in V$
22		vex	$⊢ w \in V$
23		ancom	$⊢ (x \in S \land y \in S) \leftrightarrow (y \in S \land x \in S)$
24		eleq1w	$⊢ y = z \to (y \in S \leftrightarrow z \in S)$
25		eleq1w	$⊢ x = w \to (x \in S \leftrightarrow w \in S)$
26	24 25	bi2anan9	$⊢ (y = z \land x = w) \to ((y \in S \land x \in S) \leftrightarrow (z \in S \land w \in S))$
27	23 26	syl5bb	$⊢ (y = z \land x = w) \to ((x \in S \land y \in S) \leftrightarrow (z \in S \land w \in S))$
28	27	anbi2d	$⊢ (y = z \land x = w) \to ((φ \land (x \in S \land y \in S)) \leftrightarrow (φ \land (z \in S \land w \in S)))$
29		breq12	$⊢ (x = w \land y = z) \to (x \leq y \leftrightarrow w \leq z)$
30	29	ancoms	$⊢ (y = z \land x = w) \to (x \leq y \leftrightarrow w \leq z)$
31	28 30	anbi12d	$⊢ (y = z \land x = w) \to (((φ \land (x \in S \land y \in S)) \land x \leq y) \leftrightarrow ((φ \land (z \in S \land w \in S)) \land w \leq z))$
32		equcom	$⊢ y = z \leftrightarrow z = y$
33		equcom	$⊢ x = w \leftrightarrow w = x$
34	32 33 2	syl2anb	$⊢ (y = z \land x = w) \to (ψ \leftrightarrow θ)$
35	34	bicomd	$⊢ (y = z \land x = w) \to (θ \leftrightarrow ψ)$
36	31 35	imbi12d	$⊢ (y = z \land x = w) \to ((((φ \land (x \in S \land y \in S)) \land x \leq y) \to θ) \leftrightarrow (((φ \land (z \in S \land w \in S)) \land w \leq z) \to ψ))$
37		df-3an	$⊢ (x \in S \land y \in S \land x \leq y) \leftrightarrow ((x \in S \land y \in S) \land x \leq y)$
38	37 4	sylan2br	$⊢ (φ \land ((x \in S \land y \in S) \land x \leq y)) \to θ$
39	38	anassrs	$⊢ ((φ \land (x \in S \land y \in S)) \land x \leq y) \to θ$
40	21 22 36 39	vtocl2	$⊢ ((φ \land (z \in S \land w \in S)) \land w \leq z) \to ψ$
41	11 12 20 40	vtocl2	$⊢ ((φ \land (x \in S \land y \in S)) \land y \leq x) \to χ$
42	37 5	sylan2br	$⊢ (φ \land ((x \in S \land y \in S) \land x \leq y)) \to χ$
43	42	anassrs	$⊢ ((φ \land (x \in S \land y \in S)) \land x \leq y) \to χ$
44	8 10 41 43	lecasei	$⊢ (φ \land (x \in S \land y \in S)) \to χ$

Metamath Proof Explorer

Theorem wloglei

Proof