Metamath Proof Explorer

Theorem ofpreima

Description: Express the preimage of a function operation as a union of preimages. (Contributed by Thierry Arnoux, 8-Mar-2018)

Ref Expression
Hypotheses ofpreima.1 ⊢ φ → F : A ⟶ B
ofpreima.2 ⊢ φ → G : A ⟶ C
ofpreima.3 ⊢ φ → A ∈ V
ofpreima.4 ⊢ φ → R Fn B × C
Assertion ofpreima ⊢ φ → F R f G -1 D = ⋃ p ∈ R -1 D F -1 1 st ⁡ p ∩ G -1 2 nd ⁡ p

Proof

Step Hyp Ref Expression
1 ofpreima.1 ⊢ φ → F : A ⟶ B
2 ofpreima.2 ⊢ φ → G : A ⟶ C
3 ofpreima.3 ⊢ φ → A ∈ V
4 ofpreima.4 ⊢ φ → R Fn B × C
5 nfmpt1 ⊢ Ⅎ _ s s ∈ A ⟼ F ⁡ s G ⁡ s
6 eqidd ⊢ φ → s ∈ A ⟼ F ⁡ s G ⁡ s = s ∈ A ⟼ F ⁡ s G ⁡ s
7 fnov ⊢ R Fn B × C ↔ R = x ∈ B , y ∈ C ⟼ x R y
8 4 7 sylib ⊢ φ → R = x ∈ B , y ∈ C ⟼ x R y
9 5 1 2 3 6 8 ofoprabco ⊢ φ → F R f G = R ∘ s ∈ A ⟼ F ⁡ s G ⁡ s
10 9 cnveqd ⊢ φ → F R f G -1 = R ∘ s ∈ A ⟼ F ⁡ s G ⁡ s -1
11 cnvco ⊢ R ∘ s ∈ A ⟼ F ⁡ s G ⁡ s -1 = s ∈ A ⟼ F ⁡ s G ⁡ s -1 ∘ R -1
12 10 11 eqtrdi ⊢ φ → F R f G -1 = s ∈ A ⟼ F ⁡ s G ⁡ s -1 ∘ R -1
13 12 imaeq1d ⊢ φ → F R f G -1 D = s ∈ A ⟼ F ⁡ s G ⁡ s -1 ∘ R -1 D
14 imaco ⊢ s ∈ A ⟼ F ⁡ s G ⁡ s -1 ∘ R -1 D = s ∈ A ⟼ F ⁡ s G ⁡ s -1 R -1 D
15 13 14 eqtrdi ⊢ φ → F R f G -1 D = s ∈ A ⟼ F ⁡ s G ⁡ s -1 R -1 D
16 dfima2 ⊢ s ∈ A ⟼ F ⁡ s G ⁡ s -1 R -1 D = q | ∃ p ∈ R -1 D p s ∈ A ⟼ F ⁡ s G ⁡ s -1 q
17 vex ⊢ p ∈ V
18 vex ⊢ q ∈ V
19 17 18 brcnv ⊢ p s ∈ A ⟼ F ⁡ s G ⁡ s -1 q ↔ q s ∈ A ⟼ F ⁡ s G ⁡ s p
20 funmpt ⊢ Fun ⁡ s ∈ A ⟼ F ⁡ s G ⁡ s
21 funbrfv2b ⊢ Fun ⁡ s ∈ A ⟼ F ⁡ s G ⁡ s → q s ∈ A ⟼ F ⁡ s G ⁡ s p ↔ q ∈ dom ⁡ s ∈ A ⟼ F ⁡ s G ⁡ s ∧ s ∈ A ⟼ F ⁡ s G ⁡ s ⁡ q = p
22 20 21 ax-mp ⊢ q s ∈ A ⟼ F ⁡ s G ⁡ s p ↔ q ∈ dom ⁡ s ∈ A ⟼ F ⁡ s G ⁡ s ∧ s ∈ A ⟼ F ⁡ s G ⁡ s ⁡ q = p
23 opex ⊢ F ⁡ s G ⁡ s ∈ V
24 eqid ⊢ s ∈ A ⟼ F ⁡ s G ⁡ s = s ∈ A ⟼ F ⁡ s G ⁡ s
25 23 24 dmmpti ⊢ dom ⁡ s ∈ A ⟼ F ⁡ s G ⁡ s = A
26 25 eleq2i ⊢ q ∈ dom ⁡ s ∈ A ⟼ F ⁡ s G ⁡ s ↔ q ∈ A
27 26 anbi1i ⊢ q ∈ dom ⁡ s ∈ A ⟼ F ⁡ s G ⁡ s ∧ s ∈ A ⟼ F ⁡ s G ⁡ s ⁡ q = p ↔ q ∈ A ∧ s ∈ A ⟼ F ⁡ s G ⁡ s ⁡ q = p
28 22 27 bitri ⊢ q s ∈ A ⟼ F ⁡ s G ⁡ s p ↔ q ∈ A ∧ s ∈ A ⟼ F ⁡ s G ⁡ s ⁡ q = p
29 fveq2 ⊢ s = q → F ⁡ s = F ⁡ q
30 fveq2 ⊢ s = q → G ⁡ s = G ⁡ q
31 29 30 opeq12d ⊢ s = q → F ⁡ s G ⁡ s = F ⁡ q G ⁡ q
32 opex ⊢ F ⁡ q G ⁡ q ∈ V
33 31 24 32 fvmpt ⊢ q ∈ A → s ∈ A ⟼ F ⁡ s G ⁡ s ⁡ q = F ⁡ q G ⁡ q
34 33 eqeq1d ⊢ q ∈ A → s ∈ A ⟼ F ⁡ s G ⁡ s ⁡ q = p ↔ F ⁡ q G ⁡ q = p
35 34 pm5.32i ⊢ q ∈ A ∧ s ∈ A ⟼ F ⁡ s G ⁡ s ⁡ q = p ↔ q ∈ A ∧ F ⁡ q G ⁡ q = p
36 19 28 35 3bitri ⊢ p s ∈ A ⟼ F ⁡ s G ⁡ s -1 q ↔ q ∈ A ∧ F ⁡ q G ⁡ q = p
37 36 rexbii ⊢ ∃ p ∈ R -1 D p s ∈ A ⟼ F ⁡ s G ⁡ s -1 q ↔ ∃ p ∈ R -1 D q ∈ A ∧ F ⁡ q G ⁡ q = p
38 37 abbii ⊢ q | ∃ p ∈ R -1 D p s ∈ A ⟼ F ⁡ s G ⁡ s -1 q = q | ∃ p ∈ R -1 D q ∈ A ∧ F ⁡ q G ⁡ q = p
39 nfv ⊢ Ⅎ q φ
40 nfab1 ⊢ Ⅎ _ q q | ∃ p ∈ R -1 D q ∈ A ∧ F ⁡ q G ⁡ q = p
41 nfcv ⊢ Ⅎ _ q ⋃ p ∈ R -1 D F -1 1 st ⁡ p ∩ G -1 2 nd ⁡ p
42 eliun ⊢ q ∈ ⋃ p ∈ R -1 D F -1 1 st ⁡ p ∩ G -1 2 nd ⁡ p ↔ ∃ p ∈ R -1 D q ∈ F -1 1 st ⁡ p ∩ G -1 2 nd ⁡ p
43 ffn ⊢ F : A ⟶ B → F Fn A
44 fniniseg ⊢ F Fn A → q ∈ F -1 1 st ⁡ p ↔ q ∈ A ∧ F ⁡ q = 1 st ⁡ p
45 1 43 44 3syl ⊢ φ → q ∈ F -1 1 st ⁡ p ↔ q ∈ A ∧ F ⁡ q = 1 st ⁡ p
46 ffn ⊢ G : A ⟶ C → G Fn A
47 fniniseg ⊢ G Fn A → q ∈ G -1 2 nd ⁡ p ↔ q ∈ A ∧ G ⁡ q = 2 nd ⁡ p
48 2 46 47 3syl ⊢ φ → q ∈ G -1 2 nd ⁡ p ↔ q ∈ A ∧ G ⁡ q = 2 nd ⁡ p
49 45 48 anbi12d ⊢ φ → q ∈ F -1 1 st ⁡ p ∧ q ∈ G -1 2 nd ⁡ p ↔ q ∈ A ∧ F ⁡ q = 1 st ⁡ p ∧ q ∈ A ∧ G ⁡ q = 2 nd ⁡ p
50 elin ⊢ q ∈ F -1 1 st ⁡ p ∩ G -1 2 nd ⁡ p ↔ q ∈ F -1 1 st ⁡ p ∧ q ∈ G -1 2 nd ⁡ p
51 anandi ⊢ q ∈ A ∧ F ⁡ q = 1 st ⁡ p ∧ G ⁡ q = 2 nd ⁡ p ↔ q ∈ A ∧ F ⁡ q = 1 st ⁡ p ∧ q ∈ A ∧ G ⁡ q = 2 nd ⁡ p
52 49 50 51 3bitr4g ⊢ φ → q ∈ F -1 1 st ⁡ p ∩ G -1 2 nd ⁡ p ↔ q ∈ A ∧ F ⁡ q = 1 st ⁡ p ∧ G ⁡ q = 2 nd ⁡ p
53 52 adantr ⊢ φ ∧ p ∈ R -1 D → q ∈ F -1 1 st ⁡ p ∩ G -1 2 nd ⁡ p ↔ q ∈ A ∧ F ⁡ q = 1 st ⁡ p ∧ G ⁡ q = 2 nd ⁡ p
54 cnvimass ⊢ R -1 D ⊆ dom ⁡ R
55 4 fndmd ⊢ φ → dom ⁡ R = B × C
56 54 55 sseqtrid ⊢ φ → R -1 D ⊆ B × C
57 56 sselda ⊢ φ ∧ p ∈ R -1 D → p ∈ B × C
58 1st2nd2 ⊢ p ∈ B × C → p = 1 st ⁡ p 2 nd ⁡ p
59 eqeq2 ⊢ p = 1 st ⁡ p 2 nd ⁡ p → F ⁡ q G ⁡ q = p ↔ F ⁡ q G ⁡ q = 1 st ⁡ p 2 nd ⁡ p
60 57 58 59 3syl ⊢ φ ∧ p ∈ R -1 D → F ⁡ q G ⁡ q = p ↔ F ⁡ q G ⁡ q = 1 st ⁡ p 2 nd ⁡ p
61 fvex ⊢ F ⁡ q ∈ V
62 fvex ⊢ G ⁡ q ∈ V
63 61 62 opth ⊢ F ⁡ q G ⁡ q = 1 st ⁡ p 2 nd ⁡ p ↔ F ⁡ q = 1 st ⁡ p ∧ G ⁡ q = 2 nd ⁡ p
64 60 63 syl6bb ⊢ φ ∧ p ∈ R -1 D → F ⁡ q G ⁡ q = p ↔ F ⁡ q = 1 st ⁡ p ∧ G ⁡ q = 2 nd ⁡ p
65 64 anbi2d ⊢ φ ∧ p ∈ R -1 D → q ∈ A ∧ F ⁡ q G ⁡ q = p ↔ q ∈ A ∧ F ⁡ q = 1 st ⁡ p ∧ G ⁡ q = 2 nd ⁡ p
66 53 65 bitr4d ⊢ φ ∧ p ∈ R -1 D → q ∈ F -1 1 st ⁡ p ∩ G -1 2 nd ⁡ p ↔ q ∈ A ∧ F ⁡ q G ⁡ q = p
67 66 rexbidva ⊢ φ → ∃ p ∈ R -1 D q ∈ F -1 1 st ⁡ p ∩ G -1 2 nd ⁡ p ↔ ∃ p ∈ R -1 D q ∈ A ∧ F ⁡ q G ⁡ q = p
68 abid ⊢ q ∈ q | ∃ p ∈ R -1 D q ∈ A ∧ F ⁡ q G ⁡ q = p ↔ ∃ p ∈ R -1 D q ∈ A ∧ F ⁡ q G ⁡ q = p
69 67 68 bitr4di ⊢ φ → ∃ p ∈ R -1 D q ∈ F -1 1 st ⁡ p ∩ G -1 2 nd ⁡ p ↔ q ∈ q | ∃ p ∈ R -1 D q ∈ A ∧ F ⁡ q G ⁡ q = p
70 42 69 syl5rbb ⊢ φ → q ∈ q | ∃ p ∈ R -1 D q ∈ A ∧ F ⁡ q G ⁡ q = p ↔ q ∈ ⋃ p ∈ R -1 D F -1 1 st ⁡ p ∩ G -1 2 nd ⁡ p
71 39 40 41 70 eqrd ⊢ φ → q | ∃ p ∈ R -1 D q ∈ A ∧ F ⁡ q G ⁡ q = p = ⋃ p ∈ R -1 D F -1 1 st ⁡ p ∩ G -1 2 nd ⁡ p
72 38 71 syl5eq ⊢ φ → q | ∃ p ∈ R -1 D p s ∈ A ⟼ F ⁡ s G ⁡ s -1 q = ⋃ p ∈ R -1 D F -1 1 st ⁡ p ∩ G -1 2 nd ⁡ p
73 16 72 syl5eq ⊢ φ → s ∈ A ⟼ F ⁡ s G ⁡ s -1 R -1 D = ⋃ p ∈ R -1 D F -1 1 st ⁡ p ∩ G -1 2 nd ⁡ p
74 15 73 eqtrd ⊢ φ → F R f G -1 D = ⋃ p ∈ R -1 D F -1 1 st ⁡ p ∩ G -1 2 nd ⁡ p