Metamath Proof Explorer


Theorem f1oresf1o

Description: Build a bijection by restricting the domain of a bijection. (Contributed by AV, 31-Jul-2022)

Ref Expression
Hypotheses f1oresf1o.1 φF:A1-1 ontoB
f1oresf1o.2 φDA
f1oresf1o.3 φxDFx=yyBχ
Assertion f1oresf1o φFD:D1-1 ontoyB|χ

Proof

Step Hyp Ref Expression
1 f1oresf1o.1 φF:A1-1 ontoB
2 f1oresf1o.2 φDA
3 f1oresf1o.3 φxDFx=yyBχ
4 f1of1 F:A1-1 ontoBF:A1-1B
5 1 4 syl φF:A1-1B
6 f1ores F:A1-1BDAFD:D1-1 ontoFD
7 5 2 6 syl2anc φFD:D1-1 ontoFD
8 f1ofun F:A1-1 ontoBFunF
9 1 8 syl φFunF
10 f1odm F:A1-1 ontoBdomF=A
11 1 10 syl φdomF=A
12 2 11 sseqtrrd φDdomF
13 dfimafn FunFDdomFFD=y|xDFx=y
14 9 12 13 syl2anc φFD=y|xDFx=y
15 3 abbidv φy|xDFx=y=y|yBχ
16 df-rab yB|χ=y|yBχ
17 15 16 eqtr4di φy|xDFx=y=yB|χ
18 14 17 eqtr2d φyB|χ=FD
19 18 f1oeq3d φFD:D1-1 ontoyB|χFD:D1-1 ontoFD
20 7 19 mpbird φFD:D1-1 ontoyB|χ