This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iinpreima

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

Ref Expression
Assertion iinpreima ( ( Fun 𝐹 ∧ 𝐴 ≠ ∅ ) → ( ◡ 𝐹 “ ∩ 𝑥 ∈ 𝐴 𝐵 ) = ∩ 𝑥 ∈ 𝐴 ( ◡ 𝐹 “ 𝐵 ) )

Proof

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