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 e. _V
fpwrelmapffslem.2 
|- B e. _V
fpwrelmapffslem.3 
|- ( ph -> F : A --> ~P B )
fpwrelmapffslem.4 
|- ( ph -> R = { <. x , y >. | ( x e. A /\ y e. ( F ` x ) ) } )
Assertion fpwrelmapffslem 
|- ( ph -> ( R e. Fin <-> ( ran F C_ Fin /\ ( F supp (/) ) e. Fin ) ) )

Proof

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