Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  mapdom1 Unicode version

Theorem mapdom1 7026
 Description: Order-preserving property of set exponentiation. Theorem 6L(c) of [Enderton] p. 149. (Contributed by NM, 27-Jul-2004.) (Revised by Mario Carneiro, 9-Mar-2013.)
Assertion
Ref Expression
mapdom1

Proof of Theorem mapdom1
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 reldom 6869 . . . . . . 7
21brrelex2i 4730 . . . . . 6
3 domeng 6876 . . . . . 6
42, 3syl 15 . . . . 5
54ibi 232 . . . 4
7 simpl 443 . . . . . . 7
8 enrefg 6893 . . . . . . . 8
98adantl 452 . . . . . . 7
10 mapen 7025 . . . . . . 7
117, 9, 10syl2anr 464 . . . . . 6
12 ovex 5883 . . . . . . 7
132ad2antrr 706 . . . . . . . 8
14 simprr 733 . . . . . . . 8
15 mapss 6810 . . . . . . . 8
1613, 14, 15syl2anc 642 . . . . . . 7
17 ssdomg 6907 . . . . . . 7
1812, 16, 17mpsyl 59 . . . . . 6
19 endomtr 6919 . . . . . 6
2011, 18, 19syl2anc 642 . . . . 5
2120ex 423 . . . 4
2221exlimdv 1664 . . 3
236, 22mpd 14 . 2
24 elmapex 6791 . . . . . . 7
2524simprd 449 . . . . . 6
2625con3i 127 . . . . 5
2726eq0rdv 3489 . . . 4