Metamath Proof Explorer


Theorem resf1o

Description: Restriction of functions to a superset of their support creates a bijection. (Contributed by Thierry Arnoux, 12-Sep-2017)

Ref Expression
Hypotheses resf1o.1 X = f B A | f -1 B Z C
resf1o.2 F = f X f C
Assertion resf1o A V B W C A Z B F : X 1-1 onto B C

Proof

Step Hyp Ref Expression
1 resf1o.1 X = f B A | f -1 B Z C
2 resf1o.2 F = f X f C
3 resexg f X f C V
4 3 adantl A V B W C A Z B f X f C V
5 simpr A V B W C A g B C g B C
6 difexg A V A C V
7 6 3ad2ant1 A V B W C A A C V
8 snex Z V
9 xpexg A C V Z V A C × Z V
10 7 8 9 sylancl A V B W C A A C × Z V
11 10 adantr A V B W C A g B C A C × Z V
12 unexg g B C A C × Z V g A C × Z V
13 5 11 12 syl2anc A V B W C A g B C g A C × Z V
14 13 adantlr A V B W C A Z B g B C g A C × Z V
15 1 rabeq2i f X f B A f -1 B Z C
16 15 anbi1i f X g = f C f B A f -1 B Z C g = f C
17 simprr A V B W C A Z B f B A f -1 B Z C g = f C g = f C
18 simprll A V B W C A Z B f B A f -1 B Z C g = f C f B A
19 elmapi f B A f : A B
20 18 19 syl A V B W C A Z B f B A f -1 B Z C g = f C f : A B
21 simp3 A V B W C A C A
22 21 ad2antrr A V B W C A Z B f B A f -1 B Z C g = f C C A
23 20 22 fssresd A V B W C A Z B f B A f -1 B Z C g = f C f C : C B
24 simp2 A V B W C A B W
25 simp1 A V B W C A A V
26 25 21 ssexd A V B W C A C V
27 elmapg B W C V f C B C f C : C B
28 24 26 27 syl2anc A V B W C A f C B C f C : C B
29 28 ad2antrr A V B W C A Z B f B A f -1 B Z C g = f C f C B C f C : C B
30 23 29 mpbird A V B W C A Z B f B A f -1 B Z C g = f C f C B C
31 17 30 eqeltrd A V B W C A Z B f B A f -1 B Z C g = f C g B C
32 undif C A C A C = A
33 32 biimpi C A C A C = A
34 33 reseq2d C A f C A C = f A
35 22 34 syl A V B W C A Z B f B A f -1 B Z C g = f C f C A C = f A
36 ffn f : A B f Fn A
37 fnresdm f Fn A f A = f
38 20 36 37 3syl A V B W C A Z B f B A f -1 B Z C g = f C f A = f
39 35 38 eqtr2d A V B W C A Z B f B A f -1 B Z C g = f C f = f C A C
40 resundi f C A C = f C f A C
41 39 40 eqtrdi A V B W C A Z B f B A f -1 B Z C g = f C f = f C f A C
42 17 eqcomd A V B W C A Z B f B A f -1 B Z C g = f C f C = g
43 simprlr A V B W C A Z B f B A f -1 B Z C g = f C f -1 B Z C
44 25 ad2antrr A V B W C A Z B f B A f -1 B Z C g = f C A V
45 simplr A V B W C A Z B f B A f -1 B Z C g = f C Z B
46 eqid B Z = B Z
47 46 ffs2 A V Z B f : A B f supp Z = f -1 B Z
48 44 45 20 47 syl3anc A V B W C A Z B f B A f -1 B Z C g = f C f supp Z = f -1 B Z
49 sseqin2 C A A C = C
50 49 biimpi C A A C = C
51 22 50 syl A V B W C A Z B f B A f -1 B Z C g = f C A C = C
52 43 48 51 3sstr4d A V B W C A Z B f B A f -1 B Z C g = f C f supp Z A C
53 simpl f B A Z B f B A
54 53 19 36 3syl f B A Z B f Fn A
55 inundif A C A C = A
56 55 fneq2i f Fn A C A C f Fn A
57 54 56 sylibr f B A Z B f Fn A C A C
58 vex f V
59 58 a1i f B A Z B f V
60 simpr f B A Z B Z B
61 inindif A C A C =
62 61 a1i f B A Z B A C A C =
63 fnsuppres f Fn A C A C f V Z B A C A C = f supp Z A C f A C = A C × Z
64 57 59 60 62 63 syl121anc f B A Z B f supp Z A C f A C = A C × Z
65 18 45 64 syl2anc A V B W C A Z B f B A f -1 B Z C g = f C f supp Z A C f A C = A C × Z
66 52 65 mpbid A V B W C A Z B f B A f -1 B Z C g = f C f A C = A C × Z
67 42 66 uneq12d A V B W C A Z B f B A f -1 B Z C g = f C f C f A C = g A C × Z
68 41 67 eqtrd A V B W C A Z B f B A f -1 B Z C g = f C f = g A C × Z
69 31 68 jca A V B W C A Z B f B A f -1 B Z C g = f C g B C f = g A C × Z
70 24 ad2antrr A V B W C A Z B g B C f = g A C × Z B W
71 25 ad2antrr A V B W C A Z B g B C f = g A C × Z A V
72 elmapi g B C g : C B
73 72 ad2antrl A V B W C A Z B g B C f = g A C × Z g : C B
74 simplr A V B W C A Z B g B C f = g A C × Z Z B
75 fconst6g Z B A C × Z : A C B
76 74 75 syl A V B W C A Z B g B C f = g A C × Z A C × Z : A C B
77 disjdif C A C =
78 77 a1i A V B W C A Z B g B C f = g A C × Z C A C =
79 fun2 g : C B A C × Z : A C B C A C = g A C × Z : C A C B
80 73 76 78 79 syl21anc A V B W C A Z B g B C f = g A C × Z g A C × Z : C A C B
81 simprr A V B W C A Z B g B C f = g A C × Z f = g A C × Z
82 81 eqcomd A V B W C A Z B g B C f = g A C × Z g A C × Z = f
83 21 ad2antrr A V B W C A Z B g B C f = g A C × Z C A
84 83 33 syl A V B W C A Z B g B C f = g A C × Z C A C = A
85 82 84 feq12d A V B W C A Z B g B C f = g A C × Z g A C × Z : C A C B f : A B
86 80 85 mpbid A V B W C A Z B g B C f = g A C × Z f : A B
87 elmapg B W A V f B A f : A B
88 87 biimpar B W A V f : A B f B A
89 70 71 86 88 syl21anc A V B W C A Z B g B C f = g A C × Z f B A
90 71 74 86 47 syl3anc A V B W C A Z B g B C f = g A C × Z f supp Z = f -1 B Z
91 81 adantr A V B W C A Z B g B C f = g A C × Z x A C f = g A C × Z
92 91 fveq1d A V B W C A Z B g B C f = g A C × Z x A C f x = g A C × Z x
93 73 adantr A V B W C A Z B g B C f = g A C × Z x A C g : C B
94 93 ffnd A V B W C A Z B g B C f = g A C × Z x A C g Fn C
95 fconstg Z B A C × Z : A C Z
96 95 ad3antlr A V B W C A Z B g B C f = g A C × Z x A C A C × Z : A C Z
97 96 ffnd A V B W C A Z B g B C f = g A C × Z x A C A C × Z Fn A C
98 77 a1i A V B W C A Z B g B C f = g A C × Z x A C C A C =
99 simpr A V B W C A Z B g B C f = g A C × Z x A C x A C
100 fvun2 g Fn C A C × Z Fn A C C A C = x A C g A C × Z x = A C × Z x
101 94 97 98 99 100 syl112anc A V B W C A Z B g B C f = g A C × Z x A C g A C × Z x = A C × Z x
102 fvconst A C × Z : A C Z x A C A C × Z x = Z
103 96 99 102 syl2anc A V B W C A Z B g B C f = g A C × Z x A C A C × Z x = Z
104 92 101 103 3eqtrd A V B W C A Z B g B C f = g A C × Z x A C f x = Z
105 86 104 suppss A V B W C A Z B g B C f = g A C × Z f supp Z C
106 90 105 eqsstrrd A V B W C A Z B g B C f = g A C × Z f -1 B Z C
107 81 reseq1d A V B W C A Z B g B C f = g A C × Z f C = g A C × Z C
108 res0 A C × Z =
109 res0 g =
110 108 109 eqtr4i A C × Z = g
111 77 reseq2i A C × Z C A C = A C × Z
112 77 reseq2i g C A C = g
113 110 111 112 3eqtr4ri g C A C = A C × Z C A C
114 113 a1i A V B W C A Z B g B C f = g A C × Z g C A C = A C × Z C A C
115 fresaunres1 g : C B A C × Z : A C B g C A C = A C × Z C A C g A C × Z C = g
116 73 76 114 115 syl3anc A V B W C A Z B g B C f = g A C × Z g A C × Z C = g
117 107 116 eqtr2d A V B W C A Z B g B C f = g A C × Z g = f C
118 89 106 117 jca31 A V B W C A Z B g B C f = g A C × Z f B A f -1 B Z C g = f C
119 69 118 impbida A V B W C A Z B f B A f -1 B Z C g = f C g B C f = g A C × Z
120 16 119 syl5bb A V B W C A Z B f X g = f C g B C f = g A C × Z
121 2 4 14 120 f1od A V B W C A Z B F : X 1-1 onto B C