Metamath Proof Explorer


Theorem fnpreimac

Description: Choose a set x containing a preimage of each element of a given set B . (Contributed by Thierry Arnoux, 7-May-2023)

Ref Expression
Assertion fnpreimac A V F Fn A B ran F x 𝒫 A x B F x = B

Proof

Step Hyp Ref Expression
1 eqid y B F -1 y = y B F -1 y
2 1 elrnmpt z V z ran y B F -1 y y B z = F -1 y
3 2 elv z ran y B F -1 y y B z = F -1 y
4 simpr A V F Fn A B ran F y B z = F -1 y z = F -1 y
5 simpl3 A V F Fn A B ran F y B B ran F
6 simpr A V F Fn A B ran F y B y B
7 5 6 sseldd A V F Fn A B ran F y B y ran F
8 inisegn0 y ran F F -1 y
9 7 8 sylib A V F Fn A B ran F y B F -1 y
10 9 adantr A V F Fn A B ran F y B z = F -1 y F -1 y
11 4 10 eqnetrd A V F Fn A B ran F y B z = F -1 y z
12 11 r19.29an A V F Fn A B ran F y B z = F -1 y z
13 3 12 sylan2b A V F Fn A B ran F z ran y B F -1 y z
14 13 ralrimiva A V F Fn A B ran F z ran y B F -1 y z
15 simp2 A V F Fn A B ran F F Fn A
16 simp1 A V F Fn A B ran F A V
17 15 16 jca A V F Fn A B ran F F Fn A A V
18 fnex F Fn A A V F V
19 rnexg F V ran F V
20 17 18 19 3syl A V F Fn A B ran F ran F V
21 simp3 A V F Fn A B ran F B ran F
22 20 21 ssexd A V F Fn A B ran F B V
23 mptexg B V y B F -1 y V
24 rnexg y B F -1 y V ran y B F -1 y V
25 22 23 24 3syl A V F Fn A B ran F ran y B F -1 y V
26 fvi ran y B F -1 y V I ran y B F -1 y = ran y B F -1 y
27 25 26 syl A V F Fn A B ran F I ran y B F -1 y = ran y B F -1 y
28 27 raleqdv A V F Fn A B ran F z I ran y B F -1 y z z ran y B F -1 y z
29 14 28 mpbird A V F Fn A B ran F z I ran y B F -1 y z
30 fvex I ran y B F -1 y V
31 30 ac5b z I ran y B F -1 y z f f : I ran y B F -1 y I ran y B F -1 y z I ran y B F -1 y f z z
32 29 31 syl A V F Fn A B ran F f f : I ran y B F -1 y I ran y B F -1 y z I ran y B F -1 y f z z
33 27 unieqd A V F Fn A B ran F I ran y B F -1 y = ran y B F -1 y
34 27 33 feq23d A V F Fn A B ran F f : I ran y B F -1 y I ran y B F -1 y f : ran y B F -1 y ran y B F -1 y
35 27 raleqdv A V F Fn A B ran F z I ran y B F -1 y f z z z ran y B F -1 y f z z
36 34 35 anbi12d A V F Fn A B ran F f : I ran y B F -1 y I ran y B F -1 y z I ran y B F -1 y f z z f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z
37 36 exbidv A V F Fn A B ran F f f : I ran y B F -1 y I ran y B F -1 y z I ran y B F -1 y f z z f f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z
38 32 37 mpbid A V F Fn A B ran F f f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z
39 vex f V
40 39 rnex ran f V
41 40 a1i A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z ran f V
42 simplr A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z f : ran y B F -1 y ran y B F -1 y
43 frn f : ran y B F -1 y ran y B F -1 y ran f ran y B F -1 y
44 42 43 syl A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z ran f ran y B F -1 y
45 nfv y A V F Fn A B ran F
46 nfcv _ y f
47 nfmpt1 _ y y B F -1 y
48 47 nfrn _ y ran y B F -1 y
49 48 nfuni _ y ran y B F -1 y
50 46 48 49 nff y f : ran y B F -1 y ran y B F -1 y
51 45 50 nfan y A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y
52 nfv y f z z
53 48 52 nfralw y z ran y B F -1 y f z z
54 51 53 nfan y A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z
55 17 18 syl A V F Fn A B ran F F V
56 55 ad3antrrr A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z y B F V
57 cnvexg F V F -1 V
58 imaexg F -1 V F -1 y V
59 56 57 58 3syl A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z y B F -1 y V
60 cnvimass F -1 y dom F
61 60 a1i A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z y B F -1 y dom F
62 15 fndmd A V F Fn A B ran F dom F = A
63 62 ad3antrrr A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z y B dom F = A
64 61 63 sseqtrd A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z y B F -1 y A
65 59 64 elpwd A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z y B F -1 y 𝒫 A
66 65 ex A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z y B F -1 y 𝒫 A
67 54 66 ralrimi A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z y B F -1 y 𝒫 A
68 1 rnmptss y B F -1 y 𝒫 A ran y B F -1 y 𝒫 A
69 67 68 syl A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z ran y B F -1 y 𝒫 A
70 sspwuni ran y B F -1 y 𝒫 A ran y B F -1 y A
71 69 70 sylib A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z ran y B F -1 y A
72 44 71 sstrd A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z ran f A
73 41 72 elpwd A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z ran f 𝒫 A
74 fnfun F Fn A Fun F
75 15 74 syl A V F Fn A B ran F Fun F
76 75 ad5antr A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z u ran y B F -1 y v ran y B F -1 y f u = f v Fun F
77 sndisj Disj y B y
78 disjpreima Fun F Disj y B y Disj y B F -1 y
79 76 77 78 sylancl A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z u ran y B F -1 y v ran y B F -1 y f u = f v Disj y B F -1 y
80 disjrnmpt Disj y B F -1 y Disj z ran y B F -1 y z
81 79 80 syl A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z u ran y B F -1 y v ran y B F -1 y f u = f v Disj z ran y B F -1 y z
82 simpllr A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z u ran y B F -1 y v ran y B F -1 y f u = f v u ran y B F -1 y
83 simplr A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z u ran y B F -1 y v ran y B F -1 y f u = f v v ran y B F -1 y
84 simp-4r A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z u ran y B F -1 y v ran y B F -1 y f u = f v z ran y B F -1 y f z z
85 fveq2 z = u f z = f u
86 id z = u z = u
87 85 86 eleq12d z = u f z z f u u
88 87 rspcv u ran y B F -1 y z ran y B F -1 y f z z f u u
89 88 imp u ran y B F -1 y z ran y B F -1 y f z z f u u
90 82 84 89 syl2anc A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z u ran y B F -1 y v ran y B F -1 y f u = f v f u u
91 simpr A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z u ran y B F -1 y v ran y B F -1 y f u = f v f u = f v
92 fveq2 z = v f z = f v
93 id z = v z = v
94 92 93 eleq12d z = v f z z f v v
95 94 rspcv v ran y B F -1 y z ran y B F -1 y f z z f v v
96 95 imp v ran y B F -1 y z ran y B F -1 y f z z f v v
97 83 84 96 syl2anc A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z u ran y B F -1 y v ran y B F -1 y f u = f v f v v
98 91 97 eqeltrd A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z u ran y B F -1 y v ran y B F -1 y f u = f v f u v
99 86 93 disji Disj z ran y B F -1 y z u ran y B F -1 y v ran y B F -1 y f u u f u v u = v
100 81 82 83 90 98 99 syl122anc A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z u ran y B F -1 y v ran y B F -1 y f u = f v u = v
101 100 ex A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z u ran y B F -1 y v ran y B F -1 y f u = f v u = v
102 101 anasss A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z u ran y B F -1 y v ran y B F -1 y f u = f v u = v
103 102 ralrimivva A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z u ran y B F -1 y v ran y B F -1 y f u = f v u = v
104 42 103 jca A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z f : ran y B F -1 y ran y B F -1 y u ran y B F -1 y v ran y B F -1 y f u = f v u = v
105 dff13 f : ran y B F -1 y 1-1 ran y B F -1 y f : ran y B F -1 y ran y B F -1 y u ran y B F -1 y v ran y B F -1 y f u = f v u = v
106 104 105 sylibr A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z f : ran y B F -1 y 1-1 ran y B F -1 y
107 f1f1orn f : ran y B F -1 y 1-1 ran y B F -1 y f : ran y B F -1 y 1-1 onto ran f
108 106 107 syl A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z f : ran y B F -1 y 1-1 onto ran f
109 f1oen3g f V f : ran y B F -1 y 1-1 onto ran f ran y B F -1 y ran f
110 39 108 109 sylancr A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z ran y B F -1 y ran f
111 110 ensymd A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z ran f ran y B F -1 y
112 22 23 syl A V F Fn A B ran F y B F -1 y V
113 112 ad2antrr A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z y B F -1 y V
114 59 ex A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z y B F -1 y V
115 54 114 ralrimi A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z y B F -1 y V
116 75 ad5antr A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z y B t B y t Fun F
117 simpr A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z y B t B y t y t
118 21 ad5antr A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z y B t B y t B ran F
119 simpllr A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z y B t B y t y B
120 118 119 sseldd A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z y B t B y t y ran F
121 simplr A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z y B t B y t t B
122 118 121 sseldd A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z y B t B y t t ran F
123 116 117 120 122 preimane A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z y B t B y t F -1 y F -1 t
124 123 ex A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z y B t B y t F -1 y F -1 t
125 124 necon4d A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z y B t B F -1 y = F -1 t y = t
126 125 ralrimiva A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z y B t B F -1 y = F -1 t y = t
127 126 ex A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z y B t B F -1 y = F -1 t y = t
128 54 127 ralrimi A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z y B t B F -1 y = F -1 t y = t
129 115 128 jca A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z y B F -1 y V y B t B F -1 y = F -1 t y = t
130 sneq y = t y = t
131 130 imaeq2d y = t F -1 y = F -1 t
132 1 131 f1mpt y B F -1 y : B 1-1 V y B F -1 y V y B t B F -1 y = F -1 t y = t
133 129 132 sylibr A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z y B F -1 y : B 1-1 V
134 f1f1orn y B F -1 y : B 1-1 V y B F -1 y : B 1-1 onto ran y B F -1 y
135 133 134 syl A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z y B F -1 y : B 1-1 onto ran y B F -1 y
136 f1oen3g y B F -1 y V y B F -1 y : B 1-1 onto ran y B F -1 y B ran y B F -1 y
137 113 135 136 syl2anc A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z B ran y B F -1 y
138 137 ensymd A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z ran y B F -1 y B
139 entr ran f ran y B F -1 y ran y B F -1 y B ran f B
140 111 138 139 syl2anc A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z ran f B
141 imass2 ran f ran y B F -1 y F ran f F ran y B F -1 y
142 43 141 syl f : ran y B F -1 y ran y B F -1 y F ran f F ran y B F -1 y
143 42 142 syl A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z F ran f F ran y B F -1 y
144 imauni F ran y B F -1 y = z ran y B F -1 y F z
145 imaeq2 z = F -1 y F z = F F -1 y
146 55 adantr A V F Fn A B ran F y B F V
147 146 57 58 3syl A V F Fn A B ran F y B F -1 y V
148 145 147 iunrnmptss A V F Fn A B ran F z ran y B F -1 y F z y B F F -1 y
149 funimacnv Fun F F F -1 y = y ran F
150 75 149 syl A V F Fn A B ran F F F -1 y = y ran F
151 150 adantr A V F Fn A B ran F y B F F -1 y = y ran F
152 6 snssd A V F Fn A B ran F y B y B
153 152 5 sstrd A V F Fn A B ran F y B y ran F
154 df-ss y ran F y ran F = y
155 153 154 sylib A V F Fn A B ran F y B y ran F = y
156 151 155 eqtrd A V F Fn A B ran F y B F F -1 y = y
157 156 iuneq2dv A V F Fn A B ran F y B F F -1 y = y B y
158 iunid y B y = B
159 157 158 eqtrdi A V F Fn A B ran F y B F F -1 y = B
160 148 159 sseqtrd A V F Fn A B ran F z ran y B F -1 y F z B
161 160 ad2antrr A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z z ran y B F -1 y F z B
162 144 161 eqsstrid A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z F ran y B F -1 y B
163 143 162 sstrd A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z F ran f B
164 42 adantr A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z t B f : ran y B F -1 y ran y B F -1 y
165 164 ffund A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z t B Fun f
166 simpr A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z t B t B
167 55 57 syl A V F Fn A B ran F F -1 V
168 167 ad3antrrr A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z t B F -1 V
169 imaexg F -1 V F -1 t V
170 168 169 syl A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z t B F -1 t V
171 1 131 elrnmpt1s t B F -1 t V F -1 t ran y B F -1 y
172 166 170 171 syl2anc A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z t B F -1 t ran y B F -1 y
173 164 fdmd A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z t B dom f = ran y B F -1 y
174 172 173 eleqtrrd A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z t B F -1 t dom f
175 fvelrn Fun f F -1 t dom f f F -1 t ran f
176 165 174 175 syl2anc A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z t B f F -1 t ran f
177 15 ad3antrrr A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z t B F Fn A
178 simplr A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z t B z ran y B F -1 y f z z
179 fveq2 z = F -1 t f z = f F -1 t
180 id z = F -1 t z = F -1 t
181 179 180 eleq12d z = F -1 t f z z f F -1 t F -1 t
182 181 rspcv F -1 t ran y B F -1 y z ran y B F -1 y f z z f F -1 t F -1 t
183 182 imp F -1 t ran y B F -1 y z ran y B F -1 y f z z f F -1 t F -1 t
184 172 178 183 syl2anc A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z t B f F -1 t F -1 t
185 fniniseg F Fn A f F -1 t F -1 t f F -1 t A F f F -1 t = t
186 185 simplbda F Fn A f F -1 t F -1 t F f F -1 t = t
187 177 184 186 syl2anc A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z t B F f F -1 t = t
188 fveqeq2 k = f F -1 t F k = t F f F -1 t = t
189 188 rspcev f F -1 t ran f F f F -1 t = t k ran f F k = t
190 176 187 189 syl2anc A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z t B k ran f F k = t
191 72 adantr A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z t B ran f A
192 177 191 fvelimabd A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z t B t F ran f k ran f F k = t
193 190 192 mpbird A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z t B t F ran f
194 193 ex A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z t B t F ran f
195 194 ssrdv A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z B F ran f
196 163 195 eqssd A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z F ran f = B
197 140 196 jca A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z ran f B F ran f = B
198 breq1 x = ran f x B ran f B
199 imaeq2 x = ran f F x = F ran f
200 199 eqeq1d x = ran f F x = B F ran f = B
201 198 200 anbi12d x = ran f x B F x = B ran f B F ran f = B
202 201 rspcev ran f 𝒫 A ran f B F ran f = B x 𝒫 A x B F x = B
203 73 197 202 syl2anc A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z x 𝒫 A x B F x = B
204 203 anasss A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z x 𝒫 A x B F x = B
205 204 ex A V F Fn A B ran F f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z x 𝒫 A x B F x = B
206 205 exlimdv A V F Fn A B ran F f f : ran y B F -1 y ran y B F -1 y z ran y B F -1 y f z z x 𝒫 A x B F x = B
207 38 206 mpd A V F Fn A B ran F x 𝒫 A x B F x = B