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

Theorem mapdom1 6911
 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
StepHypRef Expression
1 reldom 6755 . . . . . . 7
21brrelex2i 4637 . . . . . 6
3 domeng 6762 . . . . . 6
42, 3syl 17 . . . . 5
54ibi 234 . . . 4
7 simpl 445 . . . . . . 7
8 enrefg 6779 . . . . . . . 8
98adantl 454 . . . . . . 7
10 mapen 6910 . . . . . . 7
117, 9, 10syl2anr 466 . . . . . 6
12 ovex 5735 . . . . . . 7
132ad2antrr 709 . . . . . . . 8
14 simprr 736 . . . . . . . 8
15 mapss 6696 . . . . . . . 8
1613, 14, 15syl2anc 645 . . . . . . 7
17 ssdomg 6793 . . . . . . 7
1812, 16, 17mpsyl 61 . . . . . 6
19 endomtr 6804 . . . . . 6
2011, 18, 19syl2anc 645 . . . . 5
2120ex 425 . . . 4
2221exlimdv 1932 . . 3
236, 22mpd 16 . 2
24 elmapex 6677 . . . . . . 7
2524simprd 451 . . . . . 6
2625con3i 129 . . . . 5
2726eq0rdv 3396 . . . 4