Theorem fpwrelmapffslem 27213

Description: Lemma for fpwrelmapffs 27215. 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.)

Hypotheses

Ref	Expression
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

Ref	Expression
fpwrelmapffslem	|- ( ph -> ( R e. Fin <-> ( ran F C_ Fin /\ ( F supp (/) ) e. Fin ) ) )

Distinct variable groups:   x, y, A   x, F, y   x, R, y

Allowed substitution hints:   ph( x, y)   B( x, y)

Proof of Theorem fpwrelmapffslem

Dummy variables w z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fpwrelmapffslem.4	. . . 4 |- ( ph -> R = { <. x , y >. | ( x e. A /\ y e. ( F ` x ) ) } )
2		relopab 5120	. . . . 5 |- Rel { <. x , y >. | ( x e. A /\ y e. ( F ` x ) ) }
3		releq 5076	. . . . 5 |- ( R = { <. x , y >. | ( x e. A /\ y e. ( F ` x ) ) } -> ( Rel R <-> Rel { <. x , y >. | ( x e. A /\ y e. ( F ` x ) ) } ) )
4	2, 3	mpbiri 233	. . . 4 |- ( R = { <. x , y >. | ( x e. A /\ y e. ( F ` x ) ) } -> Rel R )
5	1, 4	syl 16	. . 3 |- ( ph -> Rel R )
6		relfi 27118	. . 3 |- ( Rel R -> ( R e. Fin <-> ( dom R e. Fin /\ ran R e. Fin ) ) )
7	5, 6	syl 16	. 2 |- ( ph -> ( R e. Fin <-> ( dom R e. Fin /\ ran R e. Fin ) ) )
8		rexcom4 3126	. . . . . . . . . . . . 13 |- ( E. x e. A E. z ( w e. z /\ z = ( F ` x ) ) <-> E. z E. x e. A ( w e. z /\ z = ( F ` x ) ) )
9		ancom 450	. . . . . . . . . . . . . . . 16 |- ( ( z = ( F ` x ) /\ w e. z ) <-> ( w e. z /\ z = ( F ` x ) ) )
10	9	exbii 1639	. . . . . . . . . . . . . . 15 |- ( E. z ( z = ( F ` x ) /\ w e. z ) <-> E. z ( w e. z /\ z = ( F ` x ) ) )
11		nfv 1678	. . . . . . . . . . . . . . . 16 |- F/ z w e. ( F ` x )
12		fvex 5867	. . . . . . . . . . . . . . . 16 |- ( F ` x ) e. _V
13		eleq2 2533	. . . . . . . . . . . . . . . 16 |- ( z = ( F ` x ) -> ( w e. z <-> w e. ( F ` x ) ) )
14	11, 12, 13	ceqsex 3142	. . . . . . . . . . . . . . 15 |- ( E. z ( z = ( F ` x ) /\ w e. z ) <-> w e. ( F ` x ) )
15	10, 14	bitr3i 251	. . . . . . . . . . . . . 14 |- ( E. z ( w e. z /\ z = ( F ` x ) ) <-> w e. ( F ` x ) )
16	15	rexbii 2958	. . . . . . . . . . . . 13 |- ( E. x e. A E. z ( w e. z /\ z = ( F ` x ) ) <-> E. x e. A w e. ( F ` x ) )
17		r19.42v 3009	. . . . . . . . . . . . . 14 |- ( E. x e. A ( w e. z /\ z = ( F ` x ) ) <-> ( w e. z /\ E. x e. A z = ( F ` x ) ) )
18	17	exbii 1639	. . . . . . . . . . . . 13 |- ( E. z E. x e. A ( w e. z /\ z = ( F ` x ) ) <-> E. z ( w e. z /\ E. x e. A z = ( F ` x ) ) )
19	8, 16, 18	3bitr3ri 276	. . . . . . . . . . . 12 |- ( E. z ( w e. z /\ E. x e. A z = ( F ` x ) ) <-> E. x e. A w e. ( F ` x ) )
20		df-rex 2813	. . . . . . . . . . . 12 |- ( E. x e. A w e. ( F ` x ) <-> E. x ( x e. A /\ w e. ( F ` x ) ) )
21	19, 20	bitr2i 250	. . . . . . . . . . 11 |- ( E. x ( x e. A /\ w e. ( F ` x ) ) <-> E. z ( w e. z /\ E. x e. A z = ( F ` x ) ) )
22	21	a1i 11	. . . . . . . . . 10 |- ( ph -> ( E. x ( x e. A /\ w e. ( F ` x ) ) <-> E. z ( w e. z /\ E. x e. A z = ( F ` x ) ) ) )
23		vex 3109	. . . . . . . . . . 11 |- w e. _V
24		nfv 1678	. . . . . . . . . . . 12 |- F/ x y = w
25		biidd 237	. . . . . . . . . . . . 13 |- ( y = w -> ( x e. A <-> x e. A ) )
26		eleq1 2532	. . . . . . . . . . . . 13 |- ( y = w -> ( y e. ( F ` x ) <-> w e. ( F ` x ) ) )
27	25, 26	anbi12d 710	. . . . . . . . . . . 12 |- ( y = w -> ( ( x e. A /\ y e. ( F ` x ) ) <-> ( x e. A /\ w e. ( F ` x ) ) ) )
28	24, 27	exbid 1829	. . . . . . . . . . 11 |- ( y = w -> ( E. x ( x e. A /\ y e. ( F ` x ) ) <-> E. x ( x e. A /\ w e. ( F ` x ) ) ) )
29	23, 28	elab 3243	. . . . . . . . . 10 |- ( w e. { y | E. x ( x e. A /\ y e. ( F ` x ) ) } <-> E. x ( x e. A /\ w e. ( F ` x ) ) )
30		eluniab 4249	. . . . . . . . . 10 |- ( w e. U. { z | E. x e. A z = ( F ` x ) } <-> E. z ( w e. z /\ E. x e. A z = ( F ` x ) ) )
31	22, 29, 30	3bitr4g 288	. . . . . . . . 9 |- ( ph -> ( w e. { y | E. x ( x e. A /\ y e. ( F ` x ) ) } <-> w e. U. { z | E. x e. A z = ( F ` x ) } ) )
32	31	eqrdv 2457	. . . . . . . 8 |- ( ph -> { y | E. x ( x e. A /\ y e. ( F ` x ) ) } = U. { z | E. x e. A z = ( F ` x ) } )
33	32	eleq1d 2529	. . . . . . 7 |- ( ph -> ( { y | E. x ( x e. A /\ y e. ( F ` x ) ) } e. Fin <-> U. { z | E. x e. A z = ( F ` x ) } e. Fin ) )
34	33	adantr 465	. . . . . 6 |- ( ( 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 ) )
35		fpwrelmapffslem.3	. . . . . . . . . . 11 |- ( ph -> F : A --> ~P B )
36		ffn 5722	. . . . . . . . . . 11 |- ( F : A --> ~P B -> F Fn A )
37		fnrnfv 5905	. . . . . . . . . . 11 |- ( F Fn A -> ran F = { z | E. x e. A z = ( F ` x ) } )
38	35, 36, 37	3syl 20	. . . . . . . . . 10 |- ( ph -> ran F = { z | E. x e. A z = ( F ` x ) } )
39	38	adantr 465	. . . . . . . . 9 |- ( ( ph /\ dom R e. Fin ) -> ran F = { z | E. x e. A z = ( F ` x ) } )
40		0ex 4570	. . . . . . . . . . 11 |- (/) e. _V
41	40	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ dom R e. Fin ) -> (/) e. _V )
42		fpwrelmapffslem.1	. . . . . . . . . . . 12 |- A e. _V
43		fex 6124	. . . . . . . . . . . 12 |- ( ( F : A --> ~P B /\ A e. _V ) -> F e. _V )
44	35, 42, 43	sylancl 662	. . . . . . . . . . 11 |- ( ph -> F e. _V )
45	44	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ dom R e. Fin ) -> F e. _V )
46		ffun 5724	. . . . . . . . . . . 12 |- ( F : A --> ~P B -> Fun F )
47	35, 46	syl 16	. . . . . . . . . . 11 |- ( ph -> Fun F )
48	47	adantr 465	. . . . . . . . . 10 |- ( ( ph /\ dom R e. Fin ) -> Fun F )
49		opabdm 27123	. . . . . . . . . . . . . 14 |- ( R = { <. x , y >. | ( x e. A /\ y e. ( F ` x ) ) } -> dom R = { x | E. y ( x e. A /\ y e. ( F ` x ) ) } )
50	1, 49	syl 16	. . . . . . . . . . . . 13 |- ( ph -> dom R = { x | E. y ( x e. A /\ y e. ( F ` x ) ) } )
51	42, 43	mpan2 671	. . . . . . . . . . . . . . . . 17 |- ( F : A --> ~P B -> F e. _V )
52		suppimacnv 6902	. . . . . . . . . . . . . . . . . 18 |- ( ( F e. _V /\ (/) e. _V ) -> ( F supp (/) ) = ( `' F " ( _V \ { (/) } ) ) )
53	40, 52	mpan2 671	. . . . . . . . . . . . . . . . 17 |- ( F e. _V -> ( F supp (/) ) = ( `' F " ( _V \ { (/) } ) ) )
54	35, 51, 53	3syl 20	. . . . . . . . . . . . . . . 16 |- ( ph -> ( F supp (/) ) = ( `' F " ( _V \ { (/) } ) ) )
55	35	feqmptd 5911	. . . . . . . . . . . . . . . . . 18 |- ( ph -> F = ( x e. A |-> ( F ` x ) ) )
56	55	cnveqd 5169	. . . . . . . . . . . . . . . . 17 |- ( ph -> `' F = `' ( x e. A |-> ( F ` x ) ) )
57	56	imaeq1d 5327	. . . . . . . . . . . . . . . 16 |- ( ph -> ( `' F " ( _V \ { (/) } ) ) = ( `' ( x e. A |-> ( F ` x ) ) " ( _V \ { (/) } ) ) )
58	54, 57	eqtrd 2501	. . . . . . . . . . . . . . 15 |- ( ph -> ( F supp (/) ) = ( `' ( x e. A |-> ( F ` x ) ) " ( _V \ { (/) } ) ) )
59		eqid 2460	. . . . . . . . . . . . . . . 16 |- ( x e. A |-> ( F ` x ) ) = ( x e. A |-> ( F ` x ) )
60	59	mptpreima 5491	. . . . . . . . . . . . . . 15 |- ( `' ( x e. A |-> ( F ` x ) ) " ( _V \ { (/) } ) ) = { x e. A | ( F ` x ) e. ( _V \ { (/) } ) }
61	58, 60	syl6eq 2517	. . . . . . . . . . . . . 14 |- ( ph -> ( F supp (/) ) = { x e. A | ( F ` x ) e. ( _V \ { (/) } ) } )
62		suppvalfn 6898	. . . . . . . . . . . . . . . . 17 |- ( ( F Fn A /\ A e. _V /\ (/) e. _V ) -> ( F supp (/) ) = { x e. A | ( F ` x ) =/= (/) } )
63	42, 40, 62	mp3an23 1311	. . . . . . . . . . . . . . . 16 |- ( F Fn A -> ( F supp (/) ) = { x e. A | ( F ` x ) =/= (/) } )
64	35, 36, 63	3syl 20	. . . . . . . . . . . . . . 15 |- ( ph -> ( F supp (/) ) = { x e. A | ( F ` x ) =/= (/) } )
65		n0 3787	. . . . . . . . . . . . . . . . . 18 |- ( ( F ` x ) =/= (/) <-> E. y y e. ( F ` x ) )
66	65	a1i 11	. . . . . . . . . . . . . . . . 17 |- ( x e. A -> ( ( F ` x ) =/= (/) <-> E. y y e. ( F ` x ) ) )
67	66	rabbiia 3095	. . . . . . . . . . . . . . . 16 |- { x e. A | ( F ` x ) =/= (/) } = { x e. A | E. y y e. ( F ` x ) }
68	67	a1i 11	. . . . . . . . . . . . . . 15 |- ( ph -> { x e. A | ( F ` x ) =/= (/) } = { x e. A | E. y y e. ( F ` x ) } )
69	64, 61, 68	3eqtr3d 2509	. . . . . . . . . . . . . 14 |- ( ph -> { x e. A | ( F ` x ) e. ( _V \ { (/) } ) } = { x e. A | E. y y e. ( F ` x ) } )
70		df-rab 2816	. . . . . . . . . . . . . . . 16 |- { x e. A | E. y y e. ( F ` x ) } = { x | ( x e. A /\ E. y y e. ( F ` x ) ) }
71		19.42v 1942	. . . . . . . . . . . . . . . . 17 |- ( E. y ( x e. A /\ y e. ( F ` x ) ) <-> ( x e. A /\ E. y y e. ( F ` x ) ) )
72	71	abbii 2594	. . . . . . . . . . . . . . . 16 |- { x | E. y ( x e. A /\ y e. ( F ` x ) ) } = { x | ( x e. A /\ E. y y e. ( F ` x ) ) }
73	70, 72	eqtr4i 2492	. . . . . . . . . . . . . . 15 |- { x e. A | E. y y e. ( F ` x ) } = { x | E. y ( x e. A /\ y e. ( F ` x ) ) }
74	73	a1i 11	. . . . . . . . . . . . . 14 |- ( ph -> { x e. A | E. y y e. ( F ` x ) } = { x | E. y ( x e. A /\ y e. ( F ` x ) ) } )
75	61, 69, 74	3eqtrd 2505	. . . . . . . . . . . . 13 |- ( ph -> ( F supp (/) ) = { x | E. y ( x e. A /\ y e. ( F ` x ) ) } )
76	50, 75	eqtr4d 2504	. . . . . . . . . . . 12 |- ( ph -> dom R = ( F supp (/) ) )
77	76	eleq1d 2529	. . . . . . . . . . 11 |- ( ph -> ( dom R e. Fin <-> ( F supp (/) ) e. Fin ) )
78	77	biimpa 484	. . . . . . . . . 10 |- ( ( ph /\ dom R e. Fin ) -> ( F supp (/) ) e. Fin )
79	41, 45, 48, 78	ffsrn 27210	. . . . . . . . 9 |- ( ( ph /\ dom R e. Fin ) -> ran F e. Fin )
80	39, 79	eqeltrrd 2549	. . . . . . . 8 |- ( ( ph /\ dom R e. Fin ) -> { z | E. x e. A z = ( F ` x ) } e. Fin )
81		unifi 7798	. . . . . . . . 9 |- ( ( { 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 )
82	81	ex 434	. . . . . . . 8 |- ( { 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 ) )
83	80, 82	syl 16	. . . . . . 7 |- ( ( 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 ) )
84		unifi3 27186	. . . . . . . 8 |- ( U. { z | E. x e. A z = ( F ` x ) } e. Fin -> { z | E. x e. A z = ( F ` x ) } C_ Fin )
85	84	a1i 11	. . . . . . 7 |- ( ( ph /\ dom R e. Fin ) -> ( U. { z | E. x e. A z = ( F ` x ) } e. Fin -> { z | E. x e. A z = ( F ` x ) } C_ Fin ) )
86	83, 85	impbid 191	. . . . . 6 |- ( ( 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 ) )
87	34, 86	bitr4d 256	. . . . 5 |- ( ( 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 ) )
88		opabrn 27124	. . . . . . . 8 |- ( R = { <. x , y >. | ( x e. A /\ y e. ( F ` x ) ) } -> ran R = { y | E. x ( x e. A /\ y e. ( F ` x ) ) } )
89	1, 88	syl 16	. . . . . . 7 |- ( ph -> ran R = { y | E. x ( x e. A /\ y e. ( F ` x ) ) } )
90	89	eleq1d 2529	. . . . . 6 |- ( ph -> ( ran R e. Fin <-> { y | E. x ( x e. A /\ y e. ( F ` x ) ) } e. Fin ) )
91	90	adantr 465	. . . . 5 |- ( ( ph /\ dom R e. Fin ) -> ( ran R e. Fin <-> { y | E. x ( x e. A /\ y e. ( F ` x ) ) } e. Fin ) )
92	39	sseq1d 3524	. . . . 5 |- ( ( ph /\ dom R e. Fin ) -> ( ran F C_ Fin <-> { z | E. x e. A z = ( F ` x ) } C_ Fin ) )
93	87, 91, 92	3bitr4d 285	. . . 4 |- ( ( ph /\ dom R e. Fin ) -> ( ran R e. Fin <-> ran F C_ Fin ) )
94	93	pm5.32da 641	. . 3 |- ( ph -> ( ( dom R e. Fin /\ ran R e. Fin ) <-> ( dom R e. Fin /\ ran F C_ Fin ) ) )
95	77	anbi1d 704	. . 3 |- ( ph -> ( ( dom R e. Fin /\ ran F C_ Fin ) <-> ( ( F supp (/) ) e. Fin /\ ran F C_ Fin ) ) )
96	94, 95	bitrd 253	. 2 |- ( ph -> ( ( dom R e. Fin /\ ran R e. Fin ) <-> ( ( F supp (/) ) e. Fin /\ ran F C_ Fin ) ) )
97		ancom 450	. . 3 |- ( ( ( F supp (/) ) e. Fin /\ ran F C_ Fin ) <-> ( ran F C_ Fin /\ ( F supp (/) ) e. Fin ) )
98	97	a1i 11	. 2 |- ( ph -> ( ( ( F supp (/) ) e. Fin /\ ran F C_ Fin ) <-> ( ran F C_ Fin /\ ( F supp (/) ) e. Fin ) ) )
99	7, 96, 98	3bitrd 279	1 |- ( ph -> ( R e. Fin <-> ( ran F C_ Fin /\ ( F supp (/) ) e. Fin ) ) )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1374   E.wex 1591   e. wcel 1762   {cab 2445   =/= wne 2655   E.wrex 2808   {crab 2811   _Vcvv 3106   \ cdif 3466   C_ wss 3469   (/)c0 3778   ~Pcpw 4003   {csn 4020   U.cuni 4238   {copab 4497   |-> cmpt 4498   `'ccnv 4991   dom cdm 4992   ran crn 4993   "cima 4995   Rel wrel 4997   Fun wfun 5573   Fn wfn 5574   -->wf 5575   ` cfv 5579  (class class class)co 6275   supp csupp 6891   Fincfn 7506

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-8 1764  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-rep 4551  ax-sep 4561  ax-nul 4569  ax-pow 4618  ax-pr 4679  ax-un 6567  ax-ac2 8832

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 969  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-reu 2814  df-rmo 2815  df-rab 2816  df-v 3108  df-sbc 3325  df-csb 3429  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-pss 3485  df-nul 3779  df-if 3933  df-pw 4005  df-sn 4021  df-pr 4023  df-tp 4025  df-op 4027  df-uni 4239  df-int 4276  df-iun 4320  df-br 4441  df-opab 4499  df-mpt 4500  df-tr 4534  df-eprel 4784  df-id 4788  df-po 4793  df-so 4794  df-fr 4831  df-se 4832  df-we 4833  df-ord 4874  df-on 4875  df-lim 4876  df-suc 4877  df-xp 4998  df-rel 4999  df-cnv 5000  df-co 5001  df-dm 5002  df-rn 5003  df-res 5004  df-ima 5005  df-iota 5542  df-fun 5581  df-fn 5582  df-f 5583  df-f1 5584  df-fo 5585  df-f1o 5586  df-fv 5587  df-isom 5588  df-riota 6236  df-ov 6278  df-oprab 6279  df-mpt2 6280  df-om 6672  df-1st 6774  df-2nd 6775  df-supp 6892  df-recs 7032  df-rdg 7066  df-1o 7120  df-oadd 7124  df-er 7301  df-map 7412  df-en 7507  df-dom 7508  df-fin 7510  df-card 8309  df-acn 8312  df-ac 8486

This theorem is referenced by:  fpwrelmapffs  27215