wemaplem1

Description: Value of the lexicographic order on a sequence space. (Contributed by Stefan O'Rear, 18-Jan-2015)

		Ref	Expression
	Hypothesis	wemapso.t	$⊢ T = \{⟨x, y⟩ \| \exists z \in A (x (z) S y (z) \land \forall w \in A (w R z \to x (w) = y (w)))\}$
	Assertion	wemaplem1	$⊢ (P \in V \land Q \in W) \to (P T Q \leftrightarrow \exists a \in A (P (a) S Q (a) \land \forall b \in A (b R a \to P (b) = Q (b))))$

Proof

Step	Hyp	Ref	Expression
1		wemapso.t	$⊢ T = \{⟨x, y⟩ \| \exists z \in A (x (z) S y (z) \land \forall w \in A (w R z \to x (w) = y (w)))\}$
2		fveq1	$⊢ x = P \to x (z) = P (z)$
3		fveq1	$⊢ y = Q \to y (z) = Q (z)$
4	2 3	breqan12d	$⊢ (x = P \land y = Q) \to (x (z) S y (z) \leftrightarrow P (z) S Q (z))$
5		fveq1	$⊢ x = P \to x (w) = P (w)$
6		fveq1	$⊢ y = Q \to y (w) = Q (w)$
7	5 6	eqeqan12d	$⊢ (x = P \land y = Q) \to (x (w) = y (w) \leftrightarrow P (w) = Q (w))$
8	7	imbi2d	$⊢ (x = P \land y = Q) \to ((w R z \to x (w) = y (w)) \leftrightarrow (w R z \to P (w) = Q (w)))$
9	8	ralbidv	$⊢ (x = P \land y = Q) \to (\forall w \in A (w R z \to x (w) = y (w)) \leftrightarrow \forall w \in A (w R z \to P (w) = Q (w)))$
10	4 9	anbi12d	$⊢ (x = P \land y = Q) \to ((x (z) S y (z) \land \forall w \in A (w R z \to x (w) = y (w))) \leftrightarrow (P (z) S Q (z) \land \forall w \in A (w R z \to P (w) = Q (w))))$
11	10	rexbidv	$⊢ (x = P \land y = Q) \to (\exists z \in A (x (z) S y (z) \land \forall w \in A (w R z \to x (w) = y (w))) \leftrightarrow \exists z \in A (P (z) S Q (z) \land \forall w \in A (w R z \to P (w) = Q (w))))$
12		fveq2	$⊢ z = a \to P (z) = P (a)$
13		fveq2	$⊢ z = a \to Q (z) = Q (a)$
14	12 13	breq12d	$⊢ z = a \to (P (z) S Q (z) \leftrightarrow P (a) S Q (a))$
15		breq2	$⊢ z = a \to (w R z \leftrightarrow w R a)$
16	15	imbi1d	$⊢ z = a \to ((w R z \to P (w) = Q (w)) \leftrightarrow (w R a \to P (w) = Q (w)))$
17	16	ralbidv	$⊢ z = a \to (\forall w \in A (w R z \to P (w) = Q (w)) \leftrightarrow \forall w \in A (w R a \to P (w) = Q (w)))$
18		breq1	$⊢ w = b \to (w R a \leftrightarrow b R a)$
19		fveq2	$⊢ w = b \to P (w) = P (b)$
20		fveq2	$⊢ w = b \to Q (w) = Q (b)$
21	19 20	eqeq12d	$⊢ w = b \to (P (w) = Q (w) \leftrightarrow P (b) = Q (b))$
22	18 21	imbi12d	$⊢ w = b \to ((w R a \to P (w) = Q (w)) \leftrightarrow (b R a \to P (b) = Q (b)))$
23	22	cbvralvw	$⊢ \forall w \in A (w R a \to P (w) = Q (w)) \leftrightarrow \forall b \in A (b R a \to P (b) = Q (b))$
24	17 23	bitrdi	$⊢ z = a \to (\forall w \in A (w R z \to P (w) = Q (w)) \leftrightarrow \forall b \in A (b R a \to P (b) = Q (b)))$
25	14 24	anbi12d	$⊢ z = a \to ((P (z) S Q (z) \land \forall w \in A (w R z \to P (w) = Q (w))) \leftrightarrow (P (a) S Q (a) \land \forall b \in A (b R a \to P (b) = Q (b))))$
26	25	cbvrexvw	$⊢ \exists z \in A (P (z) S Q (z) \land \forall w \in A (w R z \to P (w) = Q (w))) \leftrightarrow \exists a \in A (P (a) S Q (a) \land \forall b \in A (b R a \to P (b) = Q (b)))$
27	11 26	bitrdi	$⊢ (x = P \land y = Q) \to (\exists z \in A (x (z) S y (z) \land \forall w \in A (w R z \to x (w) = y (w))) \leftrightarrow \exists a \in A (P (a) S Q (a) \land \forall b \in A (b R a \to P (b) = Q (b))))$
28	27 1	brabga	$⊢ (P \in V \land Q \in W) \to (P T Q \leftrightarrow \exists a \in A (P (a) S Q (a) \land \forall b \in A (b R a \to P (b) = Q (b))))$

Metamath Proof Explorer

Theorem wemaplem1

Proof