wemappo

Description: Construct lexicographic order on a function space based on a well-ordering of the indices and a total ordering of the values.

Without totality on the values or least differing indices, the best we can prove here is a partial order. (Contributed by Stefan O'Rear, 18-Jan-2015) (Revised by AV, 21-Jul-2024)

		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	wemappo	$⊢ (R Or A \land S Po B) \to T Po (B^{A})$

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		simpllr	$⊢ (((R Or A \land S Po B) \land a \in (B^{A})) \land b \in A) \to S Po B$
3		elmapi	$⊢ a \in (B^{A}) \to a : A ⟶ B$
4	3	adantl	$⊢ ((R Or A \land S Po B) \land a \in (B^{A})) \to a : A ⟶ B$
5	4	ffvelcdmda	$⊢ (((R Or A \land S Po B) \land a \in (B^{A})) \land b \in A) \to a (b) \in B$
6		poirr	$⊢ (S Po B \land a (b) \in B) \to \neg a (b) S a (b)$
7	2 5 6	syl2anc	$⊢ (((R Or A \land S Po B) \land a \in (B^{A})) \land b \in A) \to \neg a (b) S a (b)$
8	7	intnanrd	$⊢ (((R Or A \land S Po B) \land a \in (B^{A})) \land b \in A) \to \neg (a (b) S a (b) \land \forall c \in A (c R b \to a (c) = a (c)))$
9	8	nrexdv	$⊢ ((R Or A \land S Po B) \land a \in (B^{A})) \to \neg \exists b \in A (a (b) S a (b) \land \forall c \in A (c R b \to a (c) = a (c)))$
10	1	wemaplem1	$⊢ (a \in V \land a \in V) \to (a T a \leftrightarrow \exists b \in A (a (b) S a (b) \land \forall c \in A (c R b \to a (c) = a (c))))$
11	10	el2v	$⊢ a T a \leftrightarrow \exists b \in A (a (b) S a (b) \land \forall c \in A (c R b \to a (c) = a (c)))$
12	9 11	sylnibr	$⊢ ((R Or A \land S Po B) \land a \in (B^{A})) \to \neg a T a$
13		simplr1	$⊢ (((R Or A \land S Po B) \land (a \in (B^{A}) \land b \in (B^{A}) \land c \in (B^{A}))) \land (a T b \land b T c)) \to a \in (B^{A})$
14		simplr2	$⊢ (((R Or A \land S Po B) \land (a \in (B^{A}) \land b \in (B^{A}) \land c \in (B^{A}))) \land (a T b \land b T c)) \to b \in (B^{A})$
15		simplr3	$⊢ (((R Or A \land S Po B) \land (a \in (B^{A}) \land b \in (B^{A}) \land c \in (B^{A}))) \land (a T b \land b T c)) \to c \in (B^{A})$
16		simplll	$⊢ (((R Or A \land S Po B) \land (a \in (B^{A}) \land b \in (B^{A}) \land c \in (B^{A}))) \land (a T b \land b T c)) \to R Or A$
17		simpllr	$⊢ (((R Or A \land S Po B) \land (a \in (B^{A}) \land b \in (B^{A}) \land c \in (B^{A}))) \land (a T b \land b T c)) \to S Po B$
18		simprl	$⊢ (((R Or A \land S Po B) \land (a \in (B^{A}) \land b \in (B^{A}) \land c \in (B^{A}))) \land (a T b \land b T c)) \to a T b$
19		simprr	$⊢ (((R Or A \land S Po B) \land (a \in (B^{A}) \land b \in (B^{A}) \land c \in (B^{A}))) \land (a T b \land b T c)) \to b T c$
20	1 13 14 15 16 17 18 19	wemaplem3	$⊢ (((R Or A \land S Po B) \land (a \in (B^{A}) \land b \in (B^{A}) \land c \in (B^{A}))) \land (a T b \land b T c)) \to a T c$
21	20	ex	$⊢ ((R Or A \land S Po B) \land (a \in (B^{A}) \land b \in (B^{A}) \land c \in (B^{A}))) \to ((a T b \land b T c) \to a T c)$
22	12 21	ispod	$⊢ (R Or A \land S Po B) \to T Po (B^{A})$

Metamath Proof Explorer

Theorem wemappo

Proof