Metamath Proof Explorer


Theorem dom2lem

Description: A mapping (first hypothesis) that is one-to-one (second hypothesis) implies its domain is dominated by its codomain. (Contributed by NM, 24-Jul-2004)

Ref Expression
Hypotheses dom2d.1 φxACB
dom2d.2 φxAyAC=Dx=y
Assertion dom2lem φxAC:A1-1B

Proof

Step Hyp Ref Expression
1 dom2d.1 φxACB
2 dom2d.2 φxAyAC=Dx=y
3 1 ralrimiv φxACB
4 eqid xAC=xAC
5 4 fmpt xACBxAC:AB
6 3 5 sylib φxAC:AB
7 1 imp φxACB
8 4 fvmpt2 xACBxACx=C
9 8 adantll φxACBxACx=C
10 7 9 mpdan φxAxACx=C
11 10 adantrr φxAyAxACx=C
12 nfv xφyA
13 nffvmpt1 _xxACy
14 13 nfeq1 xxACy=D
15 12 14 nfim xφyAxACy=D
16 eleq1w x=yxAyA
17 16 anbi2d x=yφxAφyA
18 17 imbi1d x=yφxAxACx=CφyAxACx=C
19 16 anbi1d x=yxAyAyAyA
20 anidm yAyAyA
21 19 20 bitrdi x=yxAyAyA
22 21 anbi2d x=yφxAyAφyA
23 fveq2 x=yxACx=xACy
24 23 adantr x=yφxAyAxACx=xACy
25 2 imp φxAyAC=Dx=y
26 25 biimparc x=yφxAyAC=D
27 24 26 eqeq12d x=yφxAyAxACx=CxACy=D
28 27 ex x=yφxAyAxACx=CxACy=D
29 22 28 sylbird x=yφyAxACx=CxACy=D
30 29 pm5.74d x=yφyAxACx=CφyAxACy=D
31 18 30 bitrd x=yφxAxACx=CφyAxACy=D
32 15 31 10 chvarfv φyAxACy=D
33 32 adantrl φxAyAxACy=D
34 11 33 eqeq12d φxAyAxACx=xACyC=D
35 25 biimpd φxAyAC=Dx=y
36 34 35 sylbid φxAyAxACx=xACyx=y
37 36 ralrimivva φxAyAxACx=xACyx=y
38 nfmpt1 _xxAC
39 nfcv _yxAC
40 38 39 dff13f xAC:A1-1BxAC:ABxAyAxACx=xACyx=y
41 6 37 40 sylanbrc φxAC:A1-1B