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	30	difexd	$⊢ ((A ≼ B \land C \in V) \land (C \neq \emptyset \land (A \approx x \land x \subseteq B))) \to B ∖ x \in V$
32		map0g	$⊢ (C \in V \land B ∖ x \in V) \to (C^{(B ∖ x)} = \emptyset \leftrightarrow (C = \emptyset \land B ∖ x \neq \emptyset))$
33		simpl	$⊢ (C = \emptyset \land B ∖ x \neq \emptyset) \to C = \emptyset$
34	32 33	biimtrdi	$⊢ (C \in V \land B ∖ x \in V) \to (C^{(B ∖ x)} = \emptyset \to C = \emptyset)$
35	34	necon3d	$⊢ (C \in V \land B ∖ x \in V) \to (C \neq \emptyset \to C^{(B ∖ x)} \neq \emptyset)$
36	29 31 35	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)$
37	28 36	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$
38		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)}))$
39	26 27 37 38	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)}))$
40		vex	$⊢ x \in V$
41	40	a1i	$⊢ ((A ≼ B \land C \in V) \land (C \neq \emptyset \land (A \approx x \land x \subseteq B))) \to x \in V$
42		disjdif	$⊢ x \cap (B ∖ x) = \emptyset$
43	42	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$
44		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)}))$
45	41 31 29 43 44	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)}))$
46	45	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))})$
47		simprrr	$⊢ ((A ≼ B \land C \in V) \land (C \neq \emptyset \land (A \approx x \land x \subseteq B))) \to x \subseteq B$
48		undif	$⊢ x \subseteq B \leftrightarrow x \cup (B ∖ x) = B$
49	47 48	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$
50	49	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}$
51	46 50	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})$
52		domentr	$⊢ ((C^{x}) ≼ ((C^{x}) \times (C^{(B ∖ x)})) \land ((C^{x}) \times (C^{(B ∖ x)})) \approx (C^{B})) \to (C^{x}) ≼ (C^{B})$
53	39 51 52	syl2anc	$⊢ ((A ≼ B \land C \in V) \land (C \neq \emptyset \land (A \approx x \land x \subseteq B))) \to (C^{x}) ≼ (C^{B})$
54		endomtr	$⊢ ((C^{A}) \approx (C^{x}) \land (C^{x}) ≼ (C^{B})) \to (C^{A}) ≼ (C^{B})$
55	25 53 54	syl2anc	$⊢ ((A ≼ B \land C \in V) \land (C \neq \emptyset \land (A \approx x \land x \subseteq B))) \to (C^{A}) ≼ (C^{B})$
56	55	expr	$⊢ ((A ≼ B \land C \in V) \land C \neq \emptyset) \to ((A \approx x \land x \subseteq B) \to (C^{A}) ≼ (C^{B}))$
57	56	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}))$
58	20 57	mpd	$⊢ ((A ≼ B \land C \in V) \land C \neq \emptyset) \to (C^{A}) ≼ (C^{B})$
59	58	adantlr	$⊢ (((A ≼ B \land C \in V) \land \neg (A = \emptyset \land C = \emptyset)) \land C \neq \emptyset) \to (C^{A}) ≼ (C^{B})$
60	13 59	pm2.61dane	$⊢ ((A ≼ B \land C \in V) \land \neg (A = \emptyset \land C = \emptyset)) \to (C^{A}) ≼ (C^{B})$
61	60	an32s	$⊢ ((A ≼ B \land \neg (A = \emptyset \land C = \emptyset)) \land C \in V) \to (C^{A}) ≼ (C^{B})$
62	61	ex	$⊢ (A ≼ B \land \neg (A = \emptyset \land C = \emptyset)) \to (C \in V \to (C^{A}) ≼ (C^{B}))$
63		reldmmap	$⊢ Rel dom ↑_{𝑚}$
64	63	ovprc1	$⊢ \neg C \in V \to C^{A} = \emptyset$
65	64 12	eqbrtrdi	$⊢ \neg C \in V \to (C^{A}) ≼ (C^{B})$
66	62 65	pm2.61d1	$⊢ (A ≼ B \land \neg (A = \emptyset \land C = \emptyset)) \to (C^{A}) ≼ (C^{B})$

Metamath Proof Explorer

Theorem mapdom2

Proof