mapdom3

Description: Set exponentiation dominates the base. (Contributed by Mario Carneiro, 30-Apr-2015) (Proof shortened by AV, 17-Jul-2022)

		Ref	Expression
	Assertion	mapdom3	$⊢ (A \in V \land B \in W \land B \neq \emptyset) \to A ≼ (A^{B})$

Proof

Step	Hyp	Ref	Expression
1		n0	$⊢ B \neq \emptyset \leftrightarrow \exists x x \in B$
2		simp1	$⊢ (A \in V \land B \in W \land x \in B) \to A \in V$
3		simp3	$⊢ (A \in V \land B \in W \land x \in B) \to x \in B$
4	2 3	mapsnend	$⊢ (A \in V \land B \in W \land x \in B) \to (A^{\{x\}}) \approx A$
5	4	ensymd	$⊢ (A \in V \land B \in W \land x \in B) \to A \approx (A^{\{x\}})$
6		simp2	$⊢ (A \in V \land B \in W \land x \in B) \to B \in W$
7	3	snssd	$⊢ (A \in V \land B \in W \land x \in B) \to \{x\} \subseteq B$
8		ssdomg	$⊢ B \in W \to (\{x\} \subseteq B \to \{x\} ≼ B)$
9	6 7 8	sylc	$⊢ (A \in V \land B \in W \land x \in B) \to \{x\} ≼ B$
10		vex	$⊢ x \in V$
11	10	snnz	$⊢ \{x\} \neq \emptyset$
12		simpl	$⊢ (\{x\} = \emptyset \land A = \emptyset) \to \{x\} = \emptyset$
13	12	necon3ai	$⊢ \{x\} \neq \emptyset \to \neg (\{x\} = \emptyset \land A = \emptyset)$
14	11 13	ax-mp	$⊢ \neg (\{x\} = \emptyset \land A = \emptyset)$
15		mapdom2	$⊢ (\{x\} ≼ B \land \neg (\{x\} = \emptyset \land A = \emptyset)) \to (A^{\{x\}}) ≼ (A^{B})$
16	9 14 15	sylancl	$⊢ (A \in V \land B \in W \land x \in B) \to (A^{\{x\}}) ≼ (A^{B})$
17		endomtr	$⊢ (A \approx (A^{\{x\}}) \land (A^{\{x\}}) ≼ (A^{B})) \to A ≼ (A^{B})$
18	5 16 17	syl2anc	$⊢ (A \in V \land B \in W \land x \in B) \to A ≼ (A^{B})$
19	18	3expia	$⊢ (A \in V \land B \in W) \to (x \in B \to A ≼ (A^{B}))$
20	19	exlimdv	$⊢ (A \in V \land B \in W) \to (\exists x x \in B \to A ≼ (A^{B}))$
21	1 20	biimtrid	$⊢ (A \in V \land B \in W) \to (B \neq \emptyset \to A ≼ (A^{B}))$
22	21	3impia	$⊢ (A \in V \land B \in W \land B \neq \emptyset) \to A ≼ (A^{B})$

Metamath Proof Explorer

Theorem mapdom3

Proof