mapdom2

Description: Order-preserving property of set exponentiation. Theorem 6L(d) of Enderton p. 149. (Contributed by NM, 23-Sep-2004) (Revised by Mario Carneiro, 30-Apr-2015)

		Ref	Expression
	Assertion	mapdom2	$⊢ (A ≼ B \land \neg (A = \emptyset \land C = \emptyset)) \to (C^{A}) ≼ (C^{B})$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ (((A ≼ B \land C \in V) \land \neg (A = \emptyset \land C = \emptyset)) \land C = \emptyset) \to C = \emptyset$
2	1	oveq1d	$⊢ (((A ≼ B \land C \in V) \land \neg (A = \emptyset \land C = \emptyset)) \land C = \emptyset) \to C^{A} = \emptyset^{A}$
3		simplr	$⊢ (((A ≼ B \land C \in V) \land \neg (A = \emptyset \land C = \emptyset)) \land C = \emptyset) \to \neg (A = \emptyset \land C = \emptyset)$
4		idd	$⊢ (((A ≼ B \land C \in V) \land \neg (A = \emptyset \land C = \emptyset)) \land C = \emptyset) \to (A = \emptyset \to A = \emptyset)$
5	4 1	jctird	$⊢ (((A ≼ B \land C \in V) \land \neg (A = \emptyset \land C = \emptyset)) \land C = \emptyset) \to (A = \emptyset \to (A = \emptyset \land C = \emptyset))$
6	3 5	mtod	$⊢ (((A ≼ B \land C \in V) \land \neg (A = \emptyset \land C = \emptyset)) \land C = \emptyset) \to \neg A = \emptyset$
7	6	neqned	$⊢ (((A ≼ B \land C \in V) \land \neg (A = \emptyset \land C = \emptyset)) \land C = \emptyset) \to A \neq \emptyset$
8		map0b	$⊢ A \neq \emptyset \to \emptyset^{A} = \emptyset$
9	7 8	syl	$⊢ (((A ≼ B \land C \in V) \land \neg (A = \emptyset \land C = \emptyset)) \land C = \emptyset) \to \emptyset^{A} = \emptyset$
10	2 9	eqtrd	$⊢ (((A ≼ B \land C \in V) \land \neg (A = \emptyset \land C = \emptyset)) \land C = \emptyset) \to C^{A} = \emptyset$
11		ovex	$⊢ C^{B} \in V$
12	11	0dom	$⊢ \emptyset ≼ (C^{B})$
13	10 12	eqbrtrdi	$⊢ (((A ≼ B \land C \in V) \land \neg (A = \emptyset \land C = \emptyset)) \land C = \emptyset) \to (C^{A}) ≼ (C^{B})$
14		simpll	$⊢ ((A ≼ B \land C \in V) \land C \neq \emptyset) \to A ≼ B$
15		reldom	$⊢ Rel ≼$
16	15	brrelex2i	$⊢ A ≼ B \to B \in V$
17	16	ad2antrr	$⊢ ((A ≼ B \land C \in V) \land C \neq \emptyset) \to B \in V$
18		domeng	$⊢ B \in V \to (A ≼ B \leftrightarrow \exists x (A \approx x \land x \subseteq B))$
19	17 18	syl	$⊢ ((A ≼ B \land C \in V) \land C \neq \emptyset) \to (A ≼ B \leftrightarrow \exists x (A \approx x \land x \subseteq B))$
20	14 19	mpbid	$⊢ ((A ≼ B \land C \in V) \land C \neq \emptyset) \to \exists x (A \approx x \land x \subseteq B)$
21		enrefg	$⊢ C \in V \to C \approx C$
22	21	ad2antlr	$⊢ ((A ≼ B \land C \in V) \land (C \neq \emptyset \land (A \approx x \land x \subseteq B))) \to C \approx C$
23		simprrl	$⊢ ((A ≼ B \land C \in V) \land (C \neq \emptyset \land (A \approx x \land x \subseteq B))) \to A \approx x$
24		mapen	$⊢ (C \approx C \land A \approx x) \to (C^{A}) \approx (C^{x})$
25	22 23 24	syl2anc	$⊢ ((A ≼ B \land C \in V) \land (C \neq \emptyset \land (A \approx x \land x \subseteq B))) \to (C^{A}) \approx (C^{x})$
26		ovexd	$⊢ ((A ≼ B \land C \in V) \land (C \neq \emptyset \land (A \approx x \land x \subseteq B))) \to C^{x} \in V$
27		ovexd	$⊢ ((A ≼ B \land C \in V) \land (C \neq \emptyset \land (A \approx x \land x \subseteq B))) \to C^{(B ∖ x)} \in V$
28		simprl	$⊢ ((A ≼ B \land C \in V) \land (C \neq \emptyset \land (A \approx x \land x \subseteq B))) \to C \neq \emptyset$
29		simplr	$⊢ ((A ≼ B \land C \in V) \land (C \neq \emptyset \land (A \approx x \land x \subseteq B))) \to C \in V$
30	16	ad2antrr	$⊢ ((A ≼ B \land C \in V) \land (C \neq \emptyset \land (A \approx x \land x \subseteq B))) \to B \in V$
31		difexg	$⊢ B \in V \to B ∖ x \in V$
32	30 31	syl	$⊢ ((A ≼ B \land C \in V) \land (C \neq \emptyset \land (A \approx x \land x \subseteq B))) \to B ∖ x \in V$
33		map0g	$⊢ (C \in V \land B ∖ x \in V) \to (C^{(B ∖ x)} = \emptyset \leftrightarrow (C = \emptyset \land B ∖ x \neq \emptyset))$
34		simpl	$⊢ (C = \emptyset \land B ∖ x \neq \emptyset) \to C = \emptyset$
35	33 34	syl6bi	$⊢ (C \in V \land B ∖ x \in V) \to (C^{(B ∖ x)} = \emptyset \to C = \emptyset)$
36	35	necon3d	$⊢ (C \in V \land B ∖ x \in V) \to (C \neq \emptyset \to C^{(B ∖ x)} \neq \emptyset)$
37	29 32 36	syl2anc	$⊢ ((A ≼ B \land C \in V) \land (C \neq \emptyset \land (A \approx x \land x \subseteq B))) \to (C \neq \emptyset \to C^{(B ∖ x)} \neq \emptyset)$
38	28 37	mpd	$⊢ ((A ≼ B \land C \in V) \land (C \neq \emptyset \land (A \approx x \land x \subseteq B))) \to C^{(B ∖ x)} \neq \emptyset$
39		xpdom3	$⊢ (C^{x} \in V \land C^{(B ∖ x)} \in V \land C^{(B ∖ x)} \neq \emptyset) \to (C^{x}) ≼ ((C^{x}) \times (C^{(B ∖ x)}))$
40	26 27 38 39	syl3anc	$⊢ ((A ≼ B \land C \in V) \land (C \neq \emptyset \land (A \approx x \land x \subseteq B))) \to (C^{x}) ≼ ((C^{x}) \times (C^{(B ∖ x)}))$
41		vex	$⊢ x \in V$
42	41	a1i	$⊢ ((A ≼ B \land C \in V) \land (C \neq \emptyset \land (A \approx x \land x \subseteq B))) \to x \in V$
43		disjdif	$⊢ x \cap (B ∖ x) = \emptyset$
44	43	a1i	$⊢ ((A ≼ B \land C \in V) \land (C \neq \emptyset \land (A \approx x \land x \subseteq B))) \to x \cap (B ∖ x) = \emptyset$
45		mapunen	$⊢ ((x \in V \land B ∖ x \in V \land C \in V) \land x \cap (B ∖ x) = \emptyset) \to (C^{(x \cup (B ∖ x))}) \approx ((C^{x}) \times (C^{(B ∖ x)}))$
46	42 32 29 44 45	syl31anc	$⊢ ((A ≼ B \land C \in V) \land (C \neq \emptyset \land (A \approx x \land x \subseteq B))) \to (C^{(x \cup (B ∖ x))}) \approx ((C^{x}) \times (C^{(B ∖ x)}))$
47	46	ensymd	$⊢ ((A ≼ B \land C \in V) \land (C \neq \emptyset \land (A \approx x \land x \subseteq B))) \to ((C^{x}) \times (C^{(B ∖ x)})) \approx (C^{(x \cup (B ∖ x))})$
48		simprrr	$⊢ ((A ≼ B \land C \in V) \land (C \neq \emptyset \land (A \approx x \land x \subseteq B))) \to x \subseteq B$
49		undif	$⊢ x \subseteq B \leftrightarrow x \cup (B ∖ x) = B$
50	48 49	sylib	$⊢ ((A ≼ B \land C \in V) \land (C \neq \emptyset \land (A \approx x \land x \subseteq B))) \to x \cup (B ∖ x) = B$
51	50	oveq2d	$⊢ ((A ≼ B \land C \in V) \land (C \neq \emptyset \land (A \approx x \land x \subseteq B))) \to C^{(x \cup (B ∖ x))} = C^{B}$
52	47 51	breqtrd	$⊢ ((A ≼ B \land C \in V) \land (C \neq \emptyset \land (A \approx x \land x \subseteq B))) \to ((C^{x}) \times (C^{(B ∖ x)})) \approx (C^{B})$
53		domentr	$⊢ ((C^{x}) ≼ ((C^{x}) \times (C^{(B ∖ x)})) \land ((C^{x}) \times (C^{(B ∖ x)})) \approx (C^{B})) \to (C^{x}) ≼ (C^{B})$
54	40 52 53	syl2anc	$⊢ ((A ≼ B \land C \in V) \land (C \neq \emptyset \land (A \approx x \land x \subseteq B))) \to (C^{x}) ≼ (C^{B})$
55		endomtr	$⊢ ((C^{A}) \approx (C^{x}) \land (C^{x}) ≼ (C^{B})) \to (C^{A}) ≼ (C^{B})$
56	25 54 55	syl2anc	$⊢ ((A ≼ B \land C \in V) \land (C \neq \emptyset \land (A \approx x \land x \subseteq B))) \to (C^{A}) ≼ (C^{B})$
57	56	expr	$⊢ ((A ≼ B \land C \in V) \land C \neq \emptyset) \to ((A \approx x \land x \subseteq B) \to (C^{A}) ≼ (C^{B}))$
58	57	exlimdv	$⊢ ((A ≼ B \land C \in V) \land C \neq \emptyset) \to (\exists x (A \approx x \land x \subseteq B) \to (C^{A}) ≼ (C^{B}))$
59	20 58	mpd	$⊢ ((A ≼ B \land C \in V) \land C \neq \emptyset) \to (C^{A}) ≼ (C^{B})$
60	59	adantlr	$⊢ (((A ≼ B \land C \in V) \land \neg (A = \emptyset \land C = \emptyset)) \land C \neq \emptyset) \to (C^{A}) ≼ (C^{B})$
61	13 60	pm2.61dane	$⊢ ((A ≼ B \land C \in V) \land \neg (A = \emptyset \land C = \emptyset)) \to (C^{A}) ≼ (C^{B})$
62	61	an32s	$⊢ ((A ≼ B \land \neg (A = \emptyset \land C = \emptyset)) \land C \in V) \to (C^{A}) ≼ (C^{B})$
63	62	ex	$⊢ (A ≼ B \land \neg (A = \emptyset \land C = \emptyset)) \to (C \in V \to (C^{A}) ≼ (C^{B}))$
64		reldmmap	$⊢ Rel dom ↑_{𝑚}$
65	64	ovprc1	$⊢ \neg C \in V \to C^{A} = \emptyset$
66	65 12	eqbrtrdi	$⊢ \neg C \in V \to (C^{A}) ≼ (C^{B})$
67	63 66	pm2.61d1	$⊢ (A ≼ B \land \neg (A = \emptyset \land C = \emptyset)) \to (C^{A}) ≼ (C^{B})$

Metamath Proof Explorer

Theorem mapdom2

Proof