Metamath Proof Explorer


Theorem dom3d

Description: A mapping (first hypothesis) that is one-to-one (second hypothesis) implies its domain is dominated by its codomain. (Contributed by Mario Carneiro, 20-May-2013)

Ref Expression
Hypotheses dom2d.1 φxACB
dom2d.2 φxAyAC=Dx=y
dom3d.3 φAV
dom3d.4 φBW
Assertion dom3d φAB

Proof

Step Hyp Ref Expression
1 dom2d.1 φxACB
2 dom2d.2 φxAyAC=Dx=y
3 dom3d.3 φAV
4 dom3d.4 φBW
5 1 2 dom2lem φxAC:A1-1B
6 f1f xAC:A1-1BxAC:AB
7 5 6 syl φxAC:AB
8 fex2 xAC:ABAVBWxACV
9 7 3 4 8 syl3anc φxACV
10 f1eq1 z=xACz:A1-1BxAC:A1-1B
11 9 5 10 spcedv φzz:A1-1B
12 brdomg BWABzz:A1-1B
13 4 12 syl φABzz:A1-1B
14 11 13 mpbird φAB