wemapso

Description: Construct lexicographic order on a function space based on a well-ordering of the indices and a total ordering of the values. (Contributed by Stefan O'Rear, 18-Jan-2015) (Revised by Mario Carneiro, 8-Feb-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	wemapso	$⊢ (R We A \land S Or B) \to T Or (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		ssid	$⊢ B^{A} \subseteq B^{A}$
3		weso	$⊢ R We A \to R Or A$
4	3	adantr	$⊢ (R We A \land S Or B) \to R Or A$
5		simpr	$⊢ (R We A \land S Or B) \to S Or B$
6		vex	$⊢ a \in V$
7	6	difexi	$⊢ a ∖ b \in V$
8	7	dmex	$⊢ dom (a ∖ b) \in V$
9	8	a1i	$⊢ ((R We A \land S Or B) \land ((a \in (B^{A}) \land b \in (B^{A})) \land a \neq b)) \to dom (a ∖ b) \in V$
10		wefr	$⊢ R We A \to R Fr A$
11	10	ad2antrr	$⊢ ((R We A \land S Or B) \land ((a \in (B^{A}) \land b \in (B^{A})) \land a \neq b)) \to R Fr A$
12		difss	$⊢ a ∖ b \subseteq a$
13		dmss	$⊢ a ∖ b \subseteq a \to dom (a ∖ b) \subseteq dom a$
14	12 13	ax-mp	$⊢ dom (a ∖ b) \subseteq dom a$
15		simprll	$⊢ ((R We A \land S Or B) \land ((a \in (B^{A}) \land b \in (B^{A})) \land a \neq b)) \to a \in (B^{A})$
16		elmapi	$⊢ a \in (B^{A}) \to a : A ⟶ B$
17	15 16	syl	$⊢ ((R We A \land S Or B) \land ((a \in (B^{A}) \land b \in (B^{A})) \land a \neq b)) \to a : A ⟶ B$
18	14 17	fssdm	$⊢ ((R We A \land S Or B) \land ((a \in (B^{A}) \land b \in (B^{A})) \land a \neq b)) \to dom (a ∖ b) \subseteq A$
19		simprr	$⊢ ((R We A \land S Or B) \land ((a \in (B^{A}) \land b \in (B^{A})) \land a \neq b)) \to a \neq b$
20	17	ffnd	$⊢ ((R We A \land S Or B) \land ((a \in (B^{A}) \land b \in (B^{A})) \land a \neq b)) \to a Fn A$
21		simprlr	$⊢ ((R We A \land S Or B) \land ((a \in (B^{A}) \land b \in (B^{A})) \land a \neq b)) \to b \in (B^{A})$
22		elmapi	$⊢ b \in (B^{A}) \to b : A ⟶ B$
23	21 22	syl	$⊢ ((R We A \land S Or B) \land ((a \in (B^{A}) \land b \in (B^{A})) \land a \neq b)) \to b : A ⟶ B$
24	23	ffnd	$⊢ ((R We A \land S Or B) \land ((a \in (B^{A}) \land b \in (B^{A})) \land a \neq b)) \to b Fn A$
25		fndmdifeq0	$⊢ (a Fn A \land b Fn A) \to (dom (a ∖ b) = \emptyset \leftrightarrow a = b)$
26	20 24 25	syl2anc	$⊢ ((R We A \land S Or B) \land ((a \in (B^{A}) \land b \in (B^{A})) \land a \neq b)) \to (dom (a ∖ b) = \emptyset \leftrightarrow a = b)$
27	26	necon3bid	$⊢ ((R We A \land S Or B) \land ((a \in (B^{A}) \land b \in (B^{A})) \land a \neq b)) \to (dom (a ∖ b) \neq \emptyset \leftrightarrow a \neq b)$
28	19 27	mpbird	$⊢ ((R We A \land S Or B) \land ((a \in (B^{A}) \land b \in (B^{A})) \land a \neq b)) \to dom (a ∖ b) \neq \emptyset$
29		fri	$⊢ ((dom (a ∖ b) \in V \land R Fr A) \land (dom (a ∖ b) \subseteq A \land dom (a ∖ b) \neq \emptyset)) \to \exists c \in dom (a ∖ b) \forall d \in dom (a ∖ b) \neg d R c$
30	9 11 18 28 29	syl22anc	$⊢ ((R We A \land S Or B) \land ((a \in (B^{A}) \land b \in (B^{A})) \land a \neq b)) \to \exists c \in dom (a ∖ b) \forall d \in dom (a ∖ b) \neg d R c$
31	1 2 4 5 30	wemapsolem	$⊢ (R We A \land S Or B) \to T Or (B^{A})$

Metamath Proof Explorer

Theorem wemapso

Proof