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 : A 1-1 onto B
f1oresf1o.2 φ D A
f1oresf1o.3 φ x D F x = y y B χ
Assertion f1oresf1o φ F D : D 1-1 onto y B | χ

Proof

Step Hyp Ref Expression
1 f1oresf1o.1 φ F : A 1-1 onto B
2 f1oresf1o.2 φ D A
3 f1oresf1o.3 φ x D F x = y y B χ
4 f1of1 F : A 1-1 onto B F : A 1-1 B
5 1 4 syl φ F : A 1-1 B
6 f1ores F : A 1-1 B D A F D : D 1-1 onto F D
7 5 2 6 syl2anc φ F D : D 1-1 onto F D
8 f1ofun F : A 1-1 onto B Fun F
9 1 8 syl φ Fun F
10 f1odm F : A 1-1 onto B dom F = A
11 1 10 syl φ dom F = A
12 2 11 sseqtrrd φ D dom F
13 dfimafn Fun F D dom F F D = y | x D F x = y
14 9 12 13 syl2anc φ F D = y | x D F x = y
15 3 abbidv φ y | x D F x = y = y | y B χ
16 df-rab y B | χ = y | y B χ
17 15 16 eqtr4di φ y | x D F x = y = y B | χ
18 14 17 eqtr2d φ y B | χ = F D
19 18 f1oeq3d φ F D : D 1-1 onto y B | χ F D : D 1-1 onto F D
20 7 19 mpbird φ F D : D 1-1 onto y B | χ