Theorem fpwrelmapffslem 26054

Description: Lemma for fpwrelmapffs 26056. 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 4987	. . . . 5 |- Rel { <. x , y >. | ( x e. A /\ y e. ( F ` x ) ) }
3		releq 4943	. . . . 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 25962	. . 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 3013	. . . . . . . . . . . . 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 1634	. . . . . . . . . . . . . . 15 |- ( E. z ( z = ( F ` x ) /\ w e. z ) <-> E. z ( w e. z /\ z = ( F ` x ) ) )
11		nfv 1673	. . . . . . . . . . . . . . . 16 |- F/ z w e. ( F ` x )
12		fvex 5722	. . . . . . . . . . . . . . . 16 |- ( F ` x ) e. _V
13		eleq2 2504	. . . . . . . . . . . . . . . 16 |- ( z = ( F ` x ) -> ( w e. z <-> w e. ( F ` x ) ) )
14	11, 12, 13	ceqsex 3029	. . . . . . . . . . . . . . 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 2761	. . . . . . . . . . . . 13 |- ( E. x e. A E. z ( w e. z /\ z = ( F ` x ) ) <-> E. x e. A w e. ( F ` x ) )
17		r19.42v 2896	. . . . . . . . . . . . . 14 |- ( E. x e. A ( w e. z /\ z = ( F ` x ) ) <-> ( w e. z /\ E. x e. A z = ( F ` x ) ) )
18	17	exbii 1634	. . . . . . . . . . . . 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 2742	. . . . . . . . . . . 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 2996	. . . . . . . . . . 11 |- w e. _V
24		nfv 1673	. . . . . . . . . . . 12 |- F/ x y = w
25		biidd 237	. . . . . . . . . . . . 13 |- ( y = w -> ( x e. A <-> x e. A ) )
26		eleq1 2503	. . . . . . . . . . . . 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 1820	. . . . . . . . . . 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 3127	. . . . . . . . . 10 |- ( w e. { y | E. x ( x e. A /\ y e. ( F ` x ) ) } <-> E. x ( x e. A /\ w e. ( F ` x ) ) )
30		eluniab 4123	. . . . . . . . . 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 2441	. . . . . . . 8 |- ( ph -> { y | E. x ( x e. A /\ y e. ( F ` x ) ) } = U. { z | E. x e. A z = ( F ` x ) } )
33	32	eleq1d 2509	. . . . . . 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 5580	. . . . . . . . . . 11 |- ( F : A --> ~P B -> F Fn A )
37		fnrnfv 5759	. . . . . . . . . . 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 4443	. . . . . . . . . . 11 |- (/) e. _V
41	40	a1i 11	. . . . . . . . . 10 |- ( ( ph /\ dom R e. Fin ) -> (/) e. _V )
42		fpwrelmapffslem.1	. . . . . . . . . . . 12 |- A e. _V
43		fex 5971	. . . . . . . . . . . 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 5582	. . . . . . . . . . . 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 25965	. . . . . . . . . . . . . 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 6722	. . . . . . . . . . . . . . . . . 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 5765	. . . . . . . . . . . . . . . . . 18 |- ( ph -> F = ( x e. A |-> ( F ` x ) ) )
56	55	cnveqd 5036	. . . . . . . . . . . . . . . . 17 |- ( ph -> `' F = `' ( x e. A |-> ( F ` x ) ) )
57	56	imaeq1d 5189	. . . . . . . . . . . . . . . 16 |- ( ph -> ( `' F " ( _V \ { (/) } ) ) = ( `' ( x e. A |-> ( F ` x ) ) " ( _V \ { (/) } ) ) )
58	54, 57	eqtrd 2475	. . . . . . . . . . . . . . 15 |- ( ph -> ( F supp (/) ) = ( `' ( x e. A |-> ( F ` x ) ) " ( _V \ { (/) } ) ) )
59		eqid 2443	. . . . . . . . . . . . . . . 16 |- ( x e. A |-> ( F ` x ) ) = ( x e. A |-> ( F ` x ) )
60	59	mptpreima 5352	. . . . . . . . . . . . . . 15 |- ( `' ( x e. A |-> ( F ` x ) ) " ( _V \ { (/) } ) ) = { x e. A | ( F ` x ) e. ( _V \ { (/) } ) }
61	58, 60	syl6eq 2491	. . . . . . . . . . . . . 14 |- ( ph -> ( F supp (/) ) = { x e. A | ( F ` x ) e. ( _V \ { (/) } ) } )
62		suppvalfn 6718	. . . . . . . . . . . . . . . . 17 |- ( ( F Fn A /\ A e. _V /\ (/) e. _V ) -> ( F supp (/) ) = { x e. A | ( F ` x ) =/= (/) } )
63	42, 40, 62	mp3an23 1306	. . . . . . . . . . . . . . . 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 3667	. . . . . . . . . . . . . . . . . 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 2982	. . . . . . . . . . . . . . . 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 2483	. . . . . . . . . . . . . 14 |- ( ph -> { x e. A | ( F ` x ) e. ( _V \ { (/) } ) } = { x e. A | E. y y e. ( F ` x ) } )
70		df-rab 2745	. . . . . . . . . . . . . . . 16 |- { x e. A | E. y y e. ( F ` x ) } = { x | ( x e. A /\ E. y y e. ( F ` x ) ) }
71		19.42v 1924	. . . . . . . . . . . . . . . . 17 |- ( E. y ( x e. A /\ y e. ( F ` x ) ) <-> ( x e. A /\ E. y y e. ( F ` x ) ) )
72	71	abbii 2561	. . . . . . . . . . . . . . . 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 2466	. . . . . . . . . . . . . . 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 2479	. . . . . . . . . . . . 13 |- ( ph -> ( F supp (/) ) = { x | E. y ( x e. A /\ y e. ( F ` x ) ) } )
76	50, 75	eqtr4d 2478	. . . . . . . . . . . 12 |- ( ph -> dom R = ( F supp (/) ) )
77	76	eleq1d 2509	. . . . . . . . . . 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 26051	. . . . . . . . 9 |- ( ( ph /\ dom R e. Fin ) -> ran F e. Fin )
80	39, 79	eqeltrrd 2518	. . . . . . . 8 |- ( ( ph /\ dom R e. Fin ) -> { z | E. x e. A z = ( F ` x ) } e. Fin )
81		unifi 7621	. . . . . . . . 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 26027	. . . . . . . 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 25966	. . . . . . . 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 2509	. . . . . 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 3404	. . . . 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 1369   E.wex 1586   e. wcel 1756   {cab 2429   =/= wne 2620   E.wrex 2737   {crab 2740   _Vcvv 2993   \ cdif 3346   C_ wss 3349   (/)c0 3658   ~Pcpw 3881   {csn 3898   U.cuni 4112   {copab 4370   e. cmpt 4371   `'ccnv 4860   dom cdm 4861   ran crn 4862   "cima 4864   Rel wrel 4866   Fun wfun 5433   Fn wfn 5434   -->wf 5435   ` cfv 5439  (class class class)co 6112   supp csupp 6711   Fincfn 7331

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4424  ax-sep 4434  ax-nul 4442  ax-pow 4491  ax-pr 4552  ax-un 6393  ax-ac2 8653

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2741  df-rex 2742  df-reu 2743  df-rmo 2744  df-rab 2745  df-v 2995  df-sbc 3208  df-csb 3310  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-pss 3365  df-nul 3659  df-if 3813  df-pw 3883  df-sn 3899  df-pr 3901  df-tp 3903  df-op 3905  df-uni 4113  df-int 4150  df-iun 4194  df-br 4314  df-opab 4372  df-mpt 4373  df-tr 4407  df-eprel 4653  df-id 4657  df-po 4662  df-so 4663  df-fr 4700  df-se 4701  df-we 4702  df-ord 4743  df-on 4744  df-lim 4745  df-suc 4746  df-xp 4867  df-rel 4868  df-cnv 4869  df-co 4870  df-dm 4871  df-rn 4872  df-res 4873  df-ima 4874  df-iota 5402  df-fun 5441  df-fn 5442  df-f 5443  df-f1 5444  df-fo 5445  df-f1o 5446  df-fv 5447  df-isom 5448  df-riota 6073  df-ov 6115  df-oprab 6116  df-mpt2 6117  df-om 6498  df-1st 6598  df-2nd 6599  df-supp 6712  df-recs 6853  df-rdg 6887  df-1o 6941  df-oadd 6945  df-er 7122  df-map 7237  df-en 7332  df-dom 7333  df-fin 7335  df-card 8130  df-acn 8133  df-ac 8307

This theorem is referenced by:  fpwrelmapffs  26056