Metamath Proof Explorer


Theorem fpwrelmapffslem

Description: Lemma for fpwrelmapffs . For this theorem, the sets A and B could be infinite, but the relation R itself is finite. (Contributed by Thierry Arnoux, 1-Sep-2017) (Revised by Thierry Arnoux, 1-Sep-2019)

Ref Expression
Hypotheses fpwrelmapffslem.1 A V
fpwrelmapffslem.2 B V
fpwrelmapffslem.3 φ F : A 𝒫 B
fpwrelmapffslem.4 φ R = x y | x A y F x
Assertion fpwrelmapffslem φ R Fin ran F Fin F supp Fin

Proof

Step Hyp Ref Expression
1 fpwrelmapffslem.1 A V
2 fpwrelmapffslem.2 B V
3 fpwrelmapffslem.3 φ F : A 𝒫 B
4 fpwrelmapffslem.4 φ R = x y | x A y F x
5 relopab Rel x y | x A y F x
6 releq R = x y | x A y F x Rel R Rel x y | x A y F x
7 5 6 mpbiri R = x y | x A y F x Rel R
8 relfi Rel R R Fin dom R Fin ran R Fin
9 4 7 8 3syl φ R Fin dom R Fin ran R Fin
10 rexcom4 x A z w z z = F x z x A w z z = F x
11 ancom z = F x w z w z z = F x
12 11 exbii z z = F x w z z w z z = F x
13 fvex F x V
14 eleq2 z = F x w z w F x
15 13 14 ceqsexv z z = F x w z w F x
16 12 15 bitr3i z w z z = F x w F x
17 16 rexbii x A z w z z = F x x A w F x
18 r19.42v x A w z z = F x w z x A z = F x
19 18 exbii z x A w z z = F x z w z x A z = F x
20 10 17 19 3bitr3ri z w z x A z = F x x A w F x
21 df-rex x A w F x x x A w F x
22 20 21 bitr2i x x A w F x z w z x A z = F x
23 22 a1i φ x x A w F x z w z x A z = F x
24 vex w V
25 eleq1w y = w y F x w F x
26 25 anbi2d y = w x A y F x x A w F x
27 26 exbidv y = w x x A y F x x x A w F x
28 24 27 elab w y | x x A y F x x x A w F x
29 eluniab w z | x A z = F x z w z x A z = F x
30 23 28 29 3bitr4g φ w y | x x A y F x w z | x A z = F x
31 30 eqrdv φ y | x x A y F x = z | x A z = F x
32 31 eleq1d φ y | x x A y F x Fin z | x A z = F x Fin
33 32 adantr φ dom R Fin y | x x A y F x Fin z | x A z = F x Fin
34 ffn F : A 𝒫 B F Fn A
35 fnrnfv F Fn A ran F = z | x A z = F x
36 3 34 35 3syl φ ran F = z | x A z = F x
37 36 adantr φ dom R Fin ran F = z | x A z = F x
38 0ex V
39 38 a1i φ dom R Fin V
40 fex F : A 𝒫 B A V F V
41 3 1 40 sylancl φ F V
42 41 adantr φ dom R Fin F V
43 3 ffund φ Fun F
44 43 adantr φ dom R Fin Fun F
45 opabdm R = x y | x A y F x dom R = x | y x A y F x
46 4 45 syl φ dom R = x | y x A y F x
47 1 40 mpan2 F : A 𝒫 B F V
48 suppimacnv F V V F supp = F -1 V
49 38 48 mpan2 F V F supp = F -1 V
50 3 47 49 3syl φ F supp = F -1 V
51 3 feqmptd φ F = x A F x
52 51 cnveqd φ F -1 = x A F x -1
53 52 imaeq1d φ F -1 V = x A F x -1 V
54 50 53 eqtrd φ F supp = x A F x -1 V
55 eqid x A F x = x A F x
56 55 mptpreima x A F x -1 V = x A | F x V
57 54 56 syl6eq φ F supp = x A | F x V
58 suppvalfn F Fn A A V V F supp = x A | F x
59 1 38 58 mp3an23 F Fn A F supp = x A | F x
60 3 34 59 3syl φ F supp = x A | F x
61 n0 F x y y F x
62 61 rabbii x A | F x = x A | y y F x
63 62 a1i φ x A | F x = x A | y y F x
64 60 57 63 3eqtr3d φ x A | F x V = x A | y y F x
65 df-rab x A | y y F x = x | x A y y F x
66 19.42v y x A y F x x A y y F x
67 66 abbii x | y x A y F x = x | x A y y F x
68 65 67 eqtr4i x A | y y F x = x | y x A y F x
69 68 a1i φ x A | y y F x = x | y x A y F x
70 57 64 69 3eqtrd φ F supp = x | y x A y F x
71 46 70 eqtr4d φ dom R = F supp
72 71 eleq1d φ dom R Fin F supp Fin
73 72 biimpa φ dom R Fin F supp Fin
74 39 42 44 73 ffsrn φ dom R Fin ran F Fin
75 37 74 eqeltrrd φ dom R Fin z | x A z = F x Fin
76 unifi z | x A z = F x Fin z | x A z = F x Fin z | x A z = F x Fin
77 76 ex z | x A z = F x Fin z | x A z = F x Fin z | x A z = F x Fin
78 75 77 syl φ dom R Fin z | x A z = F x Fin z | x A z = F x Fin
79 unifi3 z | x A z = F x Fin z | x A z = F x Fin
80 78 79 impbid1 φ dom R Fin z | x A z = F x Fin z | x A z = F x Fin
81 33 80 bitr4d φ dom R Fin y | x x A y F x Fin z | x A z = F x Fin
82 opabrn R = x y | x A y F x ran R = y | x x A y F x
83 4 82 syl φ ran R = y | x x A y F x
84 83 eleq1d φ ran R Fin y | x x A y F x Fin
85 84 adantr φ dom R Fin ran R Fin y | x x A y F x Fin
86 37 sseq1d φ dom R Fin ran F Fin z | x A z = F x Fin
87 81 85 86 3bitr4d φ dom R Fin ran R Fin ran F Fin
88 87 pm5.32da φ dom R Fin ran R Fin dom R Fin ran F Fin
89 72 anbi1d φ dom R Fin ran F Fin F supp Fin ran F Fin
90 88 89 bitrd φ dom R Fin ran R Fin F supp Fin ran F Fin
91 ancom F supp Fin ran F Fin ran F Fin F supp Fin
92 91 a1i φ F supp Fin ran F Fin ran F Fin F supp Fin
93 9 90 92 3bitrd φ R Fin ran F Fin F supp Fin