# Metamath Proof Explorer

## Theorem 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 ${⊢}\left({A}\preccurlyeq {B}\wedge ¬\left({A}=\varnothing \wedge {C}=\varnothing \right)\right)\to \left({{C}}^{{A}}\right)\preccurlyeq \left({{C}}^{{B}}\right)$

### Proof

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