Metamath Proof Explorer

Theorem iinpreima

Description: Preimage of an intersection. (Contributed by FL, 16-Apr-2012)

Ref Expression
Assertion iinpreima ⊢Fun⁡F∧A≠∅→F-1⋂x∈AB=⋂x∈AF-1B

Proof

Step Hyp Ref Expression
1 simpll ⊢Fun⁡F∧A≠∅∧y∈F-1⋂x∈AB→Fun⁡F
2 cnvimass ⊢F-1⋂x∈AB⊆dom⁡F
3 2 sseli ⊢y∈F-1⋂x∈AB→y∈dom⁡F
4 3 adantl ⊢Fun⁡F∧A≠∅∧y∈F-1⋂x∈AB→y∈dom⁡F
5 fvex ⊢F⁡y∈V
6 fvimacnvi ⊢Fun⁡F∧y∈F-1⋂x∈AB→F⁡y∈⋂x∈AB
7 6 adantlr ⊢Fun⁡F∧A≠∅∧y∈F-1⋂x∈AB→F⁡y∈⋂x∈AB
8 eliin ⊢F⁡y∈V→F⁡y∈⋂x∈AB↔∀x∈AF⁡y∈B
9 8 biimpa ⊢F⁡y∈V∧F⁡y∈⋂x∈AB→∀x∈AF⁡y∈B
10 5 7 9 sylancr ⊢Fun⁡F∧A≠∅∧y∈F-1⋂x∈AB→∀x∈AF⁡y∈B
11 fvimacnv ⊢Fun⁡F∧y∈dom⁡F→F⁡y∈B↔y∈F-1B
12 11 ralbidv ⊢Fun⁡F∧y∈dom⁡F→∀x∈AF⁡y∈B↔∀x∈Ay∈F-1B
13 12 biimpa ⊢Fun⁡F∧y∈dom⁡F∧∀x∈AF⁡y∈B→∀x∈Ay∈F-1B
14 1 4 10 13 syl21anc ⊢Fun⁡F∧A≠∅∧y∈F-1⋂x∈AB→∀x∈Ay∈F-1B
15 eliin ⊢y∈V→y∈⋂x∈AF-1B↔∀x∈Ay∈F-1B
16 15 elv ⊢y∈⋂x∈AF-1B↔∀x∈Ay∈F-1B
17 14 16 sylibr ⊢Fun⁡F∧A≠∅∧y∈F-1⋂x∈AB→y∈⋂x∈AF-1B
18 simpll ⊢Fun⁡F∧A≠∅∧y∈⋂x∈AF-1B→Fun⁡F
19 15 biimpd ⊢y∈V→y∈⋂x∈AF-1B→∀x∈Ay∈F-1B
20 19 elv ⊢y∈⋂x∈AF-1B→∀x∈Ay∈F-1B
21 20 adantl ⊢Fun⁡F∧A≠∅∧y∈⋂x∈AF-1B→∀x∈Ay∈F-1B
22 fvimacnvi ⊢Fun⁡F∧y∈F-1B→F⁡y∈B
23 22 ex ⊢Fun⁡F→y∈F-1B→F⁡y∈B
24 23 ralimdv ⊢Fun⁡F→∀x∈Ay∈F-1B→∀x∈AF⁡y∈B
25 18 21 24 sylc ⊢Fun⁡F∧A≠∅∧y∈⋂x∈AF-1B→∀x∈AF⁡y∈B
26 5 8 ax-mp ⊢F⁡y∈⋂x∈AB↔∀x∈AF⁡y∈B
27 25 26 sylibr ⊢Fun⁡F∧A≠∅∧y∈⋂x∈AF-1B→F⁡y∈⋂x∈AB
28 r19.2zb ⊢A≠∅↔∀x∈Ay∈F-1B→∃x∈Ay∈F-1B
29 28 biimpi ⊢A≠∅→∀x∈Ay∈F-1B→∃x∈Ay∈F-1B
30 cnvimass ⊢F-1B⊆dom⁡F
31 30 sseli ⊢y∈F-1B→y∈dom⁡F
32 31 rexlimivw ⊢∃x∈Ay∈F-1B→y∈dom⁡F
33 29 32 syl6 ⊢A≠∅→∀x∈Ay∈F-1B→y∈dom⁡F
34 16 33 biimtrid ⊢A≠∅→y∈⋂x∈AF-1B→y∈dom⁡F
35 34 adantl ⊢Fun⁡F∧A≠∅→y∈⋂x∈AF-1B→y∈dom⁡F
36 35 imp ⊢Fun⁡F∧A≠∅∧y∈⋂x∈AF-1B→y∈dom⁡F
37 fvimacnv ⊢Fun⁡F∧y∈dom⁡F→F⁡y∈⋂x∈AB↔y∈F-1⋂x∈AB
38 18 36 37 syl2anc ⊢Fun⁡F∧A≠∅∧y∈⋂x∈AF-1B→F⁡y∈⋂x∈AB↔y∈F-1⋂x∈AB
39 27 38 mpbid ⊢Fun⁡F∧A≠∅∧y∈⋂x∈AF-1B→y∈F-1⋂x∈AB
40 17 39 impbida ⊢Fun⁡F∧A≠∅→y∈F-1⋂x∈AB↔y∈⋂x∈AF-1B
41 40 eqrdv ⊢Fun⁡F∧A≠∅→F-1⋂x∈AB=⋂x∈AF-1B